Stream: Coq users

Topic: Axioms Vs Inductive definitions


view this post on Zulip walker (May 18 2022 at 11:46):

I noted that all the the definitions that are inductively defined can also be defined as sepaarate Axioms and vice versa for instance the axioms of Hoare logic can be inductively defined in Coq, So when would the usage of axioms be different from inductive definition (I am asking from the logic perspective).

view this post on Zulip Ali Caglayan (May 18 2022 at 11:48):

Axioms don't have the ability to be destructed by a match statement.

view this post on Zulip Ali Caglayan (May 18 2022 at 11:49):

For instance you can do:

Axiom nat : Type.
Axiom O : nat.
Axiom S : nat -> nat.

But you won't be able to define a function on nat by cases and reduce it.

view this post on Zulip Ali Caglayan (May 18 2022 at 11:51):

Also, if you care about that sort of thing, inductive types are generally constructable out of sigma types and nat which means they exist in models of type theory, e.g. Set. By assuming axioms you have no guarantee that there is indeed an object that acts this way.

view this post on Zulip Ali Caglayan (May 18 2022 at 11:52):

Actually more important than functions is the fact that you have no dependent functions i.e. no induction principle. Natural numbers without induction aren't very good at proving much.

view this post on Zulip walker (May 18 2022 at 11:56):

What about the otherway around something that are axiomatic by nature but then it gets represented by inductive types such as axioms of hoare logic, or separation logic ? I think those do work as axioms on their own yet when developed in coq they are not presented as axioms

view this post on Zulip Ali Caglayan (May 18 2022 at 11:57):

People define "axioms of logic" all the time using inductive types. However don't conflate the two uses of the word axiom here. One is about the metatheory (Coq) the other has only the meaning you intend to give it. :-)

view this post on Zulip Ali Caglayan (May 18 2022 at 12:00):

It's the same as usual mathematics: When formalizing Set theory in ZFC you never assume extra axioms on top of ZFC to talk about models of set theory, you simply have a set of sentences which you term "axioms".

view this post on Zulip Ali Caglayan (May 18 2022 at 12:01):

A simpler example is Peano arithmetic, which is just a list of arithmetic statements you expect should hold and these are termed axioms.

view this post on Zulip walker (May 18 2022 at 12:01):

because those are provable in ZFC,

view this post on Zulip walker (May 18 2022 at 12:02):

But axiom of choice is not povable in ZF so they decided to add when when they need it.

view this post on Zulip walker (May 18 2022 at 12:02):

I assume that hoare logic axioms are not provable in CIC so why was "lets assume CIC + hoare logic axioms" not the way to go ?

view this post on Zulip walker (May 18 2022 at 12:03):

also I could be wrong, I am just trying to understand why no one did it

view this post on Zulip Karl Palmskog (May 18 2022 at 12:03):

here is what the ANSSI guide to reviewing Coq code says about axioms:

The introduction of an axiom is delicate, as it may result in making the Coq logic inconsistent. Besides, certain “standard axioms” are known to be inconsistent with Coq logic (e.g., the axiom of description together with the excluded middle). However, the standard library of Coq provides several axioms that can be safely added to Coq, according to the Coq FAQ. That being said, the standard library provides the means to avoid using most of these axioms. For instance, e.g., generalized rewriting can be leveraged in place of relying on the proof irrelevance and functional extensionality axioms.

view this post on Zulip Ali Caglayan (May 18 2022 at 12:04):

I think you are getting confused here. When you study "hoare logic" in CIC or set theory, you are not "proving its axioms" that doesn't even make sense in most cases because proof systems can have different languages.

view this post on Zulip Ali Caglayan (May 18 2022 at 12:05):

You can sit down and foramlize the syntax of "hoare logic" in CIC or set theory, and then prove things about it. But the metatheory and theory of hoare logic don't coincide.

view this post on Zulip Ali Caglayan (May 18 2022 at 12:06):

That's how logic is typically studied in mathematics.

view this post on Zulip Ali Caglayan (May 18 2022 at 12:06):

Of course there are ways to make the metatheory and theory coincide (somewhat) but this is quite a complicated and delicate topic.

