32
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 ...
22
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'...
19
Actually, the approach of the CoC is more expressive -- it permits arbitrary impredicative quantification. For example, the type $\forall a.\; a \to a$ can be instantiated with itself to get $(\forall a.\; a \to a) \to (\forall a.\; a \to a)$, which is not possible with a universe hierarchy.
The reason it is not widely used is because impredicative ...
19
The short answer is yes, MLTT can reasonably be equated with CIC without impredicative Prop.
The main technical issue is that there are dozens of variants when one talks about Martin-Löf Type Theory and, perhaps more surprisingly, when one talks about CIC. For example, taking the version of CIC defined in Benjamin Werner's thesis, it doesn't even make sense ...
11
You are correct, there is an error in that paper, and the rule should indeed read:
$$\frac{\Gamma\vdash M:\Delta}{\Gamma\vdash M\cong M} $$
the use of jugements of this style for equality (sometimes called "typed equality") originates already in Martin-Löf, I think (see here for example). It's often replaced with an untyped operational definition in modern ...
10
I have not seen this in a dependently-typed setting, but a similar notion is fairly well-known in weaker systems (e.g. System F) with subtyping, under the term "F-bounded quantification". This pops up prominently in type systems for object-oriented programming languages, which typically are heavy on (equi-) type recursion. This notion was originally ...
10
One way to show that it is consistent to add cnat_ind is to internalize parametricity, i.e., we extend the type system with enough structure so that it can prove its own parametricity, from which it then follows that the Church encoding of natural numbers does indeed give natural numbers. See for instance the PhD dissertation Internalizing Parametricity by ...
9
I'll compliment Neel's (excellent, as usual) answer with a bit more exposition on why levels are used in practice.
The first important limitation of CoC is that it is trivial! A surprising observation is that there is no type for which you can prove that it has more than one element, much less an infinite number of them. Adding just 2 universes gives you ...
8
I'll summarize the comments from chi, and sketch the proof that
There can be no proof of $\mathrm{False}:=\forall X:*.X$ in the CoC in head normal form. Furthermore, this fact can be proven in a weak theory, say Peano Arithmetic (though the excluded middle is not required).
This fact implies that if the CoC is normalizing, then it is consistent, and ...
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
This is not an answer but a very long comment.
I find the idea quite interesting. To keep things focused, I think it would be very good to have a clear idea of what it means for the encoding of cubical type theory to be correct, namely that it is sound and conservative.
Soundness just means you can encode everything (for instance, that you did not forget to ...
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
Since the CoC has dependent types and system $F$ does not, I'll assume you mean a function whose types is in system $F$, but whose definition can only be written in CoC. Luckily in this case we can restrict to system $F_\omega$, which can express the same non-dependent functions as CoC, by some erasure argument.
In general, a rule of thumb to construct such ...
7
Yes, it's consistent. Probably the easiest account is in my 2013 CSL paper with Derek Dreyer, Internalizing Parametricity in the Extensional Calculus of Construction, which is all about adding this style of parametricity axiom to the CoC.
6
Let $F : \mathsf{Type} \to \mathsf{Type}$ be a type constructor and let $W_F$ be the inductive type defined by $W_F = F W_F$. Not every $F$ has such an inductive types, but this is not important for this discussion.
The starting point of Church's encodings is the observation that $W_F$ ought to be
$$\forall T : \mathsf{Type} \,.\, (F T \to T) \to T.$$
Thus, ...
6
The relationship that you're looking for is indeed well-defined, but IMO it's not quite the right thing to look at. For example:
Type checking for terms in the simply-typed lambda calculus is linear time, but normalizing terms in the STLC exceeds any fixed tower of exponentials (i.e., $O(2^{2^{2^{\ldots n}}})$.
Type checking for System F is linear time, but ...
6
Let us spell out the informal meaning of INat, IntNat and IndNat2. Suppose we have a predicate P on natural numbers. Say that P is inductive if we can inhabit P Zero and ∀ k . P k -> P (Succ k). Then we have:
NatInd P states "if P is inductive then, for all j : Nat, we have P j"
INat n P states "if P is inductive then P n"
NatInd2 P states: "if P is ...
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 ...
5
I found another reference that goes through a detailed proof of the decidability of typechecking for systems of dependent types up to the CIC:
Chapter 2 of Advanced Topics in Types and Programming Languages: Dependent Types, David Aspinall & Martin Hofmann.
As you probably know, the proof of decidability is conditional on decidability of $\beta$-...
5
As Neel points out if you work under the "propositions are types" then you can easily come up with a type whose equality cannot be shown decidable (but it is of course consistent to assume that all types have decidable equality), such as $\mathbb{N} \to \mathbb{N}$.
If we understand "proposition" as a more restricted kind of type, then the answer depends on ...
5
In a system where Type:Type, the typing rule for the product would be trivial:
$$\frac{\Gamma \vdash A:Type\hspace{1cm} \Gamma, x:A \vdash B:Type}
{\Gamma \vdash \forall x\!:\!A.B : Type}$$
Unfortunately, Type:Type is known to be inconsistent, and Type must
inhabit some different sort, say Type:BigType. Then, the following case of the
product ...
5
The definition of an object $X$ is impredicative, if the definition uses a collection $C$ in the construction of $X$, such that $X$ is a member of $C$. So impredicativity is a form of circularity.
We are wary of circular definitions because they are often paradoxical. Fortunately it turns out that not all forms of
circularity are (or appear to be) ...
5
You should use False instead of 1>2 in the conclusion of the theorem. Using indirect ways of denoting an impossible proposition is an unnecessary complication. False is the impossible proposition used in the standard library.
In order to prove that ElProp R1 is uninhabited, you need to prove that ElProp R2 is uninhabited, and vice versa. You need ...
answered May 20 '14 at 19:00
Gilles 'SO- stop being evil'
2,5871 gold badge24 silver badges35 bronze badges
5
Is there a simple algorithm? yes. Simply enumerate all possibilities. Of course this is pretty intractable in practice.
A proper sub-problem of term generation in CoC is "higher-order unification". It handles the simply typed lambda calculus. It is undecidable. But there is a classic practical solution by Huet. There are a lot of resources here: https:/...
5
It's complicated because universe constraints are simplified during inference (in order to avoid an explosion of constraints). Have a look at:
Matthieu Sozeau and Nicolas Tabareau: Universe Polymorphism in Coq, Interactive Theorem Proving - 5th International Conference, ITP 2014
Beta Ziliani & Matthieu Sozeau: A Unification Algorithm for Coq featuring ...
4
Your question is somewhat related to some work I did (sorry for the self-advertisement), where I encode some weak form of dependent type into a Curry-style language (kind of an extension of System F). The idea is to encode the dependent function type $\forall x{\in}A \Rightarrow B$ as $\forall x (x{\in}A \Rightarrow B)$. This encoding relies on first-order ...
4
I think you need induction here to help you show that there is no term like C2 (C1 (C2 (C1 .... I also think you need to strengthen your induction hypothesis, because you don't just need to know that ElProp C1 is uninhabited, but that ElProp C2 is as well.
I proved this using an auxiliary lemma
Theorem excircular_help : forall y, forall x:(ElProp y), y = ...
4
$\text{absurd} : (A : \text{U}) \to 0 \to A$ and $\text{elim} : (A : 0 \to \text{U}) \to (x : 0) \to A\,x$ are equivalent. To go right, use $\text{absurd}\,(A\,x)\,x$. To go left, use $\text{elim}\,(\lambda\,x.\,A)\,x$. Also, both types are propositions because of the $0$-s in domains. There's not much reason to assume or use $\text{elim}$ instead of $\text{...
3
On the face of it, the result you're asking for is a normalization result, as it asserts that every well-typed term of a certain form has a head-normal form (of a certain shape).
However it is legitimate to ask whether your statement is equivalent to normalization of the CC, since you are only asking for head normal forms of a certain sub-class of terms.
...
3
It is rather unusual for the type of x to be allowed to refer to x.
Your proposed typing rules are problematic when they say Γ,x:A ⊢ A:∗ because that relies on a different notion of environment than usual: normally the type of a new element x (i.e. A here) must be closed over the prefix (i.e. Γ here), whereas in your case A can have x as free variable.
[ ...
Only top voted, non community-wiki answers of a minimum length are eligible
