<darktenaibre>
__marioxcc: if you augment Coq's logic with LEM, in terms of equiconsistency, this is essentially ZFC + a scheme to get infinitely many inaccessible cardinals if I'm not mistaken
<__marioxcc>
darktenaibre: Ok. What about the HOL familiy?
<tokenrove>
__marioxcc: you might want to ask about this stuff on channels more oriented around formal methods, like #coq and #isabelle
<__marioxcc>
Ok.
<tokenrove>
i dunno about #coq, but #isabelle is fairly active, enough that you'd probably get answers within a few hours
<__marioxcc>
Thanks you.
copy_ has quit [Quit: Connection closed for inactivity]
<tokenrove>
also, the book "Interactive Theorem Proving and Program Development" was highly recommended to me, so I bought a copy, but haven't had time to read it. it uses coq.
<Armael>
w
<__marioxcc>
Thanks you. I will take a look into it.
<__marioxcc>
tokenrove.
silver has quit [Read error: Connection reset by peer]
pierpa has quit [Quit: Page closed]
sam____ has joined #ocaml
<darktenaibre>
__maroxcc: I'm not familiar enough with the logics there, as far as higher-order logic is concerned, PAω is clearly below ZF; iirc throwing in kind quantification lets you reach ZF in terms of strength
<darktenaibre>
I guess these are mostly curiosity questions ? Unless you are into esoteric pursuits, consistency strength of the systems is not really the main criterion I'd use to differentiate them
<__marioxcc>
darktenaibre: I don't really know what axioms these provers use by deafault.
<__marioxcc>
Well, yes, I'm asking for consistency only because of curiosity.
sam____ has quit [Ping timeout: 268 seconds]
<__marioxcc>
But I'm interested in using proof verifiers for a real-life task, which is formalization of chemical nomenclature.
<darktenaibre>
for someone like me (us?) who have been away for chemistry ever since high-school, this goal is a bit abstract^^
<__marioxcc>
Well, I'm interested in chemistry and a careful reading of the IUPAC "nomenclature of organic chemistry" (blue book) made me realize that we need something more serious than this.
<__marioxcc>
Becuase this one is full of errors.
<__marioxcc>
Not just omissions, but blatant inconsistency.
cmk_zzz has joined #ocaml
<darktenaibre>
mmmm so your goal is to have an algorithm in Coq/whatever which takes as input a labelled graph representing a molecule and output a name according to guidelines as written there (https://en.wikipedia.org/wiki/IUPAC_nomenclature_of_organic_chemistry) and certify it somehow ?
deep-book-gk_ has joined #ocaml
<__marioxcc>
darktenaibre: That is a secondary goal.
<__marioxcc>
First I want to define a function that takes one such graph and outputs one string, which is the preferred name of the compound.
<__marioxcc>
So if X and Y are molecule graphs which are isomorph (including the extra information like element, charge, etc...), then f(X)=f(Y)
<__marioxcc>
I see this as a formalization of chemical nomenclature.
<__marioxcc>
Currently there is no formalization. it's written in vague and very bad written (contains many omissions and contradiction) natural language.
<__marioxcc>
Only once we have a formalization can we write a program to actually compute "f".
<__marioxcc>
Do you have a suggestion of where to start with? What proof verifier, et cetera?
deep-book-gk_ has left #ocaml [#ocaml]
<darktenaibre>
well the property that you are saying is mostly sanity check, but ok, that's what I expected
<__marioxcc>
darktenaibre: Yes, of course, but I want to remark that the current nomenclature is not "sane" at all. It could not be even called a "nomenclature" properly, but only a "vague sketch of a convention".
swalk has joined #ocaml
<__marioxcc>
I have no experience with proof verifiers, except a tiny bit with metamath, so what would you suggest (I mean among Coq, Isabelle, HOL4, ...)?
<darktenaibre>
yep, I imagine you have to invent specs along the way (if I'm not mistaken, some people in PL have to do this while formalizing semantics of languages like C)
<darktenaibre>
I am not well-versed enough in all interactive theorem provers to offer meaningful advice beyond "don't use mizar for this"
<__marioxcc>
Yes, I will attempt to follow the IUPAC text, but I will have to use my own judgement whenever it is ambiguous or contradictory.
<__marioxcc>
Ok. ^.^
<darktenaibre>
all of those that you cite have support for extraction, so I'm guessing they are the most convenient for the goal that you have
<__marioxcc>
I see.
<__marioxcc>
I will be glancing at their respective documentation until I can settle on one.
<darktenaibre>
the only one I am reasonable skill with is coq
<__marioxcc>
Ok. What have you used Coq for, just for curiosity?
<darktenaibre>
nothing too big, I have some encounters with type-theory and curry-howard in my curriculum
<__marioxcc>
*IUPAC standard for organic nomenclature
<__marioxcc>
I have reported some more errors.
<__marioxcc>
What is remarkable here is the sheer amount of errors.
maxton has quit [Quit: My Mac has gone to sleep. ZZZzzz…]
<__marioxcc>
What is funny is that
<__marioxcc>
thare is a program "ACD" that is adverstised by the vendor as a way to avoid human error by generating names of compounds given their graph, but how can it avoid errors if the specification itself is erroneous?
mengu has quit [Remote host closed the connection]
<darktenaibre>
welp, I don't know the field at all, but then are they not trying to push their implementation as a spec ? in a sense, they should already be helping with disambiguation of the rules
<__marioxcc>
"but then are they not trying to push their implementation as a spec ?" ← if you mean saying "the output of this program *defines* the valid nomenclature", then AFAIK, nobody is doing that.
samrat_ has joined #ocaml
enterprisey has joined #ocaml
enterprisey has quit [Remote host closed the connection]
jao has quit [Ping timeout: 255 seconds]
mfp__ has quit [Ping timeout: 260 seconds]
jao has joined #ocaml
samrat_ has quit [Ping timeout: 255 seconds]
samrat_ has joined #ocaml
enterprisey has joined #ocaml
jlam has joined #ocaml
jlam__ has quit [Ping timeout: 255 seconds]
FreeBirdLjj has joined #ocaml
__marioxcc has left #ocaml [#ocaml]
samrat_ has quit [Ping timeout: 248 seconds]
swalk has quit [Quit: swalk]
FreeBirdLjj has quit [Remote host closed the connection]
FreeBirdLjj has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 260 seconds]
sam____ has joined #ocaml
FreeBirdLjj has joined #ocaml
maxton has joined #ocaml
sam____ has quit [Ping timeout: 255 seconds]
copy_ has quit [Quit: Connection closed for inactivity]
samrat_ has joined #ocaml
ocaml079 has joined #ocaml
ocaml079 has quit [Client Quit]
samrat_ has quit [Ping timeout: 260 seconds]
jao has quit [Ping timeout: 240 seconds]
sam____ has joined #ocaml
enterprisey has quit [Read error: Connection reset by peer]
sam____ has quit [Ping timeout: 255 seconds]
maxton has quit [Quit: My Mac has gone to sleep. ZZZzzz…]
maxton_ has joined #ocaml
maxton__ has quit [Ping timeout: 240 seconds]
sam____ has joined #ocaml
sam____ has quit [Ping timeout: 260 seconds]
sam____ has joined #ocaml
michael_ has joined #ocaml
sam____ has quit [Ping timeout: 248 seconds]
samrat_ has joined #ocaml
sam____ has joined #ocaml
tennix has joined #ocaml
MercurialAlchemi has joined #ocaml
sam____ has quit [Ping timeout: 260 seconds]
sam____ has joined #ocaml
michael_ has quit [Remote host closed the connection]
maxton_ has quit [Read error: Connection reset by peer]
sam____ has quit [Ping timeout: 240 seconds]
michael_ has joined #ocaml
sam____ has joined #ocaml
tennix has quit [Remote host closed the connection]
sam____ has quit [Ping timeout: 255 seconds]
sam____ has joined #ocaml
sam____ has quit [Ping timeout: 268 seconds]
sam____ has joined #ocaml
dakk has quit [Ping timeout: 240 seconds]
sam____ has quit [Ping timeout: 248 seconds]
ygrek has joined #ocaml
FreeBirdLjj has quit [Remote host closed the connection]
sam____ has joined #ocaml
sam____ has quit [Ping timeout: 248 seconds]
sam____ has joined #ocaml
ygrek has quit [Ping timeout: 248 seconds]
FreeBirdLjj has joined #ocaml
MercurialAlchemi has quit [Quit: Lost terminal]
FreeBirdLjj has quit [Ping timeout: 248 seconds]
MercurialAlchemi has joined #ocaml
ziyourenxiang has quit [Ping timeout: 268 seconds]
samrat_ has quit [Ping timeout: 240 seconds]
samrat_ has joined #ocaml
_whitelogger has joined #ocaml
sam____ has quit [Ping timeout: 260 seconds]
sam____ has joined #ocaml
sam____ has quit [Ping timeout: 260 seconds]
enterprisey has joined #ocaml
enterprisey has quit [Remote host closed the connection]
FreeBirdLjj has joined #ocaml
KeyJoo has joined #ocaml
enterprisey has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 248 seconds]
enterprisey has quit [Remote host closed the connection]
sam____ has joined #ocaml
sam____ has quit [Ping timeout: 255 seconds]
sam____ has joined #ocaml
MercurialAlchemi has quit [Ping timeout: 240 seconds]
FreeBirdLjj has joined #ocaml
peterpp has joined #ocaml
mrkgnao has joined #ocaml
FreeBirdLjj has quit [Remote host closed the connection]
mfp__ has joined #ocaml
peterpp has quit [Ping timeout: 240 seconds]
HoloIRCUser1 has joined #ocaml
HoloIRCUser1 is now known as HoloIRCUser18789
cranmax has joined #ocaml
FreeBirdLjj has joined #ocaml
leah2 has quit [Ping timeout: 258 seconds]
FreeBirdLjj has quit [Ping timeout: 255 seconds]
HoloIRCUser has joined #ocaml
MercurialAlchemi has joined #ocaml
HoloIRCUser18789 has quit [Ping timeout: 255 seconds]
HoloIRCUser1 has joined #ocaml
HoloIRCUser has quit [Read error: Connection reset by peer]
gallais_ has quit [Ping timeout: 240 seconds]
ziyourenxiang has joined #ocaml
leah2 has joined #ocaml
HoloIRCUser1 has quit [Remote host closed the connection]
sam____ has quit [Ping timeout: 260 seconds]
samrat_ has quit [Ping timeout: 260 seconds]
FreeBirdLjj has joined #ocaml
slash^ has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 240 seconds]
sam____ has joined #ocaml
FreeBirdLjj has joined #ocaml
_whitelogger has joined #ocaml
jlam_ has joined #ocaml
jlam has quit [Ping timeout: 248 seconds]
silver has joined #ocaml
mrkgnao has quit [Ping timeout: 255 seconds]
mrkgnao has joined #ocaml
dhil has joined #ocaml
FreeBirdLjj has joined #ocaml
FreeBirdLjj has quit [Ping timeout: 240 seconds]
sam____ has quit [Read error: Connection reset by peer]
Hannibal_Smith has joined #ocaml
mrkgnao has quit [Ping timeout: 258 seconds]
mrkgnao has joined #ocaml
sh0t has joined #ocaml
jlam has joined #ocaml
jlam_ has quit [Ping timeout: 260 seconds]
Hannibal_Smith has quit [Quit: Leaving]
michael_ has quit [Quit: Leaving]
fraggle_ has quit [Quit: -ENOBRAIN]
fraggle_ has joined #ocaml
FreeBirdLjj has joined #ocaml
jlam_ has joined #ocaml
jlam has quit [Ping timeout: 260 seconds]
cranmax has quit [Quit: Connection closed for inactivity]
jlam has joined #ocaml
jlam_ has quit [Ping timeout: 268 seconds]
jlam_ has joined #ocaml
jlam has quit [Ping timeout: 240 seconds]
gallais has joined #ocaml
jlam has joined #ocaml
samrat_ has joined #ocaml
jlam_ has quit [Ping timeout: 248 seconds]
jlam_ has joined #ocaml
<seliopou>
rgrinberg wher u at?
jlam has quit [Ping timeout: 240 seconds]
jlam has joined #ocaml
jlam_ has quit [Ping timeout: 240 seconds]
samrat_ has quit [Read error: Connection timed out]
jlam has quit [Ping timeout: 268 seconds]
malina has joined #ocaml
<rgrinberg>
Hey, Chiang Mai now.
<rgrinberg>
Real dope place btw. Perfect for chilling out and taking it easy
malina has quit [Remote host closed the connection]
malina has joined #ocaml
jmiven has quit [Quit: co'o]
jmiven has joined #ocaml
jmiven has quit [Quit: co'o]
jmiven has joined #ocaml
fraggle-boate_ has quit [Quit: Quitte]
fraggle-boate has joined #ocaml
peterpp has joined #ocaml
malina has quit [Remote host closed the connection]
enterprisey has joined #ocaml
jlam_ has joined #ocaml
KeyJoo has quit [Ping timeout: 248 seconds]
swalk has joined #ocaml
jlam_ has quit [Read error: Connection reset by peer]
jlam_ has joined #ocaml
malina has joined #ocaml
swalk has quit [Quit: swalk]
enterprisey has quit [Remote host closed the connection]
jao has joined #ocaml
<seliopou>
rgrinberg that's dope
average has quit [Ping timeout: 258 seconds]
average has joined #ocaml
jlam has joined #ocaml
peterpp_ has joined #ocaml
jlam_ has quit [Ping timeout: 255 seconds]
peterpp has quit [Ping timeout: 240 seconds]
rand__ has joined #ocaml
al-damiri has joined #ocaml
jlam_ has joined #ocaml
jlam has quit [Ping timeout: 240 seconds]
jlam_ has quit [Read error: Connection reset by peer]
<chet>
It does match l with, but then again value of l will be shadowed when it matches with a::l ?
malina has quit [Remote host closed the connection]
<chet>
should one use different variable name like a::tl instead? reusing same name l is ok as long as original l value is no longer needed?
malina has joined #ocaml
aantron_ has joined #ocaml
<octachron>
chet, rebinding the same name is indeed ok when one does not need the original value
rand__ has quit [Quit: leaving]
<chet>
ah, ok, I have used scheme before, there recursion was more explicit as I knew that recursion was getting smaller as (cdr l) was being used, here it looks like right hand side expression gets evaluated in environment enriched due to pattern match.
<chet>
Thanks octachron.
<octachron>
chet, indeed the pattern match binds variables and those bindings can be used in the rhs of the corresponding case
<octachron>
this is not so different than "let f (a,b) = a + b" where the pattern "(a,b)" bound the variable "a" and "b"
samrat_ has joined #ocaml
MercurialAlchemi has quit [Ping timeout: 248 seconds]
chet has quit [Quit: Page closed]
malina has quit [Remote host closed the connection]
aantron_ has quit [Remote host closed the connection]
aantron_ has joined #ocaml
swalk has joined #ocaml
dakk has joined #ocaml
malina has joined #ocaml
MercurialAlchemi has joined #ocaml
copy_ has joined #ocaml
ollehar has joined #ocaml
sh0t has quit [Quit: Leaving]
peterpp__ has joined #ocaml
kakadu has joined #ocaml
peterpp_ has quit [Ping timeout: 240 seconds]
kakadu_ has joined #ocaml
kakadu has quit [Ping timeout: 248 seconds]
ocaml681 has joined #ocaml
tane has joined #ocaml
swalk has quit [Quit: swalk]
dhil has quit [Ping timeout: 255 seconds]
MercurialAlchemi has quit [Ping timeout: 260 seconds]
sam____ has joined #ocaml
MercurialAlchemi has joined #ocaml
ocaml681 has quit [Quit: Page closed]
ziyourenxiang has quit [Ping timeout: 240 seconds]
sam____ has quit [Ping timeout: 255 seconds]
aantron_ has quit [Quit: leaving]
jao has quit [Ping timeout: 260 seconds]
malina has quit [Remote host closed the connection]
malina has joined #ocaml
malina has quit [Remote host closed the connection]
mrkgnao has quit [Ping timeout: 240 seconds]
samrat_ has quit [Ping timeout: 248 seconds]
swalk has joined #ocaml
riveter has joined #ocaml
mengu has joined #ocaml
jlam has quit [Read error: Connection reset by peer]
jlam has joined #ocaml
<rixed>
Is there a js_of_ocaml doc somewhere that explains the "foo##.bar" notation anywhere? I'm trying to understand how this relates to Js.gen_prop but fail.
<rixed>
I'd like to stop copy and pasting code when it comes to Js ... :/