3
$\begingroup$

So I think I somewhat understand the type theory of the various lambda calculi in the lambda cube, from the simply typed lambda calculus to the calculus of constructions, but looking at it I'm wondering if I really need lambda abstraction to use it. I understand that you can use these lambda operators to construct quantifiers, logical connectives, and the like. But do we need them or can we just use type construction on its own and create quantifiers and operators that work on terms that return a propositional type, using ordinary classical logic?

This seems more straightforward for me coming from my familiarity with logic over lambda calculus, and the logic constructed with lambda calculus seems a bit unnatural, along with it being weaker than classical logic.

Question:

Can I dispense with lambda abstraction in type theory, and what do I lose by doing that?

$\endgroup$
8
  • 1
    $\begingroup$ Without lambda abstraction, how do you create a term of function type? $\endgroup$
    – Zhen Lin
    Commented Feb 13, 2015 at 20:07
  • $\begingroup$ With the function type constructor. Without lambda abstraction I can't create anonymous functions, but I'm not quite sure I need those... $\endgroup$
    – dezakin
    Commented Feb 13, 2015 at 20:21
  • 1
    $\begingroup$ Why is it more straightforward to work in a context where functions are not first-class citizens? $\endgroup$
    – Rob Arthan
    Commented Feb 13, 2015 at 20:48
  • 3
    $\begingroup$ The function type constructor produces a type. I am asking you about terms of function type. $\endgroup$
    – Zhen Lin
    Commented Feb 13, 2015 at 21:00
  • 1
    $\begingroup$ I thought completeness depended on the semantics; We assume general semantics and it's complete. It's not obvious to me that practical implementations are simpler or less tedious with the unity of terms and propositions from my initial attempt of a HOL prover, though I trust your expertise enough to give it a second look; With propositions I only care about rules and entailment, and terms it's unification. We may be talking about different things, because lambda binding looks to mostly be about creating anonymous functions which at first look seems unnecessary if you have a Herbrand universe. $\endgroup$
    – dezakin
    Commented Feb 14, 2015 at 1:33

2 Answers 2

6
$\begingroup$

Unlike set theory, where sets taken as the most fundamental objects, type theory takes functions as the first-class mathematical objects. Then we obviously need something like a function type to work on. But how to construct inhabitants of this type? By $\lambda$-abstraction, which is what we call the function type constructor.

Let $b$ be an inhabitant of a type $B$ under the assumption that $x$ is an inhabitant of $A$, that is

$x : A \vdash b : B$

Then we can construct an inhabitant of the function type $A \to B$ by $\lambda$-abstraction on $b$:

$\vdash \lambda x.b: A\rightarrow B$

You ask what you lose if you remove $\lambda$-abstraction. The straightforward answer is that you can no longer construct elements of the function type. Since there is no such thing as a free lunch, we would have to replace it with something else.

One of the most remarkable alternatives is the notion of a combinator from combinatory logic. It eliminates the need of bound variables by using primitive high-order functions called combinators, some of which are

$$I : A \to A $$ $$K : A \to (B \to A) $$ $$S : (A \to (B \to C)) \to (A \to B) \to (A \to C) $$

for any types $A, B, C$.

Now rather than using lambda-abstraction, functions are constructed out of combinators. But note that the notion of $\lambda$-abstraction is still here under the hood. In particular,

$$I := \lambda x. x$$ $$K := \lambda x.\lambda y. x$$ $$S := \lambda f. \lambda g. \lambda x. (f x) (g x) $$

$\endgroup$
1
$\begingroup$

I think what you're after is, instead of having the following statement:

$(\lambda x \colon t_{dom}.e) \colon (\Pi x \colon t_{dom}. t_{cod})$

we have this one?

$(\lambda x \colon t_{dom}.e \colon t_{cod}) \colon (\lambda x \colon t_{dom}. t_{cod})$

It actually seems like it would almost be more consistent for me...

$\endgroup$
0

You must log in to answer this question.

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