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 ...
Neel Krishnaswami's user avatar
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. ...
cody's user avatar
  • 13.8k
18 votes
Accepted

Yet another constructive (Coq) proof that `nat -> nat -> nat` is not bijective. How to explain it to myself?

First, let me say that "constructive" does not imply "all maps are Turing computable". It means “no excluded middle and axiom of choice were used“. In constructive mathematics the ...
Andrej Bauer's user avatar
  • 28.7k
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 ...
cody's user avatar
  • 13.8k
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 ...
Andrej Bauer's user avatar
  • 28.7k
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 ...
Andreas Rossberg's user avatar
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 ...
Andrej Bauer's user avatar
  • 28.7k
10 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 ...
cody's user avatar
  • 13.8k
10 votes

Intuitive explanation of the fact that the Calculus of Constructions is not conservative over Higher-Order Logic

I do not know if this answers your question, but in Propositions as [Types] we communicate in Remark 6.6 an observation by Thierry Coquand, namely that the statement $$ (\forall x .\, \exists y .\, R(...
Andrej Bauer's user avatar
  • 28.7k
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 ...
Andrej Bauer's user avatar
  • 28.7k
8 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. ...
Martin Berger's user avatar
7 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}$$ ...
Andrea Asperti's user avatar
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 ...
cody's user avatar
  • 13.8k
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 ...
cody's user avatar
  • 13.8k
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 ...
Neel Krishnaswami's user avatar
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 ...
András Kovács's user avatar
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 ...
András Kovács's user avatar
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 ...
Andrej Bauer's user avatar
  • 28.7k
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 ...
Neel Krishnaswami's user avatar
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 ...
Andrej Bauer's user avatar
  • 28.7k
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 ...
Damiano Mazza's user avatar
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 ...
cody's user avatar
  • 13.8k
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 ...
cody's user avatar
  • 13.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". ...
user833970's user avatar
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 ...
Andrej Bauer's user avatar
  • 28.7k
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')...
Andrej Bauer's user avatar
  • 28.7k
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}\,(\...
András Kovács's user avatar
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 ...
Andrej Bauer's user avatar
  • 28.7k
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). ...
Rodolphe Lepigre's user avatar
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 ...
cody's user avatar
  • 13.8k

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