2
$\begingroup$

I'm reading the paper "The Calculus of Constructions" by Thierry Coquand and Gerard Huet, and I'm having trouble with their inductive definition of $\Lambda$, starting on the second page. When I think of induction I usually think of there being a base step and an induction step. I'm not sure what either would be in this case.

What strikes me as most bizarre is the quantification rule: $$[x:M]N \in \Lambda_0^n \text{ if } M \in \Lambda^n, N \in \Lambda_0^{n+1}$$ So the definition of $\Lambda^n_0$ is in terms of $\Lambda^{n+1}_0$, which is then defined in terms of $\Lambda^{n+2}_0$ and so on. I'd think that an inductive definition of $\Lambda^n_0$ defines it in terms of $\Lambda^{n-1}_0$ and a base case $\Lambda^n_0$ but this can't be whats intended. I'm not sure then what the induction is supposed to be here at all.

I've noticed there are a lot more complicated inductive definitions in logic/computer science (e.g. BNF notation to define pre-terms of the lambda calculus) and I've always felt rather awkward carrying out those arguments. It's difficult to distinguish poor notation and not actually understanding it, so if Its relevant I'm also wondering how you go about these proofs/definitions in a systematic way.

$\endgroup$

1 Answer 1

2
$\begingroup$

An inductive type is defined with a list of 'constructors', that are simply rules specifying how to build terms of the type, either from scratch, or using previously built terms.

Here $\Lambda$ is defined together with $\Lambda_0^n$ and $\Lambda_1^n$ for all $n$ , with a list of rules given in page 2 and 3 of the article.

The rule $variables$ shows you how to build some terms for all $\Lambda_1^n$; the rule $universe$ shows you how to build some terms for all $\Lambda_0^n$. So with these 2 rules you can define terms of $\Lambda^n$.

Now you have a way to apply the $quantification$ rule, using a term $M$ of $\Lambda^n$, and a term $N$ of $\Lambda_0^{n+1}$. This will give you a new term of $\Lambda_0^n$, and therefore of $\Lambda^n$. And so on... As you see, it is perfectly possible to build a term of $\Lambda_0^n$ using a previously built term of $\Lambda_0^{n+1}$ !

By combining the different constructors in all the possible ways, you define 'the' terms of $\Lambda$ "by induction".

$\endgroup$
2
  • $\begingroup$ I think I get it now. We aren’t doing induction on n. It’s more like we ought to have another index $\Lambda^{n,m}$ and we are doing induction on m. The base step is essentially the variables and universe rules and the rest of the rules comprise the induction step. $\endgroup$
    – Robin
    Feb 3, 2020 at 22:52
  • $\begingroup$ Natural numbers are generated by induction with 2 rules. From this definition on natural number you can deduce the recursion and induction rules for natural numbers, that tells you how to prove a proposition for all natural numbers. Each inductive type follows the same scheme: they are defined by a list of rules. And from this list of rules you can deduce a recursion and an induction rule for the type, that tells you how to prove something for all terms of the type. But natural numbers are usually not involved in such inductive rule. Each inductive type comes with its own inductive rule. $\endgroup$
    – L. Garde
    Feb 4, 2020 at 21:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.