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.1k
20
votes
Accepted
Is MLTT effectively pCiC without Prop?
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 ...
- 13.1k
19
votes
Accepted
Why an infinite type hierarchy?
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 ...
- 31.6k
11
votes
Accepted
Typo in the calculus of constructions paper?
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 ...
- 13.1k
10
votes
Accepted
Is CoC inconsistent with cnat_ind axiom?
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 ...
- 26.4k
10
votes
Is it reasonable to allow the type of a λ/∀-bound variable to refer to itself?
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 ...
- 1,290
10
votes
Can we derive Cubical Type Theory from Self-Types?
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 ...
- 26.4k
9
votes
Why an infinite type hierarchy?
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 ...
- 13.1k
8
votes
Accepted
Strong normalization property of CoC inside CoC
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 ...
- 13.1k
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.4k
7
votes
Accepted
Example of a function that you can write in Calculus of Constructions but not in System-F
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 ...
- 13.1k
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.1k
7
votes
Accepted
Church-style CoC with axiom for induction over Church-encoded unit, is it consistent?
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 ...
- 31.6k
7
votes
"Impredicative" in type theory
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.
...
- 10.2k
6
votes
Accepted
Complexity of type-checking in relation to complexity of normalization
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 ...
- 31.6k
6
votes
Accepted
Why isn't it "enough" to prove induction with one extra "INat" argument?
Let us spell out the informal meaning of INat, IntNat and IndNat2. Suppose we have a ...
- 26.4k
6
votes
Accepted
From Church-encoding to induction principle
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 ...
- 26.4k
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,783
6
votes
Accepted
What technique is used to implement type checking for CoC?
May I have a reference to why η expansion is invalid for CoC?
It's not invalid. It's up to choice whether $\eta$-conversion for functions (or other types) is included. The original CoC paper seems to ...
- 1,264
5
votes
Accepted
Is there a simple algorithm for proof search on CoC?
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". ...
- 526
5
votes
Accepted
Universe polymorphism: the inference of universes and their constraints
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 ...
- 26.4k
5
votes
Accepted
Proof of decidability of type checking of calculus of (co)inductive constructions?
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 ...
- 13.1k
5
votes
"Impredicative" in type theory
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}$$
...
- 611
5
votes
Accepted
Equality of decidable proofs?
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 ...
- 26.4k
5
votes
Accepted
How to prove that a circular prop is uninhabited?
You should use False instead of 1>2 in the conclusion of the theorem. Using indirect ways of denoting an impossible ...
4
votes
How to prove that a circular prop is uninhabited?
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, ...
- 11k
4
votes
Is it reasonable to allow the type of a λ/∀-bound variable to refer to itself?
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). ...
- 311
4
votes
Accepted
Context weakening as an explicit rule for languages of the the lambda cube?
If you intend to formalize meta-theorems in a proof assistant, then it's probably better to avoid the general weakening rule because it will pollute all your inductive arguments. Every single ...
- 26.4k
4
votes
Dependent eliminator for empty type in intensional Martin-Löf type theory
$\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}\,(\...
- 1,264
Only top scored, non community-wiki answers of a minimum length are eligible