Understanding the Semantics of Lambda Calculus

[disregardthat]

I do not understand the following extract on the semantics in the wikipedia article on lambda calculus:

The fact that lambda calculus terms act as functions on other lambda calculus terms, and even on themselves, led to questions about the semantics of the lambda calculus. Could a sensible meaning be assigned to lambda calculus terms? The natural semantics was to find a set D isomorphic to the function space D → D, of functions on itself. However, no nontrivial such D can exist, by cardinality constraints because the set of all functions from D into D has greater cardinality than D.

In the 1970s, Dana Scott showed that, if only continuous functions were considered, a set or domain D with the required property could be found, thus providing a model for the lambda calculus.

This work also formed the basis for the denotational semantics of programming languages.

Is D supposed to represent the semantics of the lambda calculus? If so, how? I would really appreciate an explanation of the whole text. They say the set of functions from D into D has greater cardinality than D, but this is not true in constructive mathematics, is it? The functions would only be computable functions, although not recursively enumerable, they are countable, is that not right? Perhaps the fact that they are not recursively enumerable poses the same difficulties as a higher cardinality would.

 

[Hurkyl]

In untyped lambda calculus, any lambda expression denotes just another "object". So if you're looking for an interpretation of the language, the lambda expressions have to map to the domain of your interpretation.

However, the interpretation also provides a way to associate a lambda expression with operators on the domain of your interpretation.


Now, you might ask "but why would we insist that D is isomorphic with D^D?" And I would agree with you; it seems like a somewhat silly thing to do.

But, it's not surprising to me that people might be interested in such things. For example, when interpreting second-order logic, people seem to like insisting on things like the domain of all relations in the interpretation really is the entirety of all set-theoretic relations that can be formed on the domain. Requiring that the domain of lambda expressions include all operators on D seems analogous to me.

 

[disregardthat]

In untyped lambda calculus, any lambda expression denotes just another "object". So if you're looking for an interpretation of the language, the lambda expressions have to map to the domain of your interpretation.

Could you explain what you mean by the domain of an interpretation and what a mapping would be to it? Are you talking of a mathematical set? And is D this domain, or is D the set of objects which can be formed in lambda calculus?

Now, you might ask "but why would we insist that D is isomorphic with D^D?" And I would agree with you; it seems like a somewhat silly thing to do.

I don't understand the relevance of that D must be isomorphic to the set of functions on D, in what way does this affect a possible semantics?

 

[adriank]

D would be the set of denotations [M] of lambda terms M. Presumably two lambda terms that are alpha/beta(/eta?)-equivalent would have the same denotation.

Well, any lambda term M induces a function on lambda terms by application $N \mapsto (M N)$, so we should be able to consider any denotation $[M] \in D$ of M as a function $D \to D$.

Also see http://en.wikipedia.org/wiki/Lambda_calculus#Semantics

(Note: I don't know much about this stuff so I might be completely wrong.)

 

[Hurkyl]

For an ordinary first-order language, an interpretation consists of:

• A set D, the "domain"
• For each constant symbol of the language, an element of D
• For each function symbol of the language, an function on D
• For each relation symbol of the language, a relation on D

Now, what of untyped lambda calculus?

This is what seems like the most obvious way to me to define an model:

As usual, a model is an interpretation, which has a set D, the domain. Any constant term (e.g. λx.x is interpreted as an element of D. Any term with n free variables is interpreted as an n-ary function on D.

Lambda calculus has a binary operator called "application". This is interpreted as a binary function on D.

Finally, lambda calculus has theorems -- e.g. (λx.x)y = y -- and so to be a model, our interpretation must translate these into theorems of set theory. e.g. for any element d of the domain, the interpretation of application applied to the interpretation of λx.x and d must yield d. (I've simplified the previous statement)

I don't understand the relevance of that D must be isomorphic to the set of functions on D, in what way does this affect a possible semantics?

The more I think about it, the less I think I'm able to guess about the specific motives behind that want.

My best guess at the moment is

If we insist on viewing application of lambda terms as function application, the fact lambda calculus is untyped amounts to using T to name the one type, and equating the formal types T and T^T. Model theorists like to insist that if we use the set D as an interpretation T, that we use set D^D as the interpretation of T^T. So, together, this implies D^D and D to be isomorphic.​

Now, typed lambda calculus avoids all these problems entirely. By distinguishing between the types like T, T^T, TxT, $$T^{T\times(T\times T)^T}$$, and so forth, you can insist on the interpretation of T^T being D^D and still have a calculus that is very naturally interpreted into any Cartesian closed category (CCC) -- and the category of sets-and-functions is the prototypical example of such a thing.

 

[adriank]

I should add to my previous post: In general, not every function from D to D need be represented by an element of D. (Consider, for example, non-computable functions.)

 

[disregardthat]

All right, thanks for the useful reply. There are some things I don't understand still. Why do we have to base an interpretation in set-theory? I may be naive, but isn't the semantics just supposed to represent the syntax of lambda calculus? It seems to me not more of a problem than inventing the semantics on the spot. I extremely unfamiliar with this, do you have some online material?