view this post on Zulip walker (May 18 2022 at 12:07):

Where can I read more about that ?

view this post on Zulip Ali Caglayan (May 18 2022 at 12:09):

Well there are efforts to formalize the CIC in CIC such as metacoq https://github.com/MetaCoq/metacoq and in mathematical logic you have "formal theories of truth" or "axiomatic theories of truth". I would warn you however, none of this would make much sense without having studied some logic first.

view this post on Zulip walker (May 18 2022 at 12:10):

I assume boolean logic does not qualify ?

view this post on Zulip Ali Caglayan (May 18 2022 at 12:10):

If you learn about Godels incompleteness theorem, then you can see these as efforts to thwart it as much as possible.

view this post on Zulip Ali Caglayan (May 18 2022 at 12:11):

If by boolean logic you mean propositional logic, then probably not since it is too weak to begin talking about its own metatheory.

view this post on Zulip walker (May 18 2022 at 12:12):

understood, then I got lots of reading to do, sadly..

view this post on Zulip Karl Palmskog (May 18 2022 at 12:12):

I think the key point is that however you define an inductive type, you won't get unsoundness because of it (so far as we know, in the current Coq implementation). But it takes just one Axiom line to get an unsound system.

view this post on Zulip Ali Caglayan (May 18 2022 at 12:13):

Karl Palmskog said:

I think the key point is that however you define an inductive type, you won't get unsoundness because of it (so far as we know, in the current Coq implementation). But it takes just one Axiom line to get an unsound system.

Right, this is what I hinted at when I talked about models earlier up.

view this post on Zulip Karl Palmskog (May 18 2022 at 12:13):

some systems such as HOL don't even have inductive types built in, instead you have to use "definitional packages" to get something resembling inductive types (but which are just regular stuff, no special status)

view this post on Zulip Ali Caglayan (May 18 2022 at 12:13):

My advice would be read up on Godel's incompleteness theorems since they will pull in most of the logical theory you need.

view this post on Zulip walker (May 18 2022 at 12:14):

Ali Caglayan said:

Karl Palmskog said:

I think the key point is that however you define an inductive type, you won't get unsoundness because of it (so far as we know, in the current Coq implementation). But it takes just one Axiom line to get an unsound system.

Right, this is what I hinted at when I talked about models earlier up.

My problem is I cannot intuit the reason that gives inductive types this advantage.

view this post on Zulip walker (May 18 2022 at 12:14):

Ali Caglayan said:

My advice would be read up on Godel's incompleteness theorems since they will pull in most of the logical theory you need.

I will start by reading about that, thanks a lot!

view this post on Zulip Ali Caglayan (May 18 2022 at 12:15):

walker said:

Ali Caglayan said:

Karl Palmskog said:

I think the key point is that however you define an inductive type, you won't get unsoundness because of it (so far as we know, in the current Coq implementation). But it takes just one Axiom line to get an unsound system.

Right, this is what I hinted at when I talked about models earlier up.

My problem is I cannot intuit the reason that gives inductive types this advantage.

If I write down an inductive types there is a "process" that lets me turn it into an equivalent type made out of simpler type formers such as sigma types and the natural numbers. Those are constructable in models of type theory hence it is consistent to assume inductive types exist (they have a possible implementation always).

view this post on Zulip Ali Caglayan (May 18 2022 at 12:16):

There is no guarantee when I write down an axiom, I am just assuming it.

view this post on Zulip Ali Caglayan (May 18 2022 at 12:16):

For instance I can write Axiom oops : 0 = 1. and this wouldn't be great for my formalization since I can derive falsehood and prove anything.

view this post on Zulip Ali Caglayan (May 18 2022 at 12:17):

There are much less obvious axioms which one could assume, that could unintentionally lead to contradictions.

view this post on Zulip Ali Caglayan (May 18 2022 at 12:17):

Hence what Karl said.

view this post on Zulip walker (May 18 2022 at 12:18):

understood, I will read about the incompleteness theorem (I vaguely know what is it about but I think I will read the proof now) and move from there.

view this post on Zulip Paolo Giarrusso (May 18 2022 at 17:50):

I'm not sure I understand why the Gödel theorems are relevant to Hoare logic...

