I am learning the typed lambda-calculus and looking into the Calculus of Constructions. It was going well until I was slapped in the face with variations, and now I'm confused about the layout of all the different versions. As far as I can tell, the versions of basic CoC include theories with:

  • Abstraction and conversion similar to pure type systems.
  • Modified abstraction rule.
  • Relaxed conversion rule.
  • Modified abstraction rule and relaxed conversion rule.

On top of this, it seems that on top of each variation can be built a more general theory of the sort (Predicative, Extended) Calculus of (Inductive, Coinductive) Constructions (with Rewriting, with eta-reduction), where you are free to pick your choice/exclusion of parentheses. I don't know exactly which combinations are allowed, however.

Can anyone give meaning to these variations, and how I can think about them in relation to each other?

  • $\begingroup$ There's no such thing as "forbidden" in mathematics, you are making axioms, so you can choose whatever you want. So unless you don't want something, it is allowed. $\endgroup$
    – Trebor
    Apr 5, 2023 at 4:55
  • 2
    $\begingroup$ I assume “allowed” means something more like “sensible”, or more precisely, maintains some useful properties that the CoC has – e.g consistency, canonicity, strong normalisation, a usable raw term language and elaboration procedure, &c. $\endgroup$
    – James Wood
    Apr 5, 2023 at 9:14
  • $\begingroup$ @mudri Something like is, say, a predicative calculus of inductive constructions with rewriting and modified abstraction rule even consistent? The other question i have is what could, say, that combination do that the others couldn't? $\endgroup$
    – Alex Byard
    Apr 5, 2023 at 21:10
  • $\begingroup$ @Trebor Yes, i agree. I just don't have the intuition for what each addition allows you to do, or what benefits each combination might have as opposed to others. Essentially I'm trying to organize it in my head as a higher dimensional lambda-cube. $\endgroup$
    – Alex Byard
    Apr 5, 2023 at 21:13
  • $\begingroup$ @AlexByard What's the “modified abstraction rule”? Anyway, I think something like this is consistent if you restrict rewrites to true (or, in particular, just provable) equations, whereas I'd be unsure about consistency with anti-Type-is-Set principles like univalence. But this is not really my area of expertise, so I wouldn't be surprised to be wrong either way. Rewriting will soon break other properties, though. $\endgroup$
    – James Wood
    Apr 6, 2023 at 8:33


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.