[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Is TLA+ still useful if your implementation language is a purely functional one, like Haskell?

   Why is a (purely) functional program not considered a system?  Does
   system imply state transitioning?

I used the term system incorrectly.  Let's define a property as a
collection of behaviors.  Any property can be specified by a TLA+
formula.  A system is a property in which every step of every behavior
can be considered either a step of the system or a step of its
environment.  A functional system is in which every (non-stuttering)
behavior consists of two steps--an environment step that provides
input to the system followed by a system step that returns an output
to the environment, such that there is a function that maps input
to output.  Such a system can be described by that function.

   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
it clearer.