view this post on Zulip Paolo Giarrusso (May 18 2022 at 17:53):

Ali Caglayan said:

I think you are getting confused here. When you study "hoare logic" in CIC or set theory, you are not "proving its axioms" that doesn't even make sense in most cases because proof systems can have different languages.

To me, of course you want to "prove the axioms of Hoare logic" — by giving a model

view this post on Zulip Karl Palmskog (May 18 2022 at 17:56):

hmm, I thought one could justify Hoare logic rules by giving a WP calculus and proving relative completeness, etc.

view this post on Zulip Karl Palmskog (May 18 2022 at 17:58):

the whole "giving a model" stuff sounds separation logic-y

view this post on Zulip Paolo Giarrusso (May 18 2022 at 18:52):

Separation logic is a kind of Hoare logic, and for this discussion I think they are the same thing.

view this post on Zulip Paolo Giarrusso (May 18 2022 at 18:56):

Iris treats { P } e { Q } as a notation for P -* WP e { Q }, so I don't know if translating between the two notations is a very interesting proof?

view this post on Zulip Paolo Giarrusso (May 18 2022 at 18:58):

there might be another cultural divide elsewhere, but a more interesting proof seems the one relating "axiomatic semantics" to e.g. operational semantics.

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:01):

or to the "canonical" semantics for your programming language (the one that's the official "language definition"), whatever that is.

view this post on Zulip Karl Palmskog (May 18 2022 at 19:05):

but if you define P e Q using a WP calculus, then your Hoare "rules" are not axioms anyway. To me, it's fine to make the WP calculus definition the canonical semantics. But sure, it's a form of validating/justifying one form of semantics if you relate it to another form

view this post on Zulip Karl Palmskog (May 18 2022 at 19:08):

but a WP calculus is a form of characterization of the state you get after running a program. It's an unambiguous description that could be used by a compiler implementer. Where does the model stuff come in? Is it really needed?

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:09):

because of that notational, I'm not sure what's the difference between Hoare logic and WP semantics. Are you saying that people would choose different axioms in the two?

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:09):

(I'd say the standard Hoare rules for loops seem something I'd want to prove and not a primitive)

view this post on Zulip Karl Palmskog (May 18 2022 at 19:11):

in my reading of the classic presentation, the Hoare logic rules are taken as given "from nothing". You could/should declare them axiomatically as a bunch of logical implications.

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:12):

sure, that seems mostly a stylistic choice. You can take those as primitive or prove them sound relative to an operational semantics.

view this post on Zulip Karl Palmskog (May 18 2022 at 19:12):

then people figure out that this WP stuff, with an actual predicate transformer function, is actually a better way to do it, both in implementation and in formalization

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:13):

one Hoare-separation difference is that it's probably more reasonable to take a Hoare logic than a modern separation logic as primitive — with some emphasis on "modern"

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:14):

but a WP calculus is a form of characterization of the state you get after running a program.

I don't think that's of the WP rules in Iris, but that might be on the "modern separation logic" part in Iris

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:16):

I just checked software foundations, and they indeed use a shallow embedding of Hoare logic using operational semantics: https://softwarefoundations.cis.upenn.edu/plf-current/Hoare.html#hoare_triple

view this post on Zulip Karl Palmskog (May 18 2022 at 19:18):

yeah, I guess you can do that, but that's not how it's done classically I believe? the most convincing formalizations separate each semantic approach and have standalone theorems connecting them

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:19):

I'm not pushing strongly for shallow embeddings, just saying "here's a common textbook which gives a model for Hoare logic"

view this post on Zulip Karl Palmskog (May 18 2022 at 19:20):

ah OK, so that's what you mean by give a model in this context

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:21):

yep, that's what we do in separation logics as well

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:21):

I wasn't hinting at domain-theoretic denotational semantics or anything like that :sweat_smile:

view this post on Zulip Karl Palmskog (May 18 2022 at 19:22):

but we agree that one could just as well take the Hoare-sep-log as primitive, and prove the opsem "correct" by giving it a "Hoare model"? Or one might say: interpreting the opsem in terms of Hoare-sep-log

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:24):

