Meta-lambda

Here's something that used to bother me when reading Winskel and learning denotational semantics.

We start with a language like the lambda calculus, and everyone looks at λn.(n+1) and knows that this represents the function that takes an integer and increments it. But that's not enough for us: we have to build up this big, complicated mathematical machinery to determine precisely what this function means; we treat it as dumb syntax and give it a translation to some domain that models it.

But when we're defining the model, we allow ourselves to represent meta-functions simply using the lambda calculus, and suddenly λn.(n+1) just means the set-theoretic function that maps integers to their successors. Why do we have to work so hard to give a precise model for our object language, but when we work with the meta-language, we can just say "you know what I mean"?

The reason is simply that the object language is generally a complex language that's made to look like lambda calculus, but has other features and effects (e.g., recursion and non-termination, mutation, etc.) that can't be modelled in obvious ways and require a precise translation. By contrast, when we work in the model, if it's simply set-theoretic functions, then we can use a simple meta-language based on the lambda calculus to represent these functions. So this meta-lambda calculus is just a convenient shorthand for elements in the domains of the model. As long as there's an obvious translation of such representations into sets, terms in the meta-lambda calculus such as λn.(n+1) can be treated as nothing more than a convenient notation, no different from { (n, n+1) | n ∈ N }.