Industrial controllers.

Stream: Real-time Systems

[Omri Schwarz]

I work with and around industrial controllers, and am very interested in using Lean either to run agents on such hardware (Modbus in, Modbus out, formally verified algorithms in between) or to at least prototype them before writing them in Rust.

[Omri Schwarz]

Dear all.

Since I work on industrial controllers, I find myself looking at a very particular
function.

It is piecewise linear. Monotonic. Has a negative Ymin and positive Ymax.
It usually has a sigmoid shape. It has a limited number of inflection points.
It runs through the origin. And it either has 0 discontinuities, or it has a horizontal
segment hitting the origin, with one vertical discontinuity on either side.

So let's call it the Noodleman Sigmoid.

Noodleman Sigmoids are ubiquitous in industrial controllers. The input and output
is almost always Modbus registers, so it's quantized to some range of integers. THe
intent is to keep a process stable with negative feedback within the controller's capability.

And the controllers will usually combine these Noodleman Sigmoids. Multiple inputs,
each with its own Noodleman Sigmoid, sometimes combined as a weighted sum. Or sometimes
there's an inner sigmoid for one input, placed within the flat deadband of another
sigmoid for another input which takes over if the second input is outside its flat deadband.
Sometimes you have to compose a Honig Sigmoid with another Noodleman Sigmoid.

So, I wonder:

1. has any applied mathematician written any proofs for interesting properties of Noodleman Sigmoids?
   a. Are any of those proofs written in something like Coq, Lean, or Haskell?

2. Is there any software library with a general implementation of Noodleman Sigmoids?
   (partial answer: Rust has a linear interpolation function that can be roped into this space)

[Mario Carneiro]

@Omri Schwarz It sounds like Noodleman sigmoids are a made up term, so I'm not sure what you are expecting for (1). Libraries usually only have definitions for real definitions not hypothetical ones (I suppose they can hypothetically have hypothetical definitions). Can you be more concrete?