Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange
2
votes
3answers
161 views

Is it reasonable to allow the type of a λ/∀-bound variable to refer to itself?

Usually, in Pure Type Systems, the type of a λ/∀-bound variable is only accessible on its body. That is, on λ (X : A) -> B, <...
4
votes
1answer
64 views

Complexity of type-checking in relation to complexity of normalization

In order to verify that a terminating program terminates, one thing that can be done is to actually run the program. That may take a lot of time. If the program is typed in a total type-system, we can ...
4
votes
1answer
155 views

Why isn't it “enough” to prove induction with one extra “INat” argument?

It is well known that it is impossible to prove the induction principle for Natural numbers on the Calculus of Constructions. That is, ...
5
votes
0answers
59 views

Can any Calculus of Construction term be built up from application of a finite number of terms?

Can we form a finite set of well typed calculus of construction terms such that any closed term can be built up from them (plus the type of large types) using only application? I conjecture that the ...
1
vote
1answer
108 views

How could one define a language based on the Calculus of Constructions, but with fixed points and EAL-style duplication restrictions?

Suppose that we take the Calculus of Constructions as a basis, but take away exponential functions (allowing only linear functions), and add the controlled duplication rules of EAL. That'd, I believe, ...
8
votes
3answers
180 views

Calculus of Constructions: Compress expression to it's smallest form

I'm aware that the Calculus of Constructions is strongly normalizing, meaning every expression has a normal for that cannot be beta,eta-reduced further. So in fact this is the most efficient ...
11
votes
1answer
178 views

Typo in the calculus of constructions paper?

In the classic the calculus of constructions paper there is a rule that states (page 7 of the pdf, page 101 of the original document) This rule would mean that any context is reducible to a member ...
4
votes
1answer
223 views

Strong normalization property of CoC inside CoC

Wikipedia says that The CoC is strongly normalizing, although, by Gödel's incompleteness theorem, it is impossible to prove this property within the CoC since it implies inconsistency. Why is ...
5
votes
1answer
165 views

Proof of decidability of type checking of calculus of (co)inductive constructions?

I often see it asserted that type checking is decidable for CIC, but I haven't seen it proven. Is there a good paper (or simple demonstration) of this?
19
votes
2answers
2k views

How do you get the Calculus of Constructions from the other points in the Lambda Cube?

The CoC is said to be the culmination of all three dimensions of the Lambda Cube. This isn't apparent to me at all. I think I understand the individual dimensions, and the combination of any two seems ...
8
votes
2answers
398 views

“Impredicative” in type theory

I am confused. I think I've read two usages of the word "impredicative" in type theory: When people talk about the "impredicative" version of Martin-Löf's type theory, which they say it is ...
9
votes
1answer
351 views

Is MLTT effectively pCiC without Prop?

Is Martin-Löf type theory basically the predicative Calculus of inductive Constructions without impredicative $\mathtt{Prop}$? If they're closely related but with more differences than just $\mathtt{...
9
votes
1answer
515 views

Equality of decidable proofs?

I want to know if the decidability of equality of two decidable proofs of the same proposition can be proved without any additional axioms in Calculus of Inductive Constructions. Specifically, I want ...
17
votes
2answers
538 views

Why an infinite type hierarchy?

Coq, Agda, and Idris have an infinite type hierarchy (Type 1 : Type 2 : Type 3 : ...). But why not do it instead like λC, the system in the lambda cube that's closest to the calculus of constructions, ...
1
vote
2answers
234 views

How to prove that a circular prop is uninhabited?

Consider the following inductive definition of "ElProp" in coq: ...
14
votes
1answer
306 views

How to show that a type in a system with dependent types is not inhabited (i.e. formula not provable)?

For systems without dependent types, like Hindley-Milner type system, the types correspond to formulas of intuitionistic logic. There we know that its models are Heyting algebras, and in particular, ...
6
votes
1answer
230 views

Forms of types in the calculus of constructions

In the usual presentations of the calculus of constructions (CC) with two kinds Prop and Type such that Prop:Type and impredicative on Prop, it is easy to show the following result: every closed term ...