Why is a (purely) functional program not considered a system? Does
system imply state transitioning?
Why is a (purely) functional program not considered a system?
Does system imply state transitioning?
A program is something that gets executed on a computer. A program
can be described as a state machine--something specified by a TLA
formula Init /\ [Next]_vars. A functional language is a particular
way of writing programs. A purely functional language, which can
implement only functional specifications, allows a lot of freedom to a
compiler--arguments can be evaluated in arbitrary order, it can
perform common subexpression elimination, etc. This means that
- It is probably inconvenient to describe the meaning of
such a program as a state machine.
- Different compilers can translate the same purely functional
program into code with very different computational complexity.
Those two observations are not unrelated.
one can wrap a pure function interface over an imperative
An algorithm is a collection of behaviors. I presume by an imperative
algorithm you mean one described in an imperative language, or as
a TLA formula Init /\ [Next]_vars. I don't know what it means to
wrap an interface over an algorithm. Perhaps you mean that the algorithm
can implement a functional property. In TLA, that means that the
specification obtained from Init /\ [Next]_vars by hiding all
the variables except those that describe the communication between
the system and its environment--the specification written
\EE some_vars : Init /\ [Next]_vars
implies the functional specification (the one the allows behaviors with
those two non-stuttering steps).
What all this boils down to is that functional programs (ones that
just compute a function) are a particular subclass of systems. Since
all systems can be described in TLA by temporal formulas, this
subclass can as well. However, that doesn't mean that it's a useful
way of describing that subclass.
I'm sorry if this is incoherent, I don't have time to try to make