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 ...
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.3k
21 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.3k
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.3k
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.8k
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 ...
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.8k
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.3k
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.8k
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. ...
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.3k
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.3k
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 ...
7 votes
Accepted

What is the computational power of the Calculus of Constructions?

There is no total language where all total computable $\mathbb{N} \to \mathbb{N}$ functions are definable. In a total language, an interpreter for the same language is not definable because if it were ...
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.8k
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 ...
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.8k
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 ...
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 ...
6 votes

What is the computational power of the Calculus of Constructions?

My understanding of András' answer is that, while it gets the gist correct, his final conclusion is not quite right: The "standard" way to determine the strength of the function space in a ...
  • 13.3k
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.3k
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}$$ ...
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.8k
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". ...
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.8k
5 votes
Accepted

Defining normalization with respect to judgmental equality instead of reduction

You could define a predicate $N(t)$ whose intuitive meaning is “term $t$ is in normal form”, and prove a theorem stating that for every closed term $t$ there is precisely one term $t'$ such that $N(t')...
  • 26.8k
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}\,(\...
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.8k
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). ...
3 votes

Forms of types in the calculus of constructions

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 ...
  • 13.3k

Only top scored, non community-wiki answers of a minimum length are eligible