Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

Lambda Calculus Semantics

  1. Aug 14, 2010 #1

    disregardthat

    User Avatar
    Science Advisor

    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. jcsd
  3. Aug 14, 2010 #2

    Hurkyl

    User Avatar
    Staff Emeritus
    Science Advisor
    Gold Member

    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.
     
  4. Aug 15, 2010 #3

    disregardthat

    User Avatar
    Science Advisor

    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?
     
  5. Aug 15, 2010 #4
    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 [itex]N \mapsto (M N)[/itex], so we should be able to consider any denotation [itex][M] \in D[/itex] of M as a function [itex]D \to D[/itex].

    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.)
     
  6. Aug 15, 2010 #5

    Hurkyl

    User Avatar
    Staff Emeritus
    Science Advisor
    Gold Member

    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. :frown:

    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, [tex]T^{T\times(T\times T)^T}[/tex], 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.
     
  7. Aug 15, 2010 #6
    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.)
     
  8. Aug 16, 2010 #7

    disregardthat

    User Avatar
    Science Advisor

    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?
     
Know someone interested in this topic? Share this thread via Reddit, Google+, Twitter, or Facebook




Similar Discussions: Lambda Calculus Semantics
  1. Predicate calculus (Replies: 7)

Loading...