1
$\begingroup$

λ-calculus an ideal mathematical model in which to interpret programs. A program can be interpreted as a lambda term, and the term can have or not have a normal form. What role the terms without normal form play when analyzing programs?

$\endgroup$
  • $\begingroup$ Welcome to SE Computer Science. Since you are a new user I should tell you that crossposting on two sites is not well regarded, as it often causes duplication of work. You should try one, then possibly have your question migrated if unsatisfied, or post it in different words later on another site, Crosspost: math.stackexchange.com/questions/1302419 $\endgroup$ – babou May 28 '15 at 14:08
  • $\begingroup$ I'm not so sure about the "ideal" part of your question. $\endgroup$ – Andrej Bauer May 29 '15 at 6:14
  • $\begingroup$ @AndrejBauer Well, "ideal" does not necessarily means best, it may also mean abstracted, referring to the concept rather than "impure" instances of the concept, such as opposing the ideal square (mathematics) to a square made of cardboard, or drawn on paper. A platonician view. - - - - => Andrej Bauer : Can we meet on chat? $\endgroup$ – babou May 29 '15 at 9:43
  • $\begingroup$ Oh I see, I misread then. $\endgroup$ – Andrej Bauer May 29 '15 at 20:21
4
$\begingroup$

A troublesome one unfortunately. When one goes to examine programs there are two main ways to do it

  1. Operationally

This is the sort of obvious approach to analysing a program in the lambda calculus. We give a set of rules for what it means for one program to step to another and then go on to prove things about programs stepping. Here a step is one small tweak to the program. We continue to step until we end up at a value at which point no more steps are applicable. A value in the lambda calculus is just a lambda term.

Now the obvious impact of nontermination is that for any term there is no guarantee that there is a finite number of steps leading it to a value. We can prove useful theorems like "Either a term is a value or there is an applicable step" (a form of type safety) and "A term can only step to at most one unique value" (a corollary of the Church Rosser Theorem). These are all still useful results that justify statements like "there are unequal lambda terms".

  1. Denotationally

Here we're trying to understand the lambda calculus by mapping each term to a particular mathematical object so that the mapping is coherent in some way. Mostly we want it so that $denote(e) = denote(e')$ if and only if $e = e'$. With this theorem in hand we can go on and prove things in the denotation equal and actually generate useful theorems about the lambda calculus.

Here nontermination causes some real pain. We can't just treat lambdas as "normal" math functions because normal math functions terminate. Instead we explicitly model nontermination by dedicating a specific element in our mathematical collection as what nonterminating programs denote to. Then we go on and prove a theorem along the lines that if $denote(e)$ gives that nonterminating object, then $e$ doesn't run to a value (runs to in the sense of operational semantics).

However the lambda calculus is a pain to denote for a much more fundamental reason though: recursion. The nontermination in the lambda calculus emanates from the fact that the lambda calculus is built on top of this sort of cyclical definition: a lambda term is a function from $A \to A$ where $A = A \to A$. This recursive definition gives us self-application eg $\lambda x. x\ x$ which gives us nontermination.

Building a denotation involves building a collection where $$A \cong A \to A$$ which is just absurd if $A$ is a set and $A \to A$ is the normal collection of set-theoretic functions!

Indeed proving that such an $A$ exists was the impetus for a large field in programming language semantics called "domain theory". Dana Scott constructed such an $A$ by cleverly defining $A$ with an ordering relation on it and restricting functions to be continuous with respect to that ordering operation. Even with this the proof is very technical (and cool).

$\endgroup$
  • $\begingroup$ Does anyone have a reference for that original paper on domain theory btw? I've seen it referenced a few times (including in the paper I'm procrastinating reading now) but a link eludes me. $\endgroup$ – jozefg May 29 '15 at 5:17
  • $\begingroup$ Dana S. Scott, Continuous lattices, Springer LNM 274, pp. 97–136. $\endgroup$ – Andrej Bauer May 29 '15 at 6:16
  • $\begingroup$ Scott's "Outline of a Mathematical Theory of Computation" (1970) is a great introduction as it is mathematically fairly simple and nicely motivates the concepts. Several copies on the web as Oxford report or as conference proceedings - - - - BTW I have been looking for a while to find a copy of Dana Scott's handwritten lecture notes for a course he gave in Amsterdam in the early seventies. I do have some chapters, but not the whole thing. Any help would be welcome. CC @AndrejBauer $\endgroup$ – babou May 29 '15 at 9:56
  • $\begingroup$ I think that Church-Rosser property is not exactly what you say (unicity of value). That is rather a consequence, when there is a value. The issue is that stepping is possible in many way (not sure whether non-deterministic is the appropriate word here), then Church-Rosser says that if A can step one way to B and another way to C, then there is a D such that both B and C can step to D. Your statement is equivalent only when there is a value, a normal form. But the property holds also when there is none. Just for the sake of precision. Nice answer. $\endgroup$ – babou May 29 '15 at 10:17
  • $\begingroup$ @babou You are completely correct, I think "a corollary of the Church Rosser Theorem" clears it up. Thanks! $\endgroup$ – jozefg May 29 '15 at 15:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.