Skip to main content
Share Your Experience: Take the 2024 Developer Survey

Questions tagged [calculus-of-constructions]

Calculus of Constructions (CoC) is a dependent type system. It's on the lambda cube and is implemented in the Coq proof assistant.

Filter by
Sorted by
Tagged with
2 votes
1 answer
78 views

What are some practical applications of inductive-inductive and inductive-recursive types?

Since this question got not many answers Im hoping asking again could convey that this has some importance. Anyway so in undergraduate education, I was working on research to implement dependent-...
AnonymousThunk's user avatar
0 votes
1 answer
131 views

Isn't it misleading for Scala 3 to claim it has dependent function types?

I am learning Scala 3 and so far I am really enjoying it. I was going through its reference documentation and I noticed that it claims to have dependent function types. This feels misleading to me ...
Valmir Junior's user avatar
10 votes
1 answer
894 views

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

Reading Barendregt's chapter “Lambda Calculi with Types” in the Handbook of Logic in Computer Science (vol. 2: Computational Structures) (Abramsky, Gabbay & Maibaum eds., 1992) I learned (op. cit. ...
Gro-Tsen's user avatar
  • 841
8 votes
3 answers
1k views

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

Here is a Coq proof I've came up with: ...
Zazaeil's user avatar
  • 212
0 votes
0 answers
42 views

List of calculi suitable for generic computation

I'm looking for a list of calculi suitable for generic computation such as Lambda calculus, Pi calculus, and event calculus. What else do we have? Thank you.
geeko's user avatar
  • 131
1 vote
1 answer
200 views

Defining normalization with respect to judgmental equality instead of reduction

In type theory with a type $\mathbb{N}$ of natural numbers (or some other base type such as booleans) and judgmental equality instead of reductions, canonicity is a meta-theoretical statement claiming ...
Ilk's user avatar
  • 920
2 votes
2 answers
450 views

What is the computational power of the Calculus of Constructions?

The calculus of constructions (CoC) without fix is clearly not Turing complete, as the program that loops infinitely cannot be expressed in it. What I'm wondering: ...
Jonathan's user avatar
1 vote
0 answers
36 views

Can this be formalized as a conversion rule for CoC?

Consider the Church encoding of booleans in CoC $$ Bool := \forall t : * . t \to t \to t \\ T := \lambda t : * . \lambda x : t . \lambda y : t . x \\ F := \lambda t : * . \lambda x: t . \lambda y : t ....
Cristian Gratie's user avatar
8 votes
4 answers
541 views

Type theory and fixed points of datatypes

For the purposes of this question, say that a datatype is a type constructor with one type parameter (this is sometimes called a type operator). In Haskell, we can define a fixed point ...
Ilk's user avatar
  • 920
3 votes
1 answer
120 views

Implementation of vectors as dependent types in CoC

I'm trying to understand dependent types in CoC and I am having trouble finding examples that are actually carried out in CoC, specifically without inductive types or pattern matching. The most ...
Cristian Gratie's user avatar
2 votes
0 answers
75 views

Properties of the polymorphic type $\Pi t : * . ((t \to t) \to t) \to t$

In the context of pure type systems (say Calculus of Constructions) I am looking for references discussing the properties of the following polymorphic type: $\Pi t : * . ((t \to t) \to t) \to t$. What ...
Cristian Gratie's user avatar
3 votes
2 answers
547 views

What technique is used to implement type checking for CoC?

I am studying David Christiansen's tutorial on implementing a dependently typed language, where it says: Typed normalization by evaluation is far from the only way to implement conversion checking ...
Siddharth Bhat's user avatar
0 votes
1 answer
248 views

Calculus of constructions: Why forall when pi exists?

I'm studying the calculus of constructions from ATAPL, Chapter 2. I'm trying to understand the Type Equivalence rule, which describes the meaning of the new type family ...
Siddharth Bhat's user avatar
2 votes
1 answer
184 views

Dependent eliminator for empty type in intensional Martin-Löf type theory

In calculus of inductive constructions you can just say that the empty type is the type with no constructors and it automatically builds the dependent eliminator. But let's say I'm setting up ...
user avatar
0 votes
0 answers
85 views

What do we call a type system where any term of any type ultimately parses down to $*:\mathbf{1}$?

If a type system allows inductive types (as in e.g. Coq) then we can coin new primitive constants that inhabit types. For example $0:\mathbb{N}$ is constructed when defining $\mathbb{N}$ and does not ...
tts's user avatar
  • 11
5 votes
1 answer
213 views

Context weakening as an explicit rule for languages of the the lambda cube?

I'm trying to formalize the syntax and typing judgments of the Calculus of Constructions in Coq. I'm choosing to use the Pure Type Systems presentation of CoC; however, I've seen mild variations in ...
NJay's user avatar
  • 117
