7
$\begingroup$

I just started reading "The calculi of lambda conversion" by Church.

Church defines functions like: id x = x, and says the domain and range are understood to be as permissible as possible. Permitting even itself, id id = id

In my experience, I've always been told to specify a domain and range with the functions I've defined. And they are usually relatively limited, in contrast to id.

This is the first time I've seen functions with a domain and range this large. Are there uses for functions with wide domains and ranges in mathematical contexts other then logic or lambda calculus?

Improve this question
$\endgroup$
2
  • $\begingroup$ Did the edit help? $\endgroup$
    – Polymer
    Commented Dec 10, 2016 at 4:29
  • $\begingroup$ Yes. That's much clearer. $\endgroup$
    – Willie Wong
    Commented Dec 10, 2016 at 21:04

3 Answers 3

Reset to default
8
$\begingroup$

The question you are trying to ask is "What is a denotational semantics for the untyped lambda calculus?"

This is a difficult problem because, as Bjorn Kjos-Hanssen said in his answer, if you try and make variables range over elements of some set $D$ you find that you must have $D \times D \cong D$ and $D^D \cong D$. Unfortunately this implies that $D$ is the singleton set and all lambda terms must represent the same function.

Dana Scott solved the problem of giving a denotational semantics to the untyped calculus with the invention of domain theory.

Improve this answer
$\endgroup$
8
  • $\begingroup$ So if I understand this answer correctly. Untyped lambda calculus is deceptively complicated. The lambda terms are "really" continuous functions of some odd space. Is that correct? $\endgroup$
    – Polymer
    Commented Dec 10, 2016 at 19:46
  • 1
    $\begingroup$ I think you need to be more careful about the distinction between a language and a semantics for that language. Lambda terms aren't anything but strings of symbols obeying a certain grammar and rewriting rules. One may attempt to associate mathematical objects to lambda terms (give a denotational semantics) but there are many ways to this. $\endgroup$
    – Justin Hilburn
    Commented Dec 10, 2016 at 21:46
  • $\begingroup$ As you said, one way of doing this makes lambda terms into elements of a domain. $\endgroup$
    – Justin Hilburn
    Commented Dec 10, 2016 at 21:47
  • 4
    $\begingroup$ It is just like how there are many different models of the theory of groups, i.e., particular groups. It doesn't make sense to say that an element of a group is "really" a matrix even though that might be true in a particular model. $\endgroup$
    – Justin Hilburn
    Commented Dec 10, 2016 at 21:58
  • 2
    $\begingroup$ If you are just trying to connect programming languages and mathematics I would learn the typed lambda calculus and look at mathoverflow.net/questions/903/… $\endgroup$
    – Justin Hilburn
    Commented Dec 11, 2016 at 0:05
2
$\begingroup$

In the standard set theoretical setup, a function cannot have itself as an input. This is because the rank of the function is strictly larger than that of its inputs and outputs.

https://en.m.wikipedia.org/wiki/Von_Neumann_universe

So when they say id(id)=id, it is meant in a more algebraic sense where composition is really just a kind of multiplication or binary operation.

Improve this answer
$\endgroup$
3
  • $\begingroup$ So id is weird. To verify your thought, I define an "application" function $id \times x = x$. Now $id \times id = id$, and we can use it $(id \times id) \times 2 = 2$. No more functions "calling themselves". I'm still confused why I haven't seen something like this sooner. Would studying ZFC closer clarify why functions calling themselves is strange? If I wanted to use this in some mathematical context, what problems might come up? $\endgroup$
    – Polymer
    Commented Dec 10, 2016 at 16:36
  • $\begingroup$ @Polymer well, functions can still "call themselves" in a different sense, like say $f(n+1):=2^{f(n)}$. $\endgroup$
    – Bjørn Kjos-Hanssen
    Commented Dec 10, 2016 at 16:51
  • 4
    $\begingroup$ @Polymer I guess you can try to get into Russell's paradox-like trouble like this: if you define $f(g)=1$ if $g(g)=0$, and $f(g)=0$ if $g(g)=1$, then what is $f(f)$? $\endgroup$
    – Bjørn Kjos-Hanssen
    Commented Dec 10, 2016 at 16:55
1
$\begingroup$

First, these are not functions. These are lambda expressions that can be artistically interpreted as functions. If you want to model lambda theory in a theory where functions are a part of the discourse, it's a different story. As it was told above, one solution is to model lambda in Set Theory. Sets have functions defined, so lambda expressions would be represented as functions. The problem is, of course, that it's impossible to model without tricks. The solution was provided by Dana Scott in the '60s. See, e.g., http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf or watch him at LambdaConf, https://www.youtube.com/watch?v=mBjhDyHFqJY&t=2s

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .