35
votes
Accepted
How do you get the Calculus of Constructions from the other points in the Lambda Cube?
First, to reiterate one of cody's points, the Calculus of Inductive Constructions (which Coq's kernel is
based on) is very different from the Calculus of Constructions. It is
best thought of as ...
- 31.6k
22
votes
How do you get the Calculus of Constructions from the other points in the Lambda Cube?
I've often wanted to try and summarize each dimension of the $\lambda$-cube and what they represent, so I'll give this one a shot.
But first, one should probably try to dis-entangle various issues. ...
- 13.2k
21
votes
Is there a typed lambda calculus which is consistent and Turing complete?
Alright I'll give a crack at it: In general for a given type system $T$, the following is true:
If all well-type terms in the calculus $T$ are normalizing, then $T$ is consistent when viewed as a ...
- 13.2k
21
votes
Accepted
Can typed lambda calculi express *all* algorithms below a given complexity?
I will give a partial answer, I hope others will fill in the blanks.
In typed $\lambda$-calculi, one may give a type to usual representations of data ($\mathsf{Nat}$ for Church (unary) integers, $\...
- 4,823
19
votes
Accepted
Historic Relationship between Typed Lambda Calculus and Lisp?
First, your friend is wrong about the history of the $\lambda$-calculus. Church created the untyped calculus first, which he intended as a foundation for mathematics. Fairly quickly, it was discovered ...
- 1,887
13
votes
Can typed lambda calculi express *all* algorithms below a given complexity?
An answer to a question Damiano raised in his excellent answer:
I am much more ignorant regarding the calculi obtained by just enabling dependent types (essentially Martin-Löf type theory without ...
- 31.6k
12
votes
Accepted
What is a term of the type $\bot\rightarrow A$?
There are several ways of writing such a term, depending on how we write the proof terms for the elimination rule for $\bot$, which is
$$\frac{\quad\bot\quad}{A}$$
The corresponding rule in $\lambda$-...
- 26.6k
11
votes
Is there a typed lambda calculus which is consistent and Turing complete?
Here is an answer to a variant of @cody's precisification of my question. There is a consistent LPTS which is Turing complete in roughly @cody's sense, if we allow the introduction of additional ...
- 461
11
votes
Accepted
Simply typed lambda calculus and higher order logic
The distinction is this: if STLC is taken as a primitive language at the type-level adding constructors and a small number of axioms is sufficient to give you the full expressive power of HOL.
Taking ...
- 13.2k
11
votes
Accepted
Is there an efficient beta-equivalence algorithm?
The answer is no. An old theorem of Statman states that $\beta$-equivalence in the simply-typed $\lambda$-calculus is not elementary recursive, that is, no algorithm whose running time is bounded by $...
- 4,823
9
votes
Accepted
Proof techniques for showing that dependent type checking is decidable
There is indeed a subtlety here, though things work out nicely in the case of type checking. I'll write down the issue here, since it seems to come up in many related threads, and try to explain why ...
- 13.2k
9
votes
Accepted
Recursive types and the empty type
First, note that nothing turns on the presence or absence of the empty type: if you have a nonlinear calculus with function types and unrestricted recursive types, then it is inconsistent. Indeed, ...
- 31.6k
8
votes
Can typed lambda calculi express *all* algorithms below a given complexity?
I'll try to complement Damiano's excellent answer.
In general a typed $\lambda$-calculus can be used as a language of realizers for a certain logic. In particular system $F$ is a language of ...
- 13.2k
8
votes
Accepted
Calculus of Constructions: compress expression to its smallest form
There's a bit of freedom in what we considre "the same value". Let me show that there is no such algorithm if "the same value" means "observationally equivalent". I will use a fragment of the Calculus ...
- 26.6k
7
votes
Calculus of Constructions: compress expression to its smallest form
As Andrej has said, the problem is undecidable if you allow replacing one term by another, extensionally equal one. However, you might be interested in optimal sharing of expressions, in the following ...
- 13.2k
7
votes
Eta expansion in the pattern lambda calculus
This is not a complete answer; it is a comment that got too large.
If you extend typed lambda calculus with products with projective eliminators (ie, product eliminators ...
- 31.6k
7
votes
Typing of substitution in a bidirectional type system
One solution is indeed to restrict to substituting with synthesizing expressions. You can only hope to replace variables with terms of the same mode (i.e. inferrable terms), anything else just won't ...
- 636
7
votes
Accepted
Typing of substitution in a bidirectional type system
The key observation is that whether the substitution theorem holds, depends on the definition of substitution.
For the usual definition of substitution of terms for variables, the substitution ...
- 31.6k
7
votes
Accepted
Understanding the Proof of Strong Normalization of the Calculus of Constructions
Unfortunately, I'm not sure there are more beginner friendly resources than Geuvers' account. You might try this note from Chris Casinghino which gives an account of several proofs in excruciating ...
- 13.2k
7
votes
Accepted
Structural equality of Pi Types with heterogeneous equality?
I am not aware that J or K exists for heterogeneous equality. It does not need an elimination principle, because it can be simply defined as a sigma type:
...
- 1,349
7
votes
Accepted
Are there strongly normalizing lambda terms that cannot be given a System F type?
As you found out yourself, the answer to your question is yes. You found a rather convoluted example, a much simpler example is the following:
$$(\lambda zy.y(zI)(zK))(\lambda x.xx)$$
where $I$ and $...
- 4,823
6
votes
What is a canonical term of $\text{Id}_A(x,y)$ if $x$ is not jugdmentally identical to $y$?
Yes, in general $\mathrm{Id}_{A}(x, y)$ will not have a canonical form. Consider the case when $x$ and $y$ are distinct free variables -- obviously you can postulate that $x$ and $y$ are equal, but ...
- 31.6k
6
votes
Type checking, Hypothetical judgments, meaning explanations and computational type theory
Part of the problem is we cannot say that we have a checker for categorical judgments, because these often reduce to hypothetical judgments. For instance, the categorical judgment $M\in A\to B$ ...
6
votes
Accepted
Enumerating all simply typed lambda terms of a given type
This question has been considered several times in the academic community, from the practical:
Yakushev & Jeuring, Enumerating Well-Typed Terms Generically
Fetsher & al, Making Random ...
- 13.2k
6
votes
Accepted
Is simply typed lambda calculus equivalent to primitive recursive functions
The simply-typed λ-calculus with β-equality at type (o → o) → o → o (which can be seen as type of the natural numbers, whenever o is any base type) can define exactly the extended polynomials (= ...
- 10.3k
6
votes
Calculus of Constructions: compress expression to its smallest form
Let me insist on the viewpoint touched upon by cody's answer.
As far a see it, the question of finding a smallest $\lambda$-term equivalent to another $\lambda$-term is not really interesting, even ...
- 4,823
6
votes
Accepted
Termination checking for Scott-encodings in System F with positive-recursive types
I'll first point you to Types for the Scott Numerals by Plotkin, Cardelli and Abadi, where they show how to encode Scott numerals in plain old system F. This at least shows that you can write the "...
- 13.2k
6
votes
Is there an efficient beta-equivalence algorithm?
I'd like to point out that if:
the terms $M$ and $N$ are strongly normalizing (as the question allows), and
one considers the complexity as depending also on the number $k_M$ and $k_N$ of beta-steps ...
6
votes
Accepted
Complexity of type inference in the simply typed lambda calculus
Type inference for simply typed lambda calculus is complete for polynomial time, as elegantly explained in section 1 of Harry Mairson's Linear lambda calculus and PTIME-completeness.
To be a bit more ...
- 4,309
6
votes
Model of MLTT with $\eta$ rule where function extensionality fails
The simplest one that I know about is the $\text{Set}$-based polynomial model ("container" model). Here, every context is interpreted as a family of sets, i.e. a $Q : \text{Set}$ together ...
- 1,349
Only top scored, non community-wiki answers of a minimum length are eligible