yes, tho I confess I wouldn't know how to set that up — but I recall Mitchell's Foundations of Programming Languages shows both directions?

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:25):

in practice, if you used Iris, then Iris experts might object strongly but for other reasons (and I suspect the same could be true in other such logics)

view this post on Zulip Karl Palmskog (May 18 2022 at 19:26):

hmm, but couldn't I write my WP calculus / predicate transformer separately from Iris?

view this post on Zulip Karl Palmskog (May 18 2022 at 19:26):

and then just plug it in and get proof mode stuff?

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:27):

re proofmode: yes but let's set that aside

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:30):

re "separate WP calculus", wikipedia's example has an imperative language without aliasing, which simplifies questions a bit too much

view this post on Zulip Karl Palmskog (May 18 2022 at 19:31):

my naive understanding has been that if I bring with me some PL semantics in some reasonable form, I can get something close to "my own VST" from Iris, i.e., a Hoare interface of sorts to prove my before-after specs for stateful programs

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:32):

Iris is a flexible framework, but the Iris program logics proper demands specifically an operational semantics

view this post on Zulip Karl Palmskog (May 18 2022 at 19:33):

ah, so the Iris WP calc is "fixed" and based on the operational semantics parameter?

view this post on Zulip Karl Palmskog (May 18 2022 at 19:33):

that's a bit less flexible than I expected

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:34):

the definition of WP by the core program logic is fixed and based on operational semantics; the "actual WP calculus" is something that you derive on top...

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:34):

but also

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:34):

you _can_ swap out the program logics with something else.

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:35):

you can just reuse the proofmode (as you said), or you can also reuse the Iris base logic (which gives you step-indexing, higher-order ghost state, etc.)

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:36):

I think the main rub is that nobody knows how to make sense of _step-indexing_ without steps

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:37):

and that there are too many ways to write fancy theorems which amount to True or False -> ...

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:38):

(a funny way to write True is ∃ i, \later^i False)

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:39):

just for reference, the abstract https://drops.dagstuhl.de/opus/volltexte/2017/7275/ also mentions that Iris relies on some operational semantics:

Iris only applies to languages with an operational interleaving semantic

view this post on Zulip Karl Palmskog (May 18 2022 at 19:39):

hmm, I think this is the problem with these separation logic specs, there are so many fancy built-in predicates it's really hard to follow what's going on

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:39):

yeah that's basically it

view this post on Zulip Karl Palmskog (May 18 2022 at 19:40):

ah, interesting, then also the Nuprl style "logic of events" is ruled out (based on happens-before relation rather than interleaving)

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:41):

and there are tons of "obviously true" rules which are unsound — if you store propositions P in ghost state, for instance, you can't read them precisely

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:42):

more accurately: if you store step-indexed predicates in ghost state :wink:

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:42):

I don't know that logic of events but I've seen happens-before for concurrency, and that paper transforms indeed such an axiomatic semantics (for C/C++/...) into an operational one to apply Iris on top.

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:45):

anyway, you shouldn't worry about those fancy predicates for Iris works: they apply Iris adequacy to end up with Iris-free top-level theorems about operational semantic traces

view this post on Zulip Karl Palmskog (May 18 2022 at 19:47):

I think I would be happy with trace properties as a final deliverable regardless of whether they came out of an operational semantics or not. Nakata and Uustalu even did a Hoare logic over traces, so it should be doable in Iris?

view this post on Zulip walker (May 18 2022 at 19:49):

/me trying to follow the dicussion, the problem is there are things I don't know and I don't even know what they are.

view this post on Zulip Karl Palmskog (May 18 2022 at 19:51):

the recent discussion has been about programming language theory, in particular programming language semantics. I think it's a bit unfortunate that Hoare conflated his particular PL semantics style with "logic" and "axioms"

view this post on Zulip Karl Palmskog (May 18 2022 at 19:52):

I think there are other semantics styles that could just as well be said to be about logic, such as denotational

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:53):

@walker sorry for hijacking the discussion, this discussion is probably not the most accessible

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:54):

but back to your questions, it's not impossible that Gödel's theorems are relevant, I just guess they're unlikely to be especially relevant depending on what you want to do

