Skip to main content
Proof Assistants Beta

Return to Question

Became Hot Network Question
edited tags
Link
Jason Rute
Jason Rute
  • 10.2k
  • 1
  • 20
  • 57
deleted 4 characters in body; edited title
Source Link
ice1000 ♦
ice1000 ♦
  • 6.5k
  • 11
  • 64

How much of trouble is Lean4'sLean's failure of normalization, given that logical consistency is not obviously broken?

This document showed that Lean4'sLean's impredicative universe of strict propositions breaks normalization (of proofs) in a way that canonicity and logical consistency are unaffected, because the counterexample lives in Prop. I wonder how much of trouble it will be to have this counterexample, like both syntactically (in terms of Lean4Lean type checking) and semantically (in terms of Lean4Lean metatheory)?

To me, it seems that you simply need to prevent reduction for terms in Prop and assume them to be equal. This will at least recover the termination of type checking (well, at least refute this particular counterexample of termination of type checking). This can solve the obvious trouble pointed out by the paper.

Pierre-Marie Pédrot said that:

Impredicative SProp breaks SN only when you can eliminate the SProp equality into a non-SProp sort. Otherwise, it's fine.

I'm also unsure about that. I think it is established that equalities in SProp cannot be eliminated into non-SProp (like boolean in SProp has true = false, but if we can eliminate this into non-SProp booleans, we get logical inconsistency), so I assumed this is disallowed in Lean4Lean, but still the paper I linked in the beginning claimed that normalization is broken by their counterexample.

How much of trouble is Lean4's failure of normalization, given that logical consistency is not obviously broken?

This document showed that Lean4's impredicative universe of strict propositions breaks normalization (of proofs) in a way that canonicity and logical consistency are unaffected, because the counterexample lives in Prop. I wonder how much of trouble it will be to have this counterexample, like both syntactically (in terms of Lean4 type checking) and semantically (in terms of Lean4 metatheory)?

To me, it seems that you simply need to prevent reduction for terms in Prop and assume them to be equal. This will at least recover the termination of type checking (well, at least refute this particular counterexample of termination of type checking). This can solve the obvious trouble pointed out by the paper.

Pierre-Marie Pédrot said that:

Impredicative SProp breaks SN only when you can eliminate the SProp equality into a non-SProp sort. Otherwise, it's fine.

I'm also unsure about that. I think it is established that equalities in SProp cannot be eliminated into non-SProp (like boolean in SProp has true = false, but if we can eliminate this into non-SProp booleans, we get logical inconsistency), so I assumed this is disallowed in Lean4, but still the paper I linked in the beginning claimed that normalization is broken by their counterexample.

How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken?

This document showed that Lean's impredicative universe of strict propositions breaks normalization (of proofs) in a way that canonicity and logical consistency are unaffected, because the counterexample lives in Prop. I wonder how much of trouble it will be to have this counterexample, like both syntactically (in terms of Lean type checking) and semantically (in terms of Lean metatheory)?

To me, it seems that you simply need to prevent reduction for terms in Prop and assume them to be equal. This will at least recover the termination of type checking (well, at least refute this particular counterexample of termination of type checking). This can solve the obvious trouble pointed out by the paper.

Pierre-Marie Pédrot said that:

Impredicative SProp breaks SN only when you can eliminate the SProp equality into a non-SProp sort. Otherwise, it's fine.

I'm also unsure about that. I think it is established that equalities in SProp cannot be eliminated into non-SProp (like boolean in SProp has true = false, but if we can eliminate this into non-SProp booleans, we get logical inconsistency), so I assumed this is disallowed in Lean, but still the paper I linked in the beginning claimed that normalization is broken by their counterexample.

Source Link
ice1000 ♦
ice1000 ♦
  • 6.5k
  • 11
  • 64

How much of trouble is Lean4's failure of normalization, given that logical consistency is not obviously broken?

This document showed that Lean4's impredicative universe of strict propositions breaks normalization (of proofs) in a way that canonicity and logical consistency are unaffected, because the counterexample lives in Prop. I wonder how much of trouble it will be to have this counterexample, like both syntactically (in terms of Lean4 type checking) and semantically (in terms of Lean4 metatheory)?

To me, it seems that you simply need to prevent reduction for terms in Prop and assume them to be equal. This will at least recover the termination of type checking (well, at least refute this particular counterexample of termination of type checking). This can solve the obvious trouble pointed out by the paper.

Pierre-Marie Pédrot said that:

Impredicative SProp breaks SN only when you can eliminate the SProp equality into a non-SProp sort. Otherwise, it's fine.

I'm also unsure about that. I think it is established that equalities in SProp cannot be eliminated into non-SProp (like boolean in SProp has true = false, but if we can eliminate this into non-SProp booleans, we get logical inconsistency), so I assumed this is disallowed in Lean4, but still the paper I linked in the beginning claimed that normalization is broken by their counterexample.