Why does the conversion rule for CIC apply only to types instead of all terms?

Miscellaneous
1

I’m currently learning Rocq and working my way through the typing rules.

One thing that stuck out to me while I was reading the rules is:

  • the convertibility rules are defined for terms in general;
  • however, the conversion typing (Conv) rule only allows types (but not terms in general) to be transformed.

Is the decision to restrict conversion to types instead of terms:

  • documented in any papers/resources on the history of Rocq?
  • due to any consistency issues in logic?
  • merely a stylistic choice that aids some way in the development of Rocq itself, in Rocq usage, or Rocq education?
  • due to some other reason?

Context: while I’ve had formal training in logic/theorem proving, it was in a non-type-theoretic setting, so it seems there is some bits of intuition/understanding/folk-lore which I haven’t picked up yet — this feels like one of those pieces.

2

Conversion applies to terms too, but what would you reduce term in type checking ?
Reduction of terms is for computation

PS: don’t hesitate to check the zulip
PS2: a reference https://dl.acm.org/doi/10.1145/3706056

3

(In Rocq,) all types are terms, but not all terms are types.

In particular, the conversion rules for terms in general are a thing, that Conv rule instead is about changing (“converting”) the type of a term given subtyping of the type: that’s no restriction, it’s just a piece of the puzzle that relates terms to types…

4

Addressing Feedback

Thanks for the replies all! Let me address them first.

Reduction of terms is for computation

This is a good intuition! Thanks for that. At the same time, that doesn’t necessarily imply (at least to me) that general term reduction would be unhelpful during type checking.

PS: don’t hesitate to check the zulip

I wasn’t aware of the Rocq Zulip — is that a better place to ask questions than here?

PS2: a reference https://dl.acm.org/doi/10.1145/3706056

Thanks for this reference — it doesn’t seem to directly answer this question, but it delves alot into the meta-theory of Rocq which helps alot with understanding!

> (In Rocq,) all types are terms, but not all terms are types.

Yep, this is important context needed to understand the overall question. Thanks for clarifying that.

that Conv rule instead is about changing (“converting”) the type of a term given subtyping of the type: that’s no restriction, it’s just a piece of the puzzle that relates terms to types…

It’s not obvious to me why your statement above is true — to my untrained eyes, the way (Conv) is written seems restricting somehow, but that could be due to my own ignorance.

Follow-up Thoughts

After thinking about my question, I realized there are some good reasons why term reduction would be unhelpful for Rocq, a type-checking based theorem prover:

  1. Incorporating general term reduction into the type-checking process requires type-checking to preserve decidability

    So, firstly, recall that β-reduction on untyped terms is non-terminating, e.g., consider self-applying the un-typable ω combinator λx.xx. This means we can’t safely reduce terms unless we know they, at least, have some type.

    Thus, to incorporate term reduction in the logic (i.e., to try and reduce a term t in a judgment E;Γ |- t : T) while keeping type checking decidable, we would need to first check that the term t has some type T’ (possibly with T != T’).

    Of course, at this point, for the overall judgment to hold, we require that T’ <= T and checking that this subtyping relation holds is exactly what the (Conv) rule allows us to check.

    But let us continue and insist on reducing t in-place. Then using the convertibility rules, we could derive a new judgment of the form E;Γ |- t' : T where t |> t’ : T’ such that _|>_:<type> represents the transitive closure over the convertibility rules where the start term has type <type> (and the final term must as well, by type preservation).

    At this point, we still need to prove t’ : T. To do so, I see two obvious strategies:

    • (a) attempt to prove t' : T without making use of the intermediate type-check step that proves that t : T’— this will likely require us to redo work that we have already done since we’ll need to build a new type derivation from scratch
    • (b) attempt to re-use the intermediate type-check step t : T’ to help us prove that t : T. But note that, if we do this, the term t’ is irrelevant and the whole enterprise essentially boils down to checking T’ <= T, i.e., applying the (Conv) rule.

    In either case, the reduction t |> t’ : T didn’t really buy us that much.

  2. Arbitrary term reduction would break any syntax directedness for the rules of the proof system

    If we try to try and use some more complex form of strategy (1)(a) where we avoid re-creating a type derivation tree, we essentially must give up syntax directedness.

    That is, at any point, the proof rule that we are applying might apply either to (i) an unreduced term t or (ii) a reduced term t’ — but in case (ii), the rules that we apply wouldn’t really correspond to the shape of t’ since the prior type derivation t : T’ was based on the structure of t.

At this point, I feel pretty convinced from the the two points I mentioned above that general term reduction in a dependently typed setting would be a bad idea.

