# Tag Info

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.8k

### 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
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
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

### 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

### 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
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
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
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

### "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.4k

### 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
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
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.8k
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 ...
• 1,349
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
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.8k
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

### 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,823
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,349

### 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
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

### "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}$$ ...
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
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". ...
• 536
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
Accepted

• 1,349
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

### 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). ...

### 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