Stream: Miscellaneous

Topic: Discussing Lean's foundations

Michael Soegtrop (Jun 12 2020 at 12:51):

@Bas: can you elaborate a bit on the Lean vs Coq ranking? it is very close but still I would be interested to learn what reasoning is behind that order.

Pierre-Marie Pédrot (Jun 12 2020 at 12:54):

Totally notwithstanding the fact that Lean is written in C++ and just that makes it more suspicious...

Karl Palmskog (Jun 12 2020 at 12:56):

Bas can confirm, but in my mind Gaëtan's experiment showed that Coq's foundations are more flexible than Lean's, and template polymorphism bugs may not help either... so non-type-theorists may have to implicitly trust more stuff.

Pierre-Marie Pédrot (Jun 12 2020 at 12:58):

As a type theorist, I personally consider the foundations of Lean to be broken by default...

Pierre-Marie Pédrot (Jun 12 2020 at 12:58):

At least in Coq you have to opt-in to wreak havoc with the type system

Paolo Giarrusso (Jun 12 2020 at 12:59):

Lean has multiple independent checkers, including one in Haskell, so I recommend ignoring the C++ part.

Paolo Giarrusso (Jun 12 2020 at 13:03):

and if you don't buy Lean foundations or consistency proofs, you're also questioning Mizar (that uses a set theory stronger than ZFC) and probably many of the other systems (does even HOL survive?)

Théo Zimmermann (Jun 12 2020 at 13:11):

Pierre-Marie has repeatedly expressed specific concerns about some properties that Lean developers do not even try to have, but I believe that soundness is not one of them.

Enrico Tassi (Jun 12 2020 at 13:29):

I think they don't have subject reduction which is a property that is typically used to prove soundness.

Enrico Tassi (Jun 12 2020 at 13:41):

Karl Palmskog said:

Bas can confirm, but in my mind Gaëtan's experiment showed that Coq's foundations are more flexible than Lean's, and template polymorphism bugs may not help either... so non-type-theorists may have to implicitly trust more stuff.

This kind of argument is, in my opinion, quite fallacious. If you take the HOL family for example, the kernel does not even understand "nat := S nat | Z". Of course the kernel is smaller, but you also have to trust some other code that does the encoding. IMO the fact that you can encode A in B, does not mean that B is more trustworthy, nor less. It just makes it harder to define where the TCB ends. Especially given that the encodings are often "extra logical" hence they don't even help relating the power of the logics (for example the encoding HOL in Coq needs axioms).

I guess making people conscious that there is no miracle, all tools can be buggy, and some a more rigorous that others, is important. But ranking tools is too hard to me.

Little anegdote: the type checker of Elpi has been incredibly useful in the development of HB. I know for sure (since I wrote it) that it is a hack, unsound and incomplete (I'm so ashamed that I'll rewrite it, at some point...). Morale: even the verification you do with a broken tool can be useful ;-)

Michael Soegtrop (Jun 12 2020 at 13:56):

Pierre-Marie has repeatedly expressed specific concerns about some properties that Lean developers do not even try to have, but I believe that soundness is not one of them.

An interesting formulation ;-)

I wonder how system like Dedukti change this trust landscape. Since an automated translation from one logic to another would not be trustworthy, one would have to manually check the top level specs in the translated form. I can imagine that this is simpler if the source logic is more expressive because the specifications would allow a more natural encoding of specifications.

Paolo Giarrusso (Jun 13 2020 at 12:55):

I know issues about Lean have been raised, but I’m unconvinced that impredicative type theory has a better story, and I’m unsure if “impredicative Prop” is predicative enough for this discussion.

Paolo Giarrusso (Jun 13 2020 at 12:57):

AFAIK, outside of predicative type theory, the normal way to prove soundness and consistency relies on a stronger metatheory — which is what happens for Lean and non-type theoretic systems — including HOL, I expect?
Now, impredicative type theories (up to Coq with impredicative Set) does that too — consistency relies on strong normalization which relies on an impredicative metatheory!

Paolo Giarrusso (Jun 13 2020 at 13:02):

The only arguably-better story which I’ve seen is predicative type theory with Martin-Löf’s meaning explanation. You might be able to model proof-irrelevant impredicative Prop with a boolean model in a predicative metatheory — but does that scale to full Coq with cumulativity etc.? Otherwise, I’m not sure why I should trust Coq more than Lean.

Bas Spitters (Jun 13 2020 at 13:04):