So, two last questions:

  1. Do you guys agree with my points above? If not, I’d love to know why!
  2. Are there any other points aside from the above two that would demonstrate that general term reduction would be unhelpful for a type-checking-based theorem prover like Rocq?
5

Do you guys agree with my points above? If not, I’d love to know why!

No, Rocq is not a “type-checking-based theorem prover”, it is more generally a full-fledged dependently-typed functional language. And few of those term conversion rules, i.e. alpha-conversion and beta-reduction, you can indeed already find in plain lambda-calculus.

The typing, and especially the dependent typing, rather adds expressivity and complexity, up to proving theorems: but then again, that does not reduce to any system of “just logic”.

to my untrained eyes, the way (Conv) is written seems restricting somehow

As for the typing rules, the Conv rule says, in short, that if t : T, then also t : U for any supertype U of T. It’s an enlargement/lifting (maybe more precisely a kind of cumulativity, but I am not 100% sure that label is appropriate there), anyway the very opposite of a “restriction”.

So, firstly, recall that β-reduction on untyped terms is non-terminating, e.g., consider self-applying the un-typable ω combinator λx.xx.

Except that indeed you cannot do that in (plain) Rocq/CIC…

The devil is in the detail. ; )

6

No, Rocq is not a “type-checking-based theorem prover”, it is more generally a full-fledged dependently-typed functional language. And few of those term conversion rules, i.e. alpha-conversion and beta-reduction, you can indeed already find in plain lambda-calculus.

The typing, and especially the dependent typing, rather adds expressivity and complexity, up to proving theorems: but then again, that does not reduce to any system of “just logic”.

Thanks for that clarification. I agree!

As for the typing rules, the Conv rule says, in short, that if t : T, then also t : U for any supertype U of T. It’s an enlargement/lifting (maybe more precisely a kind of cumulativity, but I am not 100% sure that label is appropriate there), anyway the very opposite of a “restriction”.

Hmm… perhaps I did not express myself clearly enough. My original point was that the Conv rule with premises:

E;Γ |- U : s E;Γ |- t : T E;Γ |- T <= U

And conclusion:

E;Γ |- t : U

Restricts the application of any reduction/convertibility rules including:

  • β
  • δ
  • ζ
  • and so on…

embedded in the _ <= _ relation to types, when these embedded rules also apply to terms. So we could imagine an alternate form of the conversion rule Conv2 that has the premises:

E;Γ |- U : s E;Γ |- t : T E;Γ |- t |> t' E;Γ |- T <= U

And the conclusion:

E;Γ |- t' : U

where t |> t’ is the transitive closure of the union of all of the reduction/convertibility relations (β, δ, ζ, …).

The restriction to which I was referring was the fact that the reduction/convertibility relation is not applied freely in Conv but limited to be used on types.

Except that indeed you cannot do that in (plain) Rocq/CIC…

I agree!

My point in that paragraph was that the untyped lambda calculus is non-terminating — I was not talking about CIC or any other typed lambda calculus-based system.

I made that point to discuss the need for well-typedness in order to preserve termination, decidability of term normalization, and decidability of type checking (in a dependently typed system).

Hopefully that’s more clear. Thanks.

7

My original point was that the Conv rule [… r]estricts the application of any reduction/convertibility rules

I don’t see it: that Conv is a bit a misnomer, but the two things, term conversion rules and the typing rules, are rather orthogonal.

t |> t’ is the transitive closure of the union of all of the reduction/convertibility relations

That I find literally meaningless (as part of a typing rule), anyway I think I get the intent: let t' be any term that t converts/reduces to, then t' (too!) has type T' for any supertype T' of T: but, you can get the same by 1) reducing the term, which won’t change its type, then 2) lifting the type; or vice versa, i.e. lifting the type then reducing the term. IOW, as said, it seems to me you are rather mixing orthogonal concepts there.

8

I understand my first answer was unprecise. You do not have a rule a : A and a conv v => v : A because this is a property of typing: subject reduction. You do have computation of term in types, for instance vec A (1 + 3) conv vec A 4. This is vital as soon as you start having real type dependency.

The restriction to which I was referring was the fact that the reduction/convertibility relation is not applied freely in Conv but limited to be used on types.

This is wrong. Reduction is applied generically in typing. In Rocq conversion is untyped, so it is the same algorithm for types and terms. If it is only applied to types, it is because they are no reason to apply it to anything else in the definition of typing. This will still reduce any term in types, using whatever rules it needs, like in the vec example above.

term conversion rules and the typing rules, are rather orthogonal.