view this post on Zulip Paolo Giarrusso (May 18 2022 at 19:55):

maybe if you say a bit more we can be more helpful

view this post on Zulip walker (May 18 2022 at 19:59):

So let me see, I was watching prof Dreyer talking once about Iris and saying that the problem with previous separation logic is that have complex axioms, but then When I read an iris journal paper for iris 3, The axioms (I am not even sure if that is the right name) are really really complex. So I thought that perhaps a better approach would be to extend CIC to reason about pointer accesses given that CIC is powerful, this might be similar to the way typed lambda calculus was extended with inductive constructions to form CIC. But given my theoretical knowledge is really shallow, I wanted to know why didn't anyone do that before.

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:00):

walker said:

I assume that hoare logic axioms are not provable in CIC so why was "lets assume CIC + hoare logic axioms" not the way to go ?

https://softwarefoundations.cis.upenn.edu/plf-current/Hoare.html "proves the axioms" of Hoare logic

view this post on Zulip walker (May 18 2022 at 20:01):

it feels to me that they didn't prove it, they modeled it ?

view this post on Zulip walker (May 18 2022 at 20:02):

isn't it possible to also model unsound logic rules the same way ?

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:02):

no you can't model unsound logics

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:03):

or rather: the point of a modeling logic A (hoare logic) in logic B (Coq) is to prove relative soundness: if A is unsound, then B is unsound as well!

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:04):

From another POV:

So I thought that perhaps a better approach would be to extend CIC to reason about pointer accesses given that CIC is powerful, this might be similar to the way typed lambda calculus was extended with inductive constructions to form CIC.

When people add rules to CIC, they also write complex proofs to make sure those rules are sound.

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:05):

Finally, people _have_ built tools that take complex separation logics as primitive rules. The only question is whether those axioms are true.

view this post on Zulip walker (May 18 2022 at 20:06):

Paolo Giarrusso said:

When people add rules to CIC, they also write complex proofs to make sure those rules are sound.

Are these proofs something different from the local soundness and local completeness proofs (eliminating introductions and going the other way round)?

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:07):

it sounds like you're referring to Pfenning's concepts? Those are different indeed.

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:07):

(deleted)

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:07):

sorry

view this post on Zulip walker (May 18 2022 at 20:07):

Paolo Giarrusso said:

it sounds like you're referring to Pfenning's concepts? Those are different indeed.

Yes I learned it from one of his lectures.

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:08):

Reposting:

Finally, people _have_ built tools that take complex separation logics as primitive rules. The only question is whether those axioms are true.

... It's a bit as if somebody wrote rules as complex as those of Iris, said "these rules are obviously sound", and skipped writing a proof.

view this post on Zulip walker (May 18 2022 at 20:08):

Paolo Giarrusso said:

Reposting:

Finally, people _have_ built tools that take complex separation logics as primitive rules. The only question is whether those axioms are true.

... It's a bit as if somebody wrote rules as complex as those of Iris, said "these rules are obviously sound", and skipped writing a proof.

yes I understand.

view this post on Zulip walker (May 18 2022 at 20:09):

one last question, so what is the problem with Pfenning's concepts approach to soundness and completeness proofs?

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:10):

there's no problem, but the soundness in "local soundness" is just a different thing.

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:10):

(I'm not even entirely sure why it has that name...)

view this post on Zulip walker (May 18 2022 at 20:11):

I understand ... thanks for the discussion I will do a bit more research/ learning.

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:11):

I should take back the last answer; I'm not entirely sure

view this post on Zulip walker (May 18 2022 at 20:12):

If I recall correctly he always talked about local soundeness vs global soundness but never mentioned what that global soundness is.

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:12):

but "soundness" in general means "you can't prove False", and for a logic as complex as Coq you can't just prove local soundness

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:14):

for instance, Coq's soundness is proven by showing that there's all proofs can be normalized, and that there's no proof of False in normal form

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:14):

(oversimplifying quite a bit!)

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:14):

"no proof of False in normal form" is typically easy

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:15):

"all proofs can be normalized" is very hard

view this post on Zulip walker (May 18 2022 at 20:15):

Paolo Giarrusso said:

