Lambda the Ultimate

ActorScript(TM): Industrial strength integration of local and nonlocal concurrency for Client-cloud Computing by Carl Hewitt, 2009.

ActorScript is based on a mathematical model of computation that treats “Actors” as the universal primitives of concurrent digital computation [Hewitt, Bishop, and Steiger 1973; Hewitt 1977]. Actors been used both as a framework for a theoretical understanding of concurrency, and as the theoretical basis for several practical implementations of concurrent systems.

I hope I do not need to introduce Carl Hewitt or his Actor model. This paper is a modern attempt to expose that model via a practical PL.

The more papers I read, the more I see the term "higher order" applied to seemingly anything. We have HO (high order) programming, HO programming languages, HO functions, HO modules. Those readily come to mind, although I am confident I can find other applications of HO to other terms in computer science.

So what *is* the exact meaning of "higher order." Does it have one precise definition? Or maybe one broader, generally applicable definition? Or is the term simply misused?

Thanks much.

Scott

Question

What,if anything, prevents the execution of a Haskell term from being a proof in equational logic?

Below are some things thay may impede treating Haskell as a logical system with terms being true equations. Any feedback on these reasons would be welcome. Are they are valid reasons? What is their possible impact? Are there more reason?

--------------------Reason (1)------------------

There are some equations that are not expressible in Haskell e.g. mirror (mirror x) = x . It is not possible at the value level, because Haskell does not support dependent types and thus cannot express the type of the proposition "forall a . forall x:Tree a, mirror (mirror x) = x", and therefore a proof term also cannot be constructed. Another example from Torrini et al discusses specifying order. A partial order that is also linear is called a total order. The class linorder of total orders is specified using the usual total order axioms. They conclude that such axiomatizations are not possible in Haskell.

--------------------Reason (2)------------------

According to Thompson the equations in Miranda (and I assume Haskell) are not pure mathematical equations due to *where* and other reasons. According to Danielsson the fact that they are not always structurally equations does not prevent functional programmers from
using them as if they were valid equations. Danielsson show that this informal *fast and loose* use of equational axioms and theorems is *morally correct*. In particular, it is impossible to transform a terminating program into a looping one. These results justify the informal reasoning that functional programmers use.

Kieburtz states that neither the syntax nor type system discriminate between values and latent computations.
To prove some property of a Haskell program the verification logic must support such distinctions. To address this shortcomming of Haskell Kieburtz has included P-Logic in the Programatica Project to provide a verification logic for Haskell

--------------------Reason (3)------------------

There is no formal specification for the meaning of a Haskell program (i.e. its meaning is not defined in a logic). At the level of precise logical specification and logical interoperability this could be a problem (e.g. semantic web likes logic). This should not be a problem for programming tasks, after all most languages like Java do not have a formal semantic definition in logic (like Maude or CafeOBJ ).