# Lambda Calculus Semantics

1. Aug 14, 2010

### disregardthat

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

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.

2. Aug 14, 2010

### Hurkyl

Staff Emeritus
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 DD?" 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.

3. Aug 15, 2010

### disregardthat

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?

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?

4. Aug 15, 2010

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

5. Aug 15, 2010

### Hurkyl

Staff Emeritus
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)

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 TT. Model theorists like to insist that if we use the set D as an interpretation T, that we use set DD as the interpretation of TT. So, together, this implies DD and D to be isomorphic.​

Now, typed lambda calculus avoids all these problems entirely. By distinguishing between the types like T, TT, TxT, $$T^{T\times(T\times T)^T}$$, and so forth, you can insist on the interpretation of TT being DD 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.

6. Aug 15, 2010