but "soundness" in general means "you can't prove False", and for a logic as complex as Coq you can't just prove local soundness

It is funny because Coq's logic looks deceivingly simple and very very small so I would never think of it as complex until I hear from people or go read papers about metacoq.

view this post on Zulip Gaëtan Gilbert (May 18 2022 at 20:17):

https://coq.github.io/doc/master/refman/language/core/inductive.html#theory-of-inductive-definitions is not that simple or small

view this post on Zulip Gaëtan Gilbert (May 18 2022 at 20:17):

imo

view this post on Zulip walker (May 18 2022 at 20:19):

the notion looks complex, but I assumed they are the ones here https://hal.inria.fr/hal-01094195/document

view this post on Zulip Karl Palmskog (May 18 2022 at 20:22):

nearly all of us want inductive types to get our work done. So we can either choose to build inductive types from inside the logic (lots of encoding work), or the designers of the logic can make inductive types primitive. If we do the latter, the designers and implementers of the logic have a lot of work to prove soundness. With a logic without inductive types, we have to do work over and over to get inductive types, but we know we are sound without extra work.

view this post on Zulip Ali Caglayan (May 18 2022 at 20:25):

Paolo Giarrusso said:

I'm not sure I understand why the Gödel theorems are relevant to Hoare logic...

I mentioned Godel not because I know anything about Hoare, but because it highlights the difficulties in formalizing logic in logic. The question from before was roughly "where can I learn about logics who are their own meta theory" and I replied with some pointers but that in order to appreciate them, studying Godel is a good first step.

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:27):

@Karl Palmskog we know they’re sound, but I’ve seen people point out that “do they have the right meaning?” can be tricky (e.g. Enrico I think brought that up?)

view this post on Zulip Karl Palmskog (May 18 2022 at 20:29):

I agree, if you make inductive types primitive, there are many ways that can be sound but useless/strange

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:29):

Enrico’s point was about the encodings

view this post on Zulip Karl Palmskog (May 18 2022 at 20:30):

OK, a logic like HOL is to me a very "extensional" logic - one shouldn't really look inside, just take stuff at face value.

view this post on Zulip Karl Palmskog (May 18 2022 at 20:31):

so most of the time, you don't really care that these encodings of inductive types are super convoluted, because the system shields you from the horrible details

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:31):

But what happens if the elaboration in HOL is buggy?

view this post on Zulip Karl Palmskog (May 18 2022 at 20:31):

I can definitely see that in a "non-extensional" theory like Coq's, bad encodings can make the whole thing crumble

view this post on Zulip Karl Palmskog (May 18 2022 at 20:32):

I mean, someone can correct me here, but HOL really doesn't do much elaboration, at least it's very modest [compared to Coq]

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:32):

You know HOL better than me, but in principle a buggy encoding could let you prove 0 = 1, right?

view this post on Zulip Karl Palmskog (May 18 2022 at 20:33):

every definition has to go through the core operations

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:33):

Of course, but that doesn’t prevent Pollack inconsistency

view this post on Zulip Karl Palmskog (May 18 2022 at 20:33):

OK, sure, yes, HOL doesn't protect from that

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:34):

And maybe 0 = 1 holds because the code that encodes inductive types has a Pollack-inconsistency bug,

view this post on Zulip Karl Palmskog (May 18 2022 at 20:34):

hmm, not immediately obvious, but, maybe?

view this post on Zulip Karl Palmskog (May 18 2022 at 20:35):

I have a colleague who works on soundness of Isabelle/HOL kernel, can ask him at some point

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:36):

IIUC, this isn't about the "kernel"

view this post on Zulip Karl Palmskog (May 18 2022 at 20:36):

the definitional mechanism interacts directly with the kernel

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:37):

but IIUC somebody (@Enrico Tassi ?) was pointing out that HOL does not let you prove 0 = 1, only "crazy encoding of 0 = crazy encoding of 1", so if the crazy encoding is subtly wrong it could produce equivalent results for 0 and 1

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:38):

hence (he said) if you don't check that the crazy encoding did the right thing, you need to treat it as part of your TCB. Which seems pretty much tautological.

view this post on Zulip Karl Palmskog (May 18 2022 at 20:38):