18 votes
1 answer
1k views

Can we derive Cubical Type Theory from Self-Types?

Self Types are known for being a simple extension to the Calculus of Constructions that allow it to derive all inductive datatypes of a proof assistant like Coq and Agda, without a "hardcoded&...
MaiaVictor's user avatar
  • 3,137
4 votes
1 answer
500 views

Church-style CoC with axiom for induction over Church-encoded unit, is it consistent?

If we start with the Calculus of Constructions, and then use the following definitions for the Church-encoded Unit: ...
Labbekak's user avatar
  • 701
2 votes
1 answer
369 views

From Church-encoding to induction principle

I am looking for an algorithm to go from a Church-encoded datatype to their induction principle in the Calculus of Constructions. For example: ...
Labbekak's user avatar
  • 701
3 votes
1 answer
209 views

Type of induction principle for fixpoint types

To the Calculus of Constructions we could add a general fixpoint type constructor (accepting inconsistencies or assuming F is a ...
Labbekak's user avatar
  • 701
2 votes
1 answer
163 views

Lack of atomic propositions in the Calculus of Constructions from ATTAPL textbook

I am working through the Dependent Types chapter from Advanced Topics in Types and Programming Languages (ATTAPL) by Benjamin Pierce et al. I am confused with the calculus presented Fig 2-7 (Calculus ...
Ram's user avatar
  • 31
0 votes
0 answers
100 views

Proposition terms vs types in Coq

Consider the following div function written in Coq. It takes in a proof that the divider is non-zero. Definition div (n d:nat) (pf: ~(d = 0)) := n/d. Focus on <...
Ram's user avatar
  • 31
7 votes
1 answer
260 views

Example of a function that you can write in Calculus of Constructions but not in System-F

It's been suggested in an answer to this question that the Calculus of Constructions has more computational strength than System-F. What are examples of functions that you express in CoC that you ...
Labbekak's user avatar
  • 701
8 votes
0 answers
626 views

An axiom for John Major's Equality

In the the standard library of Coq, there is the axiom: Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y. Why isn't it provable? Can it be reduced ...
Bob's user avatar
  • 381
4 votes
1 answer
158 views

Is there a simple algorithm for proof search on CoC?

Given the usual Calculus of Constructions with an extra primitive, _, that stands for "attempt to fill this location in a way that type-checks", is there any simple/...
MaiaVictor's user avatar
  • 3,137
4 votes
0 answers
119 views

Proof that CIC or Dybjer-style eliminators are strongly-normalizing?

Related to this question I'm wondering, what is the standard technique for showing that dependent types with eliminators are strongly normalizing? I'm thinking something like the Calculus of ...
Joey Eremondi's user avatar
3 votes
1 answer
381 views

Universe polymorphism: the inference of universes and their constraints

When making a universe polymorphic definition in Coq, universes and their constraints are automatically inferred. Are they somewhat the most general ones (in a sense similar to the principal type ...
Bob's user avatar
  • 381
6 votes
1 answer
154 views

Is CoC inconsistent with cnat_ind axiom?

It is not possible to derive induction for Church-encoded datatypes on the Calculus of Constructions (source). Moreover, according to the accepted answer to another question, it is also not possible ...
MaiaVictor's user avatar
  • 3,137
3 votes
3 answers
247 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, <...
MaiaVictor's user avatar
  • 3,137
5 votes
1 answer
477 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 ...
Łukasz Lew's user avatar
  • 1,187
4 votes
1 answer
246 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, ...
MaiaVictor's user avatar
  • 3,137
4 votes
0 answers
87 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 ...
Christopher King's user avatar
1 vote
1 answer
176 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, ...
MaiaVictor's user avatar
  • 3,137
11 votes
3 answers
320 views

Calculus of Constructions: compress expression to its 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 ...
user47376's user avatar
  • 213
10 votes
1 answer
237 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 ...
user833970's user avatar
6 votes
1 answer
660 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 ...
amakarov's user avatar
  • 163
6 votes
1 answer
326 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?
Shea Levy's user avatar
  • 213
26 votes
2 answers
4k 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 ...
sleepytea's user avatar
  • 363
14 votes
2 answers
2k 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 ...
user40579's user avatar
  • 141
15 votes
1 answer
1k 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{...
user's user avatar
  • 615
9 votes
1 answer
952 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 ...
Adam Barak's user avatar
20 votes
2 answers
975 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, ...
Rui Baptista's user avatar
1 vote
2 answers
363 views

How to prove that a circular prop is uninhabited?

Consider the following inductive definition of "ElProp" in coq: ...
Gowtham Kaki's user avatar
16 votes
2 answers
464 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, ...
Petr's user avatar
  • 2,601
6 votes
1 answer
289 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 ...
Vincent's user avatar
  • 61