As we all know, due to @Gaëtan Gilbert , coq is a great type checker for lean.

Pierre-Marie Pédrot (Jun 13 2020 at 13:15):

@Paolo G. Giarrusso my personal problem with Lean is not predicativity vs. impredicativity. I am fairly confident about impredicativity actually, and never quite understood why the Swedish school of constructive mathematics were that traumatized by it. Heck, I actually have no problem with ZFC + whatever big cardinal assumption as far as soundness goes.

No, my grudge against Lean is that you can't really trust the computational content of the proofs because of the lack of decidable type-checking and the subsequent loss of subject reduction. You pick a term, you compute with it, and it might happen that the result doesn't even type-check.

Enrico Tassi (Jun 13 2020 at 13:18):

Pierre-Marie Pédrot said:

Paolo G. Giarrusso my personal problem with Lean is not predicativity vs. impredicativity. I am fairly confident about impredicativity actually, and never quite understood why the Swedish school of constructive mathematics were that traumatized by it.

Because at some point they proposed an impredicative system that was broken ;-)

Pierre-Marie Pédrot (Jun 13 2020 at 13:18):

Fair enough, but then this is entering a Freudian territory.

Enrico Tassi (Jun 13 2020 at 13:18):

Indeed

Pierre-Marie Pédrot (Jun 13 2020 at 13:19):

LISP got static binding wrong, that's not a reason to reject higher-order functions on those grounds...

Pierre-Marie Pédrot (Jun 13 2020 at 13:20):

I think it's still an open problem whether System F can be proved SN predicatively.

Pierre-Marie Pédrot (Jun 13 2020 at 13:20):

As far as my personal beliefs go, I have no doubt that System F is SN...

Enrico Tassi (Jun 13 2020 at 13:20):

I agree, I was mostly joking

Kenji Maillard (Jun 13 2020 at 13:20):

@Pierre-Marie Pédrot If you use the "idealized" non-decidable conversion rule that lean is theoretically using, won't you recover subject reduction ? Or is there another obstruction beside the impossibility in general to re-typecheck an evaluated term ?

Pierre-Marie Pédrot (Jun 13 2020 at 13:21):

@Kenji Maillard yes, you can pick your poison: non decidable type-checking or no SR.

Kenji Maillard (Jun 13 2020 at 13:21):

Well, I'm usually fine with having a theoretical SR

Pierre-Marie Pédrot (Jun 13 2020 at 13:21):

but this claim that there is the idealized system and the actual implementation is nonsense to me

Kenji Maillard (Jun 13 2020 at 13:22):

I mean I won't try to retypecheck an evaluated term because it will often be impractical, no ?

Pierre-Marie Pédrot (Jun 13 2020 at 13:22):

@Kenji Maillard then you also break computation in some sense

Pierre-Marie Pédrot (Jun 13 2020 at 13:22):

it's not necessarily reduction, it pervades into conversion actually

Pierre-Marie Pédrot (Jun 13 2020 at 13:23):

this brings in the same kind of issues that ETT has

Pierre-Marie Pédrot (Jun 13 2020 at 13:23):

i.e. you can apply computational equations to the term but there is no reason that they are equi-typable

Kenji Maillard (Jun 13 2020 at 13:24):

hm, you mean if $\Gamma \vdash A \,ok$ and $A \equiv B$ you don't necessarily have $\Gamma \vdash B ok$ ?

Pierre-Marie Pédrot (Jun 13 2020 at 13:24):

so in practice you made the whole computational content of the theory highly dubious

Pierre-Marie Pédrot (Jun 13 2020 at 13:24):

@Kenji Maillard yep

Enrico Tassi (Jun 13 2020 at 13:25):

It wold be worse if you had A ok, A = B, B ko ;-)

Enrico Tassi (Jun 13 2020 at 13:25):

as in PHP

Kenji Maillard (Jun 13 2020 at 13:27):

I'm still a bit puzzled: Isn't it just that the typechecking algoritm and the conversion procedure are not complete with respect to their specs ?

Paolo Giarrusso (Jun 13 2020 at 13:27):

Yeah, won’t you get B okay using the “idealized system”? (I don’t care for decidable complete typechecking either)

Enrico Tassi (Jun 13 2020 at 13:34):

Kenji Maillard said:

I'm still a bit puzzled: Isn't it just that the typechecking algoritm and the conversion procedure are not complete with respect to their specs ?

I guess that is more like "they can't be"

