<ousado>
I'd rather argue that especially in light of the delusional nature of man, negative proofs are extremely useful
paolooo_ has quit [Quit: Page closed]
<bernardofpc>
ousado: right, but this perception should come with a change of goals, once we're not deluded anymore ! And I for one think that Zeilberger's goal is very interesting
<bernardofpc>
having effective results (as opposed to existence results) should have come as a trivial corollary of all incompleteness theorems
<bernardofpc>
however, we still spend too much time with ineffective math, and also ineffective computing, where the constants before the O()'s are glossed over
<bernardofpc>
for example, if some algorithm has better O() performance for N > # particles in the universe, do we *really* care ?
<bernardofpc>
(I don't remember the status of PRIMES as to its constant, but back when it was published, it was outright useless)
<ousado>
it's seldom useless to engage ones mind
<ousado>
and science is in its infancy so far anyway.. what do we know which ideas, algorithms or whatever will be considered useful in a few 10, 100 or 1000 years
breakds has joined #ocaml
<bernardofpc>
perhaps we can learn from history those that stood the test of time
<bernardofpc>
and try to find a common pattern
<bernardofpc>
but I admit it is a hard thing
<bernardofpc>
but comming back to the original motivating question, if one wishes to compare two functions with a simple recursive algorithm, why shouldn't he be able to ?
<bernardofpc>
if that implies an infinite recursion, well, nothing prevents you from writing infinite loops in OCaml, right ?
<ousado>
are you still talking about comparing the ASTs?
<bernardofpc>
abstractly, yes
<bernardofpc>
but as all functions in OCaml have only one parameter, this is a simple recursion
<bernardofpc>
you compare the function and its argument for equality
<ousado>
if so, they're not available at runtime. and if they were, that would hardly buy anyone anything (speaking of inefficient computations and such)
<bernardofpc>
as the argument has been calculated and is in a known (for the ocmpiler) locationb in the closure text, this does not seem so impossible ?
<ousado>
how do you know which closures are being compared?
<ousado>
you only know about their type
<bernardofpc>
well, something in (+) 3 has to know a pointer for (+), or does it no ?
<ousado>
you get the general answer in the papaer wmeyer linked to
<ousado>
*paper
<bernardofpc>
ousado: note that I do not require that f = g terminates
<bernardofpc>
if this is absurdly recursive that the closure comparison by destructing the fun pointer + argument does not stop, it's the programmer's fault
<ousado>
and honestly, if you want to give some functoin an id, so you can compare it, it's much more efficient to do just that
<bernardofpc>
perhaps it is best to have another model for testing = between closures, but I believe that it should not be "the general case is T-Complete"
<bernardofpc>
the general case might be usefull, but since it is impossible, we might want to see wether more restricted semantics (à la Coq as was mentionned) can still provide usefull tools
emmanuelux has quit [Quit: emmanuelux]
<ousado>
"hey, here's a bug, the program freezes!" - "it's not frozen, it's just trying to figure out whether those two closures are equal"
<bernardofpc>
well
<bernardofpc>
if you find that you tree is in fact a cyclic graph, that's what you get :D
<bernardofpc>
that's probably harder to make with OCaml types, though
<bernardofpc>
an unrelated question: does OCaml use %rdi for some return information ?
<ousado>
no idea
<ousado>
alright, going to sleep, too
<bernardofpc>
gnight
<bernardofpc>
it would be nice to have a description somewhere of "how closures are implemented"
<bernardofpc>
from what I can see, this creates a 32 byte chunk on the stack, one with a magic number, another with the function adress, another magic number, then the argument
<bernardofpc>
(on (+) n)
gnuvince has quit [Ping timeout: 272 seconds]
yacks has quit [Ping timeout: 240 seconds]
yacks has joined #ocaml
madroach has quit [Ping timeout: 248 seconds]
madroach has joined #ocaml
weie has joined #ocaml
weie_ has quit [Ping timeout: 256 seconds]
weie has quit [Quit: Leaving...]
weie has joined #ocaml
gnuvince has joined #ocaml
nalaginrut has joined #ocaml
chrisdotcode_ has joined #ocaml
ulfdoz has joined #ocaml
ggole has joined #ocaml
caligula__ has joined #ocaml
caligula_ has quit [Ping timeout: 240 seconds]
bartholomew has quit [Quit: leaving]
breakds has quit [Quit: Konversation terminated!]
raichoo has joined #ocaml
ulfdoz has quit [Ping timeout: 260 seconds]
Watcher7 is now known as Watcher7|off
awm22 has quit [Quit: Leaving.]
ttamttam has joined #ocaml
ttamttam has left #ocaml []
Arsenik has joined #ocaml
talzeus has joined #ocaml
ontologiae has joined #ocaml
djcoin has joined #ocaml
cdidd has joined #ocaml
jsvgoncalves has joined #ocaml
ontologiae has quit [Ping timeout: 252 seconds]
awm22 has joined #ocaml
mika1 has joined #ocaml
cago has joined #ocaml
hkBst has joined #ocaml
ttamttam1 has joined #ocaml
hkBst_ has joined #ocaml
ttamttam1 has quit [Client Quit]
hkBst has quit [Ping timeout: 258 seconds]
hkBst_ has quit [Excess Flood]
hkBst_ has joined #ocaml
hkBst_ has quit [Read error: Connection reset by peer]
hkBst_ has joined #ocaml
jsvgoncalves has quit [Ping timeout: 252 seconds]
jbrown__ has joined #ocaml
Kakadu has joined #ocaml
eikke has joined #ocaml
jsvgoncalves has joined #ocaml
mcclurmc has quit [Ping timeout: 256 seconds]
Kakadu has quit [Ping timeout: 252 seconds]
<gasche>
bernardofpc: see the online book "Developping Applications with Objective Caml" for descriptions of OCaml value representations
<gasche>
(I respectfully doubt the idea that anyone should give a damn about the precise choice of heap layout for closures)
dwmw2_gone is now known as dwmw2
cdidd has quit [Read error: Connection reset by peer]
mathieui has quit [Ping timeout: 240 seconds]
mathieui has joined #ocaml
beckerb has joined #ocaml
jsvgoncalves has quit [Ping timeout: 252 seconds]
jsvgoncalves has joined #ocaml
<pippijn>
wmeyer: right, I hadn't considered the halting problem
<pippijn>
wmeyer: I think it would work for pure functions, though
mcclurmc has joined #ocaml
RagingDave has joined #ocaml
UncleVasya has joined #ocaml
groovy2shoes has quit [Quit: groovy2shoes]
jsvgoncalves has quit [Ping timeout: 264 seconds]
pancake has joined #ocaml
<pancake>
im trying to compiled findlib-1.3.3 with ocaml 4.0.0 but i get this error "Error: Unbound module Toploop
<pancake>
is there any fix for this?
gal_bolle has joined #ocaml
Tobu has quit [Ping timeout: 246 seconds]
awm22 has quit [Ping timeout: 245 seconds]
<def-lkb>
cls
<def-lkb>
oops, sorry
awm22 has joined #ocaml
pancake has left #ocaml []
nalaginrut has quit [Ping timeout: 245 seconds]
leoncamel has quit [Ping timeout: 272 seconds]
leoncamel has joined #ocaml
cdidd has joined #ocaml
_andre has joined #ocaml
<rixed>
quick fun poll people? Do you (a) understand or (b) do not understand the issue with injective types raised this WE on caml-list?
<rixed>
I for sure vote (b) :)
Anarchos has joined #ocaml
* csmrfx
ocaml noob votes b
<csmrfx>
(have not read the list)
paddymahoney has quit [Remote host closed the connection]
maurer has joined #ocaml
<maurer>
Ocaml has given me Fatal error: exception Stack_overflow
<maurer>
The code is quite complex, how do I track down where this was caused?
<pippijn>
maurer: Printexc.record_backtrace true;
<pippijn>
or something like that
<pippijn>
yep, that
<maurer>
OK, did that, where did my backtrace go?
nalaginrut has joined #ocaml
<maurer>
Doesn't seem to have gone to stdout or stderr
<maurer>
Segmentation fault
jsvgoncalves has joined #ocaml
<maurer>
:(
<maurer>
I'm not supposed to have segfaults in this language
<Anarchos>
i need some help on coq if anybody knows it
<maurer>
If anyone else was listening, re-running the program with bytecode avoids the segfault and prints the trace
<Anarchos>
maurer no idea sorry
<maurer>
So if you are trying to print the trace for a stack overflow, that may be useful
<maurer>
Anarchos: I found the answer to my question, I was just trying to put it in channel there in case someone is later grepping logs with a similar issue
<pippijn>
maurer: you need to build with debug
<pippijn>
ocamlopt -g
sepp2k has joined #ocaml
<Anarchos>
maurer you mean you used an in_channel instead of an out_channel ?
<maurer>
Anarchos: no...
<Cypi>
Anarchos : don't ask to ask. I won't be able to answer your question, but maybe someone else will.
<Anarchos>
Cypi i try to improve and finish the definition of PDemonstration and verification in this file : http://pastebin.com/qn642vP5
cdidd has quit [Ping timeout: 272 seconds]
eikke has quit [Ping timeout: 248 seconds]
eikke has joined #ocaml
breakds has joined #ocaml
cdidd has joined #ocaml
raichoo has quit [Quit: leaving]
alang_ has quit [Read error: Connection reset by peer]
alang_ has joined #ocaml
gnuvince has quit [Ping timeout: 252 seconds]
Neros has quit [Ping timeout: 245 seconds]
<gasche>
| a5 : AProp A5
<gasche>
yay readability
<gasche>
it looks like a mathematician picked the notations
<ggole>
It's perfectly reasonable notation for paper sizes.
<gasche>
those are names for axioms in the Coq development of Anarchos
<ggole>
Well, I hope he's proving something about paper size.
* ggole
looks
<gasche>
Anarchos: what are you trying to do exactly?
<gasche>
what is missing from you development, I think, are "specification tests"
<gasche>
when you introduce a notion in Coq, you should use it somehow, build a value of your type and/or prove something about it
<gasche>
to make sure that it makes sense
maurer has left #ocaml []
<gasche>
that's unit testing in the era of proof assistants
yacks has quit [Ping timeout: 272 seconds]
<gasche>
you define a "substitution" function, you should prove that, I don't know, forall foo, subst foo id = foo.
<gasche>
same thing with Pdemonstration, I expect to see an example of a demonstration of a property
<gasche>
(eg. (X*Y) -> (Y*X))
q66 has joined #ocaml
willy_ has joined #ocaml
<Anarchos>
gasche i am trying to define a verifier for propositional calculus
<Anarchos>
gasche for subst, i just copyied the work of gyesik lee, i will add the proofs from him afterwards.
ttamttam has joined #ocaml
wwilly has quit [Ping timeout: 256 seconds]
<gasche>
the point is that each time you define something
<gasche>
you have no clue whether the definition is actually what you think it is
<gasche>
so you should make an use of it, anything
<gasche>
an "example"
<gasche>
it will let you know that you're not horribly wrong in your idea of what it means
<gasche>
and also make you see potential problems with the use of the definition, before you do actual serious hard work with it, which can be a time-saver
<Anarchos>
gasche i know, i am just unable to state a strong specification of verification
<gasche>
it's not even about verification for now
ttamttam has quit [Remote host closed the connection]
<Anarchos>
gasche i want a function which takes a list of formulas and returns the list of axioms and substitutions used to state each formula of the list, or the first formula that is not a logical consequence of the antecedents in the list
Neros has joined #ocaml
<gasche>
hmm okay
<gasche>
what will the list of substitutions used for? cut elimination?
<gasche>
it looks more painful than just answering "yes it's valid" or "no it's not"
ttamttam has joined #ocaml
<gasche>
other than that
jsvgoncalves has quit [Ping timeout: 256 seconds]
<gasche>
I find your type for verification strange ('d' is not used in {d:.. | ...}), and you at least forgot the empty case in Pdemonstration
jsvgoncalves has joined #ocaml
<Anarchos>
gasche cut or instanciation of axioms
<Anarchos>
gasche my problem is really on the specification of "verification", i know i have to rewrite it clean, but i don't know how to do it.
<Anarchos>
gasche as the system is schedule to help students, it would be great to return also the first formula who is not an application of these logical soundness rules
smondet has joined #ocaml
<csmrfx>
which is not an application of these validity rules
<csmrfx>
;)
ttamttam has quit [Remote host closed the connection]
yacks has joined #ocaml
<Anarchos>
csmrfx what do you mean ?
<csmrfx>
just english correction
cago has left #ocaml []
mika1 has quit [Quit: Leaving.]
willy_ has quit [Quit: Leaving]
<gasche>
Anarchos: my advice would be to write the important part first
<gasche>
ie. -> option (Pdemonstration f l)
<gasche>
and then go for the fancy error reporting and stuff
<gasche>
as a second iteration
<gasche>
also you might want a monadic syntactic sugar for an error monad, but with this Hilbert-style proofs you probably won't have that much recursive calls
<gasche>
(I mean not much more than one per case)
<gasche>
hm
<gasche>
there are two separate concerns in your Pdemonstration type: (1) structure to ensure validity (the arguments of the constructors) and (2) information of what was proved (the first index of the type)
<gasche>
I think you could separate the two: have a type for valid demonstration, and a function that returns the formula that was proved (just 'head' it seems with your type)
<Anarchos>
gasche i just need help to write this strong specification of option (Pdemonstration f l), in order to extract ocaml code.
<gasche>
because so far you have no recursive use for the information on what was proved
<Anarchos>
gasche may you write it for me, or give enough clues ?
<Anarchos>
gasche or where can i find near coq files ?
Yoric has joined #ocaml
<gasche>
I don't know Anarchos
<gasche>
I'm not sure I understand what you mean
<gasche>
I think I would be able to develop the Pdemonstration type and write the checker function for it, but it looks a bit painful and would take me some time (I'm not proficient enough with Coq to do these things quickly)
<Anarchos>
i am looking just for the types, i am able to do the proofs alone if i have the type. The ultimate goal is to extract an ocaml code of the verifier.
gnuvince has joined #ocaml
jsvgoncalves has quit [Ping timeout: 240 seconds]
fantasticsid has joined #ocaml
Yoric has quit [Read error: Connection reset by peer]
<gasche>
Anarchos: well, just adding a case for the empty list in Pdemonstration and using option (Pdemonstration f l) looks like it would do the job at first approximation
<gasche>
that said, finding the substitution that corresponds to a term is probably going to be more painful than you imagine
<gasche>
(you have to implement a form of pattern-matching that takes two formula and returns an (option substitution) such that applying the substitution to the first formula returns the second one)
Yoric has joined #ocaml
<Anarchos>
gasche i already saw this difficulty , that is why i have the article of Gyesik lee about substitution ...
<Anarchos>
gasche i thought that the empty list could not be part of a demonstration....
gnuvince has quit [Ping timeout: 258 seconds]
Yoric has quit [Ping timeout: 252 seconds]
tane has joined #ocaml
tane has quit [Remote host closed the connection]
jsvgoncalves has joined #ocaml
awm22 has quit [Quit: Leaving.]
<gasche>
hm
<gasche>
Anarchos: good point about the empty list
<gasche>
I'm too used to other list invariants, and other proof structures (I would have assumed the empty list proves True, that is nothing at all, but you don't actually need that if it's one of your axioms).
bitbckt has quit [Quit: out]
bitbckt has joined #ocaml
<Anarchos>
gasche i wanted to use the syntax ... ->{d | demonstration d list_formula} to extract the ocaml code
beckerb has quit [Ping timeout: 245 seconds]
chrisdotcode_ has quit [Remote host closed the connection]
<gasche>
Anarchos: I don't understand what the link between extraction and the { d | ... } syntax is
<gasche>
but I'll have to go soon anyway
fantasticsid has quit [Remote host closed the connection]
Neros has quit [Ping timeout: 245 seconds]
<Anarchos>
gasche no pbm
darkf has quit [Quit: Leaving]
ttamttam has joined #ocaml
Arsenik has quit [Remote host closed the connection]
gal_bolle has quit [Remote host closed the connection]
hkBst_ has quit [Quit: Konversation terminated!]
UncleVasya has quit [Read error: Connection reset by peer]
jsvgoncalves has quit [Ping timeout: 255 seconds]
travisbrady has joined #ocaml
jsvgoncalves has joined #ocaml
Anarchos has quit [Quit: Vision[0.9.7-H-090423]: i've been blurred!]
jonludlam has joined #ocaml
Neros has joined #ocaml
UncleVasya has joined #ocaml
awm22 has joined #ocaml
Kakadu has joined #ocaml
breakds has quit [Quit: Konversation terminated!]
travisbrady has quit [Quit: travisbrady]
pango_ has joined #ocaml
eikke has quit [Ping timeout: 260 seconds]
pango has quit [Ping timeout: 264 seconds]
ggole has quit []
pango_ is now known as pango
nalaginrut has quit [Ping timeout: 272 seconds]
watermind has joined #ocaml
travisbrady has joined #ocaml
Neros has quit [Ping timeout: 258 seconds]
zpe has quit [Remote host closed the connection]
Neros has joined #ocaml
troydm has quit [Read error: Operation timed out]
troydm has joined #ocaml
Anarchos has joined #ocaml
Nahra has quit [Remote host closed the connection]
Nahra has joined #ocaml
emmanuelux has joined #ocaml
zpe has joined #ocaml
Neros_ has joined #ocaml
zpe has quit [Ping timeout: 276 seconds]
Neros has quit [Ping timeout: 258 seconds]
thizanne has quit [Ping timeout: 258 seconds]
thizanne has joined #ocaml
adahlberg has joined #ocaml
adahlberg has left #ocaml []
mcclurmc has quit [Ping timeout: 264 seconds]
groovy2shoes has joined #ocaml
tane has joined #ocaml
eikke has joined #ocaml
stevej has joined #ocaml
eikke has quit [Read error: Operation timed out]
eikke has joined #ocaml
eikke has quit [Ping timeout: 264 seconds]
eikke has joined #ocaml
zpe has joined #ocaml
jsvgoncalves has quit [Ping timeout: 260 seconds]
zpe has quit [Ping timeout: 248 seconds]
eikke has quit [Ping timeout: 246 seconds]
eikke has joined #ocaml
mcclurmc has joined #ocaml
eikke has quit [Ping timeout: 256 seconds]
eikke has joined #ocaml
gnuvince has joined #ocaml
sepp2k has quit [Ping timeout: 252 seconds]
ttamttam has left #ocaml []
Drup has joined #ocaml
jsvgoncalves has joined #ocaml
watermind has quit [Quit: Konversation terminated!]
malo_ has joined #ocaml
eikke has quit [Ping timeout: 240 seconds]
zpe has joined #ocaml
zpe has quit [Ping timeout: 256 seconds]
eni has joined #ocaml
malo_ is now known as malo
jsvgoncalves has quit [Ping timeout: 264 seconds]
Watcher7|off is now known as Watcher7
travisbrady has quit [Quit: travisbrady]
travisbrady has joined #ocaml
tane has quit [Quit: Verlassend]
zpe has joined #ocaml
_andre has quit [Quit: leaving]
malo has quit [Quit: Leaving]
eikke has joined #ocaml
zpe has quit [Ping timeout: 245 seconds]
beginner42 has joined #ocaml
beginner42585 has joined #ocaml
jsvgoncalves has joined #ocaml
Kakadu has quit []
<beginner42585>
i need to update an opam package and adding some lines to the _oasis file. i am new to oasis how do i proceed?
<thelema>
run 'oais setup'
<thelema>
*oasis
<thelema>
if you don't have oasis installed, opam can install it
<beginner42585>
thelema: thanks, always very helpful :)
RagingDave has quit [Quit: Ex-Chat]
<thelema>
beginner42585: n/p
Nahra has quit [Ping timeout: 252 seconds]
Nahra has joined #ocaml
djcoin has quit [Quit: WeeChat 0.3.9.2]
thizanne has quit [Ping timeout: 258 seconds]
thizanne has joined #ocaml
UncleVasya has quit [Ping timeout: 256 seconds]
rgrinberg has joined #ocaml
rgrinberg has quit [Quit: leaving]
beginner42585 has quit [Quit: irc2go]
q66 has quit [Remote host closed the connection]
q66 has joined #ocaml
Anarchos has quit [Ping timeout: 258 seconds]
beginner42 has quit [Remote host closed the connection]
smerz_ has joined #ocaml
q66 has quit [Remote host closed the connection]
Anarchos has joined #ocaml
dwmw2 is now known as dwmw2_gone
smondet has quit [Ping timeout: 252 seconds]
jonludlam has quit [Remote host closed the connection]
jbrown__ has quit [Ping timeout: 255 seconds]
ulfdoz has joined #ocaml
mcclurmc has quit [Ping timeout: 245 seconds]
eni has quit [Quit: Leaving]
zpe has joined #ocaml
rgrinberg has joined #ocaml
zpe has quit [Ping timeout: 252 seconds]
rgrinberg has quit [Quit: WeeChat 0.4.0]
jsvgoncalves has quit [Ping timeout: 248 seconds]
travisbrady has quit [Quit: travisbrady]
Anarchos has quit [Quit: Vision[0.9.7-H-090423]: i've been blurred!]