[Solved]: Quantifiers in lambda calculus

Problem Detail: 

I'm learning lambda calculus, however I'm quite confused about the quantifiers in lambda calculus. As far as I know, quantifiers such as "∃" are concepts of first order logic (FOL), which are not needed by lambda calculus. Moreover, I didn't find anything about quantifiers in any tutorials I have read.

However, I find this paper (Lambda Dependency-Based Compositional Semantics), in the first page of which the author used quantifier in lambda calculus.

So, are quantifiers used in lambda calculus? If so, what do they mean? Is it the same as in FOL?

Precisely, what does "∃" mean in the following lambda calculus?

λx.∃e.PlacesLived(x, e) ∧ Location(e, Seattle) 

Asked By : Zhao

Answered By : chi

It appears that the author is using lambda notation for sets and relations. That is, sets are represented as boolean-valued unary functions, and relations are represented as boolean-valued binary (or k-ary) functions. In other words, we work with the sets/relations' characteristic functions instead, with no loss of generality.

For instance $\{n | n\geq 5\}$ is written as $\lambda n.\ n\geq 5$ where "$n\geq 5$" must be understood as the boolean $\sf true$ or $\sf false$, depending on the value of $n$.

The existential expression $\exists x.\ p(x)$ must be understood similarly: it "evaluates" to true iff there is some value of $x$ which satisfies $p$.

Also, note that, in the theory of typed lambda calculi, we do have some powerful type systems which allow $\forall/\exists$ to appear. For instance the second-order lambda calculus $\lambda 2$ (AKA System F) allows universals in types. In the very powerful Calculus of Constructions we can indeed write things such as $\lambda x:\tau.\ \exists y:\sigma.\ p x y$ which is a function of type $\tau \rightarrow *$. It takes a value of type $\tau$, and returns an existential type.

You do not need this theory for the paper you mention, though.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/64824

 Ask a Question

 Download Related Notes/Documents