Kenji Maillard (Jun 13 2020 at 13:34):

Well I do think that being complete is an important property (also in practice): when your program does not typecheck you know that the problem is either in the program itself or it's a bug of the typechecker (possibly a performance bug)

Pierre-Marie Pédrot (Jun 13 2020 at 13:38):

Completeness defines the type theory

Pierre-Marie Pédrot (Jun 13 2020 at 13:38):

I really don't understand the claim that Lean as implemented is an approximation of the idealized theory.

Pierre-Marie Pédrot (Jun 13 2020 at 13:39):

It's just not true, they are two different theories.

Kenji Maillard (Jun 13 2020 at 13:44):

I guess that is more like "they can't be"

Fair enough :)

Completeness defines the type theory

Do you mean that there are cases where $\Gamma \vdash_{ideal} t : A$ holds but the lean typechecker will say $\Gamma \not\vdash_{lean} t : A$ instead of saying that it is unable to answer in finite time ?

Pierre-Marie Pédrot (Jun 13 2020 at 13:44):

Have you heard about the halting problem?

Kenji Maillard (Jun 13 2020 at 13:45):

I think someone told me about these kind of horror stories when I was a kid ^^

Kenji Maillard (Jun 13 2020 at 13:52):

but I still don't see how it applies here (sorry to be so slow; or maybe just ignorant).
If you have a program that you try to typecheck for an intrisically semi-decidable type system you could have 3 kinds of outputs:

• the program typechecks fine and you return a derivation witnessing it
• the program does not typecheck and you can build a proof that no derivation exists
• you timeout: with the ressources you were provided you couldn't achieve neither of the two goals before

(I'm assuming that you want to write a total typechecker of course)

Pierre-Marie Pédrot (Jun 13 2020 at 13:55):

I don't understand how having a tri-valued function helps...

Kenji Maillard (Jun 13 2020 at 13:58):

I'm trying to understand what you mean by "completeness defines the type theory": this tri-valued function does not define any type theory but it would still validate the spec of the undecidable type theory.

Pierre-Marie Pédrot (Jun 13 2020 at 13:59):

I don't understand how you define the "practical" type theory

Pierre-Marie Pédrot (Jun 13 2020 at 13:59):

you can always semi-decide that something is in the idealized type theory, I agree

Pierre-Marie Pédrot (Jun 13 2020 at 14:00):

but the stuff that says I don't know you never really know

Kenji Maillard (Jun 13 2020 at 14:01):

Is there such a thing as a "practical" type theory in that case ?
Or rather where is that essentially needed when we work with type theory ?

Kenji Maillard (Jun 13 2020 at 14:01):

Pierre-Marie Pédrot said:

but the stuff that says I don't know you never really know

Happens :shrug:

Pierre-Marie Pédrot (Jun 13 2020 at 14:01):

I think this is entering the realm of philosophy

Kenji Maillard (Jun 13 2020 at 14:02):

please no, I meant on a practical ground

Kenji Maillard (Jun 13 2020 at 14:02):

In particular with respect to your earlier claim that computation was broken in some sense

Pierre-Marie Pédrot (Jun 13 2020 at 14:03):

My claim is the following: in the "practical" type theory whatever it means, conversion incurs arbitrary needs of fuel

Kenji Maillard (Jun 13 2020 at 14:03):

100% Agreed

Pierre-Marie Pédrot (Jun 13 2020 at 14:04):

So this means that you cannot really be sure about the validity of conversion

Pierre-Marie Pédrot (Jun 13 2020 at 14:04):

so by reducing stuff you actually lose some bits of confidence

Kenji Maillard (Jun 13 2020 at 14:05):

You cannot be sure of the absence of conversion: is that used anywhere in type theory ?

Pierre-Marie Pédrot (Jun 13 2020 at 14:05):

I don't think so, type theory should be monotonic w.r.t. conversion

Pierre-Marie Pédrot (Jun 13 2020 at 14:05):

except that it's not clear with strict proposition

Kenji Maillard (Jun 13 2020 at 14:06):

Pierre-Marie Pédrot said:

except that it's not clear with strict proposition

how so ?

Pierre-Marie Pédrot (Jun 13 2020 at 14:06):

I am not sure

Pierre-Marie Pédrot (Jun 13 2020 at 14:07):

But the root of the undecidability is the fact that you can eliminate SProp Acc into Type

Pierre-Marie Pédrot (Jun 13 2020 at 14:08):

In ETT, you're not monotonic because you can invoke conversions that have logical contents not present in the term

Pierre-Marie Pédrot (Jun 13 2020 at 14:08):

For Lean, I don't know

Paolo Giarrusso (Jun 13 2020 at 14:36):

I knew somebody would bring up “decidable typechecking” as a practical problem, as if Coq commands were terminating in feasible time; and I don’t talk of Ltac loops, just of typeclass search and unification.

Gaëtan Gilbert (Jun 13 2020 at 14:40):

ETT looks monotonic AFAICT

Kenji Maillard (Jun 13 2020 at 17:31):

@Paolo G. Giarrusso In practice both Coq and Lean have similar practical limitations in their implementations. That's why I would like to understand better the theoretical consequences of a type theory where typechecking is only semi-decidable and not decidable.

Enrico Tassi (Jun 13 2020 at 18:54):

I could pass proofs from Coq to Matita and see the inability to type check them as a bug in Matita (or more interestingly a soundness bug in Coq)? If I try to write a third party checker for a tool based on an undecidable type theory, what can I really conclude from a failt to check?

Paolo Giarrusso (Jun 13 2020 at 19:01):

I assume Lean’s existing third-party checkers must use the same algorithm, and if a proof is rejected, you must fix it (like with Coq).

Enrico Tassi (Jun 13 2020 at 19:03):

As far as I know the importer from Lean to Coq turns conversion-checking off, right @Gaëtan Gilbert ?

Paolo Giarrusso (Jun 13 2020 at 19:04):

To me, the problem with undecidable type systems is how to formally test whether they’re “good enough” — clearly it’d be bad if the typechecker always looped, but that’s not what happens.

Enrico Tassi (Jun 13 2020 at 19:04):

Paolo G. Giarrusso said:

I assume Lean’s existing third-party checkers must use the same algorithm, and if a proof is rejected, you must fix it (like with Coq).

"third party" and "same algorithm" in the same sentence is funny ;-)

