Computer Programs and lambda terms without normal form

Question

λ-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?

Answer 1

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".

2. 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).