Talk:Calculus of constructions

Total

CoC can represent all functions provably total in higher-order logic, right? So, in what system is the strong normalization theory proved? Jim Apple 08:03, 19 August 2005 (UTC)

From the freely online accessible paper, I see no special care about this, even if the proof is not given. However, it does not seem that strong normalization is equivalent to consistency; they are both stated as corollaries of the same, rather technical theorem (whose proof is not included - the full reference given there is a PhD thesis in French). --Blaisorblade (talk) 01:14, 20 June 2008 (UTC)

Deficiencies in the article

The inference rules presented in this article seem deficient. In particular, there is no way to prove anything of the form ${\Gamma \vdash x:MN}$ from them. I imagine what's missing is a rule allowing one to derive $x:A$ from a derivation of $x:B$ and the beta-equality of $A$ and $B$, or something like that. Hopefully, someone more familiar with this material can clear things up. -Chinju 17:41, 2 November 2005 (UTC)

The online article (Coquand and Huet, 1986) states an obvious inference rule to prove typing for variables (they have the type declared in $\Gamma$), and states as a lemma (lemma 5 on page 7) that "if ${\Gamma \vdash M:N_{1}}$ and ${\Gamma \vdash M:N_{2}}$, then ${\Gamma \vdash N_{1}:N_{2}}$). I can't find the deduction rule you would like to have, but it should be surely a theorem, not a rule (even because typing judgements are introduced before conversion rules; conversion rules is the equivalent of beta-conversion in that article).--Blaisorblade (talk) 01:14, 20 June 2008 (UTC)

I retract my previous comment. The article has been changed significantly, and it now indeed includes a conversion typing rule, that is, "a rule allowing one to derive $x:A$ from a derivation of $x:B$ and the beta-equality of $A$ and $B$", as Chinju wrote. (It has the extra condition that $A:K$ for whatever technical reasons — but that might need a citation). I even misquoted Lemma 5 above: it should read ${\Gamma \vdash N_{1}=N_{2}}$. In the paper, the rule of conversion is the one asked for by Chinju, and does not need that side condition. However, that side condition is often needed (depending on the details of the formalization), for instance it is needed in pure type systems. --Blaisorblade (talk) 21:59, 10 August 2014 (UTC)

The whole article seem to miss many definitions or assume to get them from lambda calculus. When terms are defined, variables are not at all introduced. At a first look at the freely available paper, one sees no way to fully reconcile the article with the paper (in particular, it is not sufficient to assume that M and N are terms to form the term $(\lambda x:M)N$). The rules of conversion are omitted from the article; and so on. I'm marking this with the {{expert}} template.--Blaisorblade (talk) 00:46, 20 June 2008 (UTC)

A note: I know lambda-calculus and have read about Curry-Howard isomorphism, but I'm not at all an expert in the subject (particularly, in the calculus of constructions - I've just tried browsing the article to make sense of it). --Blaisorblade (talk) 01:14, 20 June 2008 (UTC)

Equiconsistency with ZFC

I removed the claim that the CoC was equiconsistent with ZFC because the paper cited ("Sets in types, types in sets") doesn't prove this. It uses a stronger type theory with inductive types, the calculus of inductive constructions. If ZFC[i] is ZFC with i inaccessible cardinals and CIC[i] is the calculus of inductive constructions with sorts Prop, Type₁, ..., Type_i, then the paper constructs a model of CIC[i] (plus choice and excluded middle axioms) in ZFC[i-1] and a model of ZFC[i] in CIC[i+2] (plus choice and excluded middle axioms.) Spacepotato (talk) 03:17, 3 February 2022 (UTC)

Clarification needed for notation

What do the notations

• $AB$,
• $\lambda x:A.B$, and
• $\forall x:A.B$

mean? The are not defined anywhere in the article. The-erinaceous-one (talk) 22:20, 24 February 2023 (UTC)

They represent function application, lambda-abstraction, and dependent product formation, respectively. Spacepotato (talk) 19:24, 17 April 2023 (UTC)

On the page Lambda cube, the calculus of constructions uses the $\Pi$ operator instead of $\forall$. It's my understanding that the use of $\forall$ in, e.g. System F or Hindley–Milner, gets translated as $\forall X.T[X]:=\Pi _{X:\ast }.T[X]$, i.e. "for all types X, T[X] is a type", so the $\Pi$ operator is more general. Does this need to be fixed, or is $\forall$ being used in a "punning" way? Metaweta (talk) 16:06, 24 May 2023 (UTC)

In this context, there is not much difference between $\Pi$ and $\forall$. You can use whichever you prefer. Spacepotato (talk) 17:35, 31 July 2023 (UTC)

Definition of "small" and "large" types

These terms are not defined on this page, nor anywhere else on Wikipedia as far as I can tell. They should either be defined or removed. Ablueberry87 (talk) 01:49, 6 January 2024 (UTC)

Bold 5.139.227.97 (talk) 11:56, 7 April 2024 (UTC)