Paolo Giarrusso (Jun 13 2020 at 19:05):

Hm, same “actual” type system, at least.

Enrico Tassi (Jun 13 2020 at 19:05):

(we had for a long time an "independent checker" using "the same code" in Coq, so no pun intended)

Paolo Giarrusso (Jun 13 2020 at 19:06):

Has that changed now?

Enrico Tassi (Jun 13 2020 at 19:07):

no, but at least it is now documented as such I believe (CC @Maxime Dénès ), no claims of independence

Paolo Giarrusso (Jun 13 2020 at 19:08):

In Lean’s case, I guess you could formalize a translation from the “ideal” type system to the “actual” one (that adds more “annotations” of some sort), and inspect the translation (since it’s something the user might have to do on occasion)

Enrico Tassi (Jun 13 2020 at 19:08):

Today an independent checker would be Dedukti, there everything is very different!

Paolo Giarrusso (Jun 13 2020 at 19:10):

Dedukti + CoqInE if/when it’s completed, right?

Enrico Tassi (Jun 13 2020 at 19:11):

yes something like that. But my point was the independence, not the actual state of the tool

Paolo Giarrusso (Jun 13 2020 at 19:12):

Sure. On such a translation for Lean, I haven’t actually seen one for Lean, but it could probably be extracted from Carneiro’s master thesis with some work.

Gaëtan Gilbert (Jun 13 2020 at 19:27):

Enrico Tassi said:

As far as I know the importer from Lean to Coq turns conversion-checking off, right Gaëtan Gilbert ?

Not in general. It's pretty slow so turning conversion checking off is useful eg to see if it will bug on terms which depend on terms that don't reasonably-terminate, but it's meant to succeed even when checking conversion.

Pierre-Marie Pédrot (Jun 13 2020 at 20:16):

you could formalize a translation from the “ideal” type system to the “actual” one

This is the way to justify ETT into ITT + UIP + funext, but there is something I judge wrong with that that I can't pinpoint

Pierre-Marie Pédrot (Jun 13 2020 at 20:17):

because this translation is not compatible with reduction in the sense that if you reduce a term you don't necessarily know how to retrieve a correctness derivation for the reduced term

Pierre-Marie Pédrot (Jun 13 2020 at 20:17):

I think that Théo Winterhalter's PhD has more formal complaints about this

Pierre-Marie Pédrot (Jun 13 2020 at 20:19):

so once again, if you only care about soundness this is moot

Last updated: Jun 05 2023 at 09:01 UTC