Questions tagged [lambda-calculus]
λ-calculus is a formal system for function definition, function application and recursion which forms the mathematical basis of functional programming.
609 questions
- Bountied 0
- Unanswered
- Frequent
- Score
- Trending
- Week
- Month
- Unanswered (my tags)
1
vote
1
answer
78
views
solution feedback (lambda calculus, type theory, free variables)
I am uncertain about my solution to exercise 6.11(c) from Type Theory and Formal Proof (Nederpelt).
Let $Γ ⊢M : N$ in λC and $Γ ≡ x_1 : A_1,...,x_n : A_n$.
(c) Prove that $FV(A_i) ⊆ \{x_1,...,x_{i−1}\...
0
votes
0
answers
20
views
Finding minimal subsystem of λ-cube - different answer to author's solution
A part of Exercise 6.8 of Type Theory & Formal Proof (Nederpelt) requires me to identify all the $\Pi$-types on the derivation of the inhabitant of the following expression:
$$N ≡ [Πα : *. ((Πx : ...
2
votes
1
answer
175
views
Why does lambda calculus have clear semantics, easy comprehensibility, and serve as a foundation for proof languages?
I'm worried that my question might be ill-posed, but I've tried to formulate it as precisely as possible.
As a computational model, lambda calculus has numerous alternatives, including Turing machines....
0
votes
0
answers
34
views
working out sub-system of λ-cube for non-trivial ∏-types
To establish which of the 8 subsystems of the λ-cube an expression belongs to, we consider each ∏-type in that expression, and use the following table to find which systems support that type.
The $s_1,...
0
votes
0
answers
59
views
typing a λC term - error in author's solution or my error?
As part of exercise 6.6 in Type Theory and Formal Proof, I need to find the type of the following term:
$$λS : *. λP : S →*. λx : S. (P x →⊥)$$
where $\bot \equiv \Pi \alpha:*.\alpha$.
My solution ...
0
votes
0
answers
27
views
logical interpretation of λC type $(S \to S \to *) \to S \to *$
Exercise 6.5 of Type Theory and Formal Proof (Nederpelt) asks us to interpret logically the following judgement:
$$ S : * \quad \vdash \quad \lambda Q : S \to S \to *. \lambda x : S. Qxx \quad : \...
0
votes
0
answers
30
views
logical interpretation of a λP type about reflexivity and asymmetry
Exercise 6.4 of Type Theory and Formal Proof (Nederpelt) asks us to derive the following type, and also derive an inhabitant, in the context $Γ ≡S : *, Q : S →S →*$
$$(Πx,y : S. (Qxy → Qyx → ⊥)) → Πz :...
0
votes
0
answers
67
views
Syntax of $\eta$-longest $\beta$-normal form
In Church-style STLC, the syntax of typed $\beta$-normal form is:
Then, I am wondering how to define $\eta$-longest $\beta$-normal form inductively.
0
votes
0
answers
37
views
struggling to find an inhabitant of a λP type (limited scope of variables)
I'm doing exercise 6.2 from Type Theory and Formal Proof.
Exercise 6.2
Let $Γ ≡S : ∗, P : S →∗, A : ∗$.
Prove by means of a flag derivation that the following expression is inhabited in λC with ...
0
votes
0
answers
39
views
solution feedback: which of the 8 λ-cube systems do $\bot$ and $\bot \to \bot$ belong to?
Chapter 6 of Type Theory and Formal Proof introduces the λ-cube with its 8 systems, differential primarily by how their (form) rules work, summarised in the table below.
Question: I am a little ...
0
votes
1
answer
40
views
Coinductive combinatory and lambda reduction systems
SK combinators and the lambda-calculus are inductively-defined reduction systems. A nice online lambda-calculus interpreter is at https://lambdacalc.dev/
Question: what happens if instead of ...
0
votes
1
answer
96
views
Logical proposition corresponding to the λP type $\Pi x:S.*$?
I'm continuing to work through Chapter 5 of Type Theory and Formal Proof (Nederpelt).
Doing exercise 5.10 I've run into a wall.
I know there is a correspondence between λP types and logical ...
1
vote
1
answer
52
views
Why are λP $\Pi$-types written as $\Pi x:A.B$ and not $\Pi A.B$?
I'm working through Type Theory and Formal Proof Chapter 5 which is on λP.
Question: Why are $\Pi$-types written as
$$\Pi x:A.B$$
and not
$$\Pi A.B$$
As I understand it, the important information is $...
1
vote
2
answers
167
views
Church numerals subtraction, more efficiently
Googling for "efficient subtraction on Church numbers" brings back the usual repeated predecessor stuff, $\lambda mn. n\ \text{pred}\ m$. So, nothing efficient.
In fact, it is monstrously ...
1
vote
0
answers
50
views
can't find inhabitant of $ \Pi z:A . (\Pi y:(\Pi x:A.B).B) $ in λP
I'm doing ex 5.5 from Type Theory and Formal Proof. Chapter 5 introduces λP, typed dependent on terms, and also the minimal predicate logical equivalents of types.
Ex 5.5 Prove that $A ⇒ ((A ⇒ B) ⇒ B)...