not sure how that would work, but I can't say it's impossible

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:38):

Coq elaboration has the same problem in principle, but people here suggest you should look at the elaboration result for the top-level theorems

view this post on Zulip Paolo Giarrusso (May 18 2022 at 20:39):

(anyway, sorry @walker we digressed again in your thread)

view this post on Zulip walker (May 18 2022 at 21:20):

don't be sorry, I am really enjoying reading stuff.

view this post on Zulip Enrico Tassi (May 19 2022 at 05:32):

I confirm I consider the non trivial encoding of datatypes in HOL part of TCB, exactly as the positivity checker or the termination checker are part of the Coq one. But some Isabelle core devs had different ipinions IIRC last time a loophole was found in their datatype definitiona mechanism (which let you prove false in HOL but not in Pure).

The elboration of Coq can be left out since its output is not totally different than the input, still you can have Pollack's inconsistencies due to notations and stuff like that... but well, that is a matter of UI to me: it is like if vscode would stop colorimg errors in red, not food for logicians :-)

view this post on Zulip Guillaume Melquiond (May 19 2022 at 06:31):

I think Coq's users are a bit too eager to forget that there is a ton of encoding in Coq too. Equality, existential, disjunction, even implication, are all encoded. And there is not even a consensus about this encoding. We had to modify the public API of Coq to please the many users that redefine equality with their own version.

view this post on Zulip Pierre-Marie Pédrot (May 19 2022 at 06:35):

Where do you put the limit between an encoding and a definition then?

view this post on Zulip Guillaume Melquiond (May 19 2022 at 06:38):

There is no limit. There is a continuum. My point was more than, if you actually compare the encoding of 0 = 1 in HOL and Coq, the one in HOL does not look so crazy anymore.

view this post on Zulip Guillaume Melquiond (May 19 2022 at 06:47):

For example, if you take a bunch of students with only basic knowledge of first-order logic, set theory, Peano's arithmetic, etc, I would not be surprised if you can convince them faster that the HOL's encoding of 0 = 1 makes sense.

view this post on Zulip walker (May 19 2022 at 10:32):

quick question, is coq not a HOL ? @Guillaume Melquiond you are putting distinction between both of them ?

view this post on Zulip Enrico Tassi (May 19 2022 at 10:39):

I'm a bit lost, how can you see peano numbers in Coq as encoded? They are literally how you find them on paper.

view this post on Zulip Karl Palmskog (May 19 2022 at 12:04):

"HOL" is usually used to mean a specific higher order logic variant: https://plato.stanford.edu/entries/type-theory-church/

This does not rule out that there are other higher order logics

view this post on Zulip Guillaume Melquiond (May 19 2022 at 12:12):

Enrico Tassi said:

I'm a bit lost, how can you see peano numbers in Coq as encoded? They are literally how you find them on paper.

No, Peano never talked about inductive types. And the equality he used was the primitive one from the logic, not a really strange thing with hard to explain eliminators.

view this post on Zulip Guillaume Melquiond (May 19 2022 at 12:15):

walker said:

quick question, is coq not a HOL ?

And to extend on Karl's answer, what people tend to call HOL (written as such) is the logic used in the HOL family of proof systems: Isabelle/HOL, HOL4, HOL Light, and so on. Coq is completely unrelated to it and follows different paradigms.

view this post on Zulip Enrico Tassi (May 19 2022 at 13:31):

Hum, it did no call it as such because the concept was not there... But the fact that naturals are made of a base symbol and another one meaning the successor is, afaict, very close to what the inductive nat says in Coq. If you start to define plus as a type theoretic function with computational rules the you start to diverge, but you don't need that to write 0=1. And the equal of Coq is the equality of the logic. The inductive incarnates the introduction and elimination of that concept, which is hardcoded (unlike say, setoids). That is technical to explain, sure.

view this post on Zulip Karl Palmskog (May 19 2022 at 15:48):

maybe relevant here, the paper on the verified subset of HOL Light incl user interaction came out: https://cakeml.org/itp22-candle.pdf

It outlines what is typically assumed in a proof assistant implementation (background ZF(C) set theory)


Last updated: Feb 01 2023 at 11:04 UTC