I know about the concept of the "model" of a logical proposition in the context of mathematical logic: It is a mathematical structure in which that proposition is true.

However, it's not clear to me what a "model" of lambda calculus is. Wikipedia states the following:

To formulate such a denotational semantics, one might first try to construct a model for the lambda calculus, in which a genuine (total) function is associated with each lambda term. Such a model would formalize a link between the lambda calculus as a purely syntactic system and the lambda calculus as a notational system for manipulating concrete mathematical functions. The combinator calculus is such a model.

What confuses me about this statement is that it seems to me that the combinator calculus (i.e. combinatory logic) is on the same footing as lambda calculus, in the sense of being a model of computation. It's unclear to me why lambda calculus would be considered a "syntactic" entity while the combinator calculus is a "semantic" entity. I am generally confused by this article.

So what exactly does it mean for something to be a "model of lambda calculus"?

  • $\begingroup$ Forget about that Wikipedia paragraph, I've worked with models of the λ-calculus and I can't make sense of it either. $\endgroup$ Commented Nov 5, 2022 at 0:30


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.