28
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 starting at Martin-Löf type theory with universes,
and then adding a sort Prop at the bottom of the type hierarchy. This
is a very different beast than the ...
21
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. The Coq interactive theorem prover is based on an underlying type theory, sometimes lovingly called the calculus of inductive constructions with universes. You'...
21
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 logic.
The proof generally proceeds by assuming you have a term $\mathrm{absurd}$ of type $\mathrm{False}$, using subject reduction to get a normal form, and ...
19
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, $\mathsf{Str}$ for binary strings, $\mathsf{Bool}$ for Booleans) and wonder what is the complexity of the functions/problems representable/decidable by typed terms. ...
18
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 that the logic derived from this calculus was inconsistent (because non-terminating programs existed). Eventually Church developed the simple theory of types ...
12
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$-calculus is
$$\frac{\Gamma \vdash e : \bot}{\Gamma \vdash \mathtt{absurd}_A(e) : A}.$$
(We call $\mathtt{absurd}_A$ an eliminator.)
Thus, the term of type $\bot ...
12
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 equality and natural numbers), higher order types or both. In these calculi, types are powerful but terms can't access this power, so I don't know what you get.
...
11
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 axioms and $\beta$-reduction rules. Thus strictly speaking the system is not an LPTS; it is merely something much like one.
Consider the calculus of constructions (...
11
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 $\iota$ as the base type of numbers ans $\omicron$ as the base type of propositions, you can add the constants
$$ \forall_\tau:(\tau\rightarrow \omicron)\...
9
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 things work out all right when type-checking in a "standard" dependent type theory (I'll be deliberately vague, since these issues tend to crop up ...
8
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, your derivation works regardless of the type of the answer -- the very same term you have works for $\mu a.\; a \to X$ for any $X$.
This is known as Curry's ...
8
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 of constructions, namely Gödel's System T (simply typed $\lambda$-calculus, natural numbers, and primitive recursion on them), so the argument applies to a ...
8
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 $2^{\vdots^{2^{|S|+|T|}}}$ for a tower of exponentials of fixed height may decide whether two simply-typed terms $S$ and $T$ are $\beta$-equivalent.
The ...
7
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 sense: given the reduction
$$(\lambda x:T.C\ x\ x)\ u\rightarrow_\beta C\ u\ u $$
it is clear that the occurrences of the term $u$ can be shared in memory, and ...
7
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 fst(e) and snd(e)), there are no basically issues whatsoever. The reason it took so long to figure out is because it turns out to be more natural to do eta expansions rather than eta ...
7
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 realizers for 2nd order Heyting arithmetic $\mathrm{HA}_2$. The informal theorem can be stated as follows
If the terms of a typed calculus $\cal{T}$ are the ...
7
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:
coe : ∀{i}{A B : Set i} → A ≡ B → A → B
HEq : ∀ {i}{A B : Set i} → A → B → Set _
HEq {_}{A} {B} x y = Σ (A ≡ B) λ p → coe p x ≡ y
To do anything with HEq, it is enough to consider J and K for ...
6
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 you can't provide a proof of it.
Even more simply, consider the empty type $0$. It has no canonical forms at all, but there's nothing stopping you from assuming ...
6
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$ reduces to a hypothetico-general judgment.
In practice, the way that you implement this kind of type theory is by formalizing rules for hypothetico-general equality &...
6
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 Judgments: Automatically Generating
Well-Typed Terms from the Definition of a Type-System
to the more theoretical
Grygiel & Lescanne, Counting and generating ...
6
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 (= polynomials with if-then-else), see (1). Other notions of equality change this. (2) shows that using $\beta\eta$-equality leads to a larger class of definable ...
6
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 if it there were an algorithm computing it. In fact, most programs you write in the $\lambda$-calculus (or whatever calculus of the $\lambda$-cube) are already ...
6
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 fit. It is not that restrictive in the sense that usually a checkable term together with a type annotation gives you an inferrable term. This embedding is ...
6
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 theorem is only true for substituting synthesizing terms for variables.
Indeed, if you introduce separate grammatical classes for synthesizing and checking terms, ...
6
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 detail.
I'm not sure I understand the gist of your confusion, but I think one important thing to note, is the following lemma (Corollary 5.2.14), proven in the ...
6
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 "natural" recursion principles on Scott numerals, and because they correspond to recursors in this encoding, they are guaranteed to terminate.
However, if you want ...
5
It is an interesting problem to figure out what bothers the OP. First of all, it is not at all the case that the equation put forward by the OP says "different computations have the same value". For instance, the computations
do _ <- putStr "foo"
return 42
and
do _ <- putStr "bar"
return 42
both "have" value 42 but are different, since one ...
5
There hasn't been a huge amount of work in this space, but what work there is, is pretty interesting.
Torben Mogensen has worked on this problem. Here are two papers of his.
The first paper gives an algorithm for first-order functional programs, and the second extends it to higher-order. The precise characterization of when this algorithm will succeed is ...
5
As Andrej notes, $\lambda\Pi$ is a conservative extension of first-order logic which means:
Adding the axioms of PA to $\lambda\Pi$ gives exactly the same arithmetic theorems as PA.
However, because of the more expressive system, it is possible to finitely axiomatize induction using the following (encoding of) this axiom:
$$ \forall P: {\mathbb N}\...
4
At least the problem of whether 2 terms are equal modulo the theory of Cartesian Closed Categories (or $\beta\eta$ conversion) is decidable, because (in part) of the normalization property.
Another, more categorical way to see this is by extracting a conversion algorithm through normalization by evaluation which gives decision procedures for equality in ...
Only top voted, non community-wiki answers of a minimum length are eligible
