Share Your Experience: Take the 2024 Developer Survey

# 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 ...
• 32.6k

### 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.9k
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 ...
• 29.2k
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.9k

### 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 ...
• 29.2k

### 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,320
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 ...
• 29.2k
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.9k

### 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.9k
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.9k
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 ...
• 32.6k
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,629
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,629
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 ...
• 29.2k
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 ...
• 32.6k
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 ...
• 29.2k

### 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 ...
• 5,483

### 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.9k
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.9k
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". ...
• 546
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 ...
• 29.2k
Accepted

• 1,629
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 ...
• 29.2k