This is rather false. Decidability of conversion is fundamental for decidability of type checking, and to verify most properties we care about typing like subject reduction. Moreover, if you start having a typed conversion, then typing and conversion become mutually inductive which makes the whole thing complicated, and having typed conversion to get eta-conversion is a subject of research.

However, @sskeirik you are right to think that applying conversion to well-formed types is important.
From what I rememeber, it is cruciall to prove properties like validity, i.e. t : T => exists s, T : Sort s. I think this can be seen in how conversion is split and dispatch in the bidirectional algorithm that is used in practice to type check terms.

9

But “orthogonal” entails “independent”, which is the opposite of how you are reading it. OTOH, your reference to “type checking” is rather all encompassing and just beside the point in the context of the original question and the explanations I have been giving.

(P.S: I didn’t know flagging your post would hide it and I cannot undo it: I am only complaining about a behaviour that is as unreasonable and destructive as it’s becoming a habit. As a minimum, you should take a little bit more time reading things before you jump your guns: and do stick to Zulip please, if that’s all eventually you have to say.)

10

Thanks for the pointers @jp-diegidio @thomas-lamiaux.

After the last round of posts, something finally clicked for me.

I realized that my mental model of Rocq was inaccurate and that led me to misunderstand the Conv rule.

Essentially, Rocq can be understood through two lenses:

  1. As a dependently typed functional language with a type-checker and evaluator for the language;
  2. As a theorem prover for a logic embedded in the language via the Curry-Howard correspondence, i.e. propositions-as-types and proofs-as-terms.

Previously, I have been primarily viewing Rocq through lens (2). From this lens, I was viewing the typing rules of Rocq like proof rules for a higher-order logic proof system (of course, this is not really precise).

But from the point of view of a logical proof system, I was thinking that it would be good to normalize terms aggressively (and perhaps have an invariant that terms are stored in normalized form). I have encountered proof systems that do this very thing. If used correctly, normalization can make a proof much smaller/more efficient.

On the other hand, from lens (1), i.e., a functional programming and programming language theory lens, it feels so obvious why terms are not reduced during the type checking algorithm — because that’s how type checking itself is defined! And I believe this is the point that @thomas-lamiaux was trying to make in his original response.

Indeed, we want to type check the input term as written by the programmer and not some term that the input term reduces to ! Going further, it may even be the case that an ill-typed term reduces to a well-typed term, so attempting this may actually break type checking instead of optimizing it.

Anyway, that summarizes my thoughts up to this point. As always, I welcome your feedback. Thanks much!

11

Essentially, Rocq can be understood through two lenses […]
(of course, this is not really precise).

And isn’t a more precise understanding exactly what you are looking for? E.g. if you get deeper, even Curry-Howard needs some caution:
https://ncatlab.org/nlab/show/propositions+as+types
https://ncatlab.org/nlab/show/propositions+as+some+types

And a plain “proposition as types” I find not even particularly illuminating, all the more so if we look at the concrete details of Rocq: indeed, Prop (and even SProp, in principle) are just sorts with some peculiar rules, and they only approximately represent any propositional or otherwise logic.

it feels so obvious why terms are not reduced
during the type checking algorithm

And I did say orthogonal. And then again, the devil is in the detail: e.g. can you tell in the Core chapter of the manual, where exactly “type checking” (without further qualifications) starts and where it ends? We could rather get even deeper there, and my point just was: 1) we shouldn’t be blurring the very distinctions we were trying to make; and, indeed, 2) as I am sure you’d agree, past an initial introductory level, reading (and linking from) the manual is in fact crucial…

12

I do not understand what you mean by

But “orthogonal” entails “independent”, which is the opposite of how you are reading it.

FYI: I have no animosity towards you. I don’t know you :smiley:. You are simply saying sth that looks scientifically false, so I answered using my experience and knowledge of Type Theory and MetaRocq. That is it. If you think my answer is false for a good reason, or misunderstood you which can obviously happen when people do not speak in their native language, you are free to answer to clarify your thoughts or point out an error I would have made.

and do stick to Zulip please

Let us make one thing clear. You got ban from zulip for repeated infringement to the code of conduct. Not me. I am free to answer here, and because it is not part of your sanction, so are you provided you respect the code of conduct. If you feel my behaviour is not appropriate and breaks the code of conduct, you are free to signal it to the moderators, and they will look at it. However, you are not a moderator and telling people there are not allowed to discuss here is not acceptable.

This being said, I really have nothing against you and I wish you to have a good summer.

Best,
Thomas Lamiaux