From: Guillaume Brunerie <guillaume.brunerie@en...>  20100206 16:46:30
Attachments:
Message as HTML

2010/2/5 Hongwei Xi <hwxi@...> > > I can easily follow your proof. > > In the attached file, I gave an incomplete implementation. Usually, > I go with a topdown approach, laying out a blueprint first by > introducing absprops abundantly. > Thank you :) We have indeed not the same approach. For example, I would directly define MOD and DIV in terms of MUL instead of using absprops and extern proof functions. > BTW, You can change something like > > [n > 0] (...) > > into > > (() > [n > 0] void, ...) > > so as to circumvent the problem you reported earlier. Thank you, it works. > >>Yes, I think it would be a good idea to have a flag controlling whether > or > >>not unimplemented proof functions are allowed. > > Okay, I have put this on the todolist. > > >>And what is "praxi" ? If this if for introducing axioms, why not use > praxi > >>instead of "extern prfun" ? > > The original plan is to use praxi to introduce axioms requiring no proofs. > With prfun, a proof can be postponed but still required. > > >>Another thing which would be useful, I think, would be to have a symbol > >>(like "_") which would be a proof of everything. > >>We could then write things like that : > >> > >>fun f (a : int) : ( (* complicated prop with several components *)  int) > = > >>let > >> prval pf1 = (* proof of the first component *) > >>in > >> ((pf1, _, _, _)  a + 1) > >>end > >>in order to be able to check easily some parts of the proof (but > obviously > >>this has to be refused when compiling to C and/or display a warning > during > >>typechecking saying that some components have not been proven yet) > > For this, you can have something like > > extern prfun oralce {P:prop} (): P > > and then replace _ with oracle(). I tried to do something like extern prval oracle {P : prop} : P but it didn’t worked. With a function it works :) > >>Other question : > >>As a prop must always be pure, is there a difference between > and <> > in > >>props ? > > There should be no difference. Sometimes, you also see <prf>. Should something like prfn f (a : () > void) : void = a () work ? It doesn’t, the compiler complains that 'a' can have effects and that this is disallowed in a proof function. But shouldn’t 'a' be considered as a prop, ie that 'a' implicitely would be pure and total ? Thank you for all your answers :) Cheers, Guillaume Brunerie 
From: Guillaume Brunerie <guillaume.brunerie@en...>  20100203 15:51:49
Attachments:
Message as HTML

Hi, The following code doesn’t typechecks and gives an internal error : propdef Test (p : int) = [p >= 2] ({x : nat} MUL (0, x, 0) <> void) extern fun test () : [p : pos] (Test p  int p) val [p : int] (_ : Test p  _ : int p) = test () $ atsccsvn tc bug.dats /home/fractal/Programmation/ATS/svn/bin/atsopt typecheck dynamic bug.dats /home/fractal/Programmation/ATS/bug.dats: 134(line=3, offs=16)  144(line=3, offs=26): INTERNAL ERROR (ats_constraint): s2var_index_find: the static constant [x$29$30$31] is not associated with any index. exit(ATS): uncaught exception: ATS_2d0_2e2_2e0_2src_2ats_error_2esats__FatalErrorException(1002) exit(ATS): [typecheck_file(bug.dats)] failed. When I remove the assertion [p >= 2] in the prop "Test", the code is successfully typechecked. About asserting props, it is said in the FAQ (end of the first question) that asserting types are not very useful in practice, but I think that at least asserting props are. For example the prop PRIME is given in the examples as : propdef PRIME (p:int) = // if p >= 2 {x,y:nat  x <= y} MUL (x, y, p) <> [x==1] void but asserting props would make the compiler check that every prime number is >= 2, by writing : propdef PRIME (p:int) = [p >= 2] {x,y:nat  x <= y} MUL (x, y, p) <> [x==1] void I think it is worth to have a PRIME prop which is really satisfied only by prime numbers. Guillaume Brunerie 
From: Hongwei Xi <hwxi@cs...>  20100203 22:43:50

On Wed, 3 Feb 2010, Guillaume Brunerie wrote: >>Hi, >> >>The following code doesn't typechecks and gives an internal error : >> >> >>propdef Test (p : int) = [p >= 2] ({x : nat} MUL (0, x, 0) <> void) >>extern fun test () : [p : pos] (Test p  int p) >>val [p : int] (_ : Test p  _ : int p) = test () >> >>$ atsccsvn tc bug.dats >>/home/fractal/Programmation/ATS/svn/bin/atsopt typecheck dynamic >>bug.dats >>/home/fractal/Programmation/ATS/bug.dats: 134(line=3, offs=16)  >>144(line=3, offs=26): INTERNAL ERROR (ats_constraint): s2var_index_find: the >>static constant [x$29$30$31] is not associated with any index. >>exit(ATS): uncaught exception: >>ATS_2d0_2e2_2e0_2src_2ats_error_2esats__FatalErrorException(1002) >>exit(ATS): [typecheck_file(bug.dats)] failed. Here is the reason: say T is a type involving several quantifiers: T = {a:int} [b:int] ... Trying to prove (automatically) that T is a subtype of T is nontrivial. In ATS, there are a set of (very simple) rules for eliminating quantifiers when proving a subtyping relation. In this case, these rules are not adequate to prove that Test(p) is a subtype of Test(p). I have just checked the rules (given in the DML journal paper). I could readily modify them so that this case can be handled. Obviously, the problem is where I should stop if I do this. If you do: val [p : int] (_  _ : int p) = test () then you should have no problem. >>When I remove the assertion [p >= 2] in the prop "Test", the code is >>successfully typechecked. >>About asserting props, it is said in the FAQ (end of the first question) >>that asserting types are not very useful in practice, but I think that at >>least asserting props are. For example the prop PRIME is given in the >>examples as : >> >>propdef PRIME (p:int) = // if p >= 2 >> {x,y:nat  x <= y} MUL (x, y, p) <> [x==1] void >> >>but asserting props would make the compiler check that every prime number is >>>= 2, by writing : >> >>propdef PRIME (p:int) = [p >= 2] >> {x,y:nat  x <= y} MUL (x, y, p) <> [x==1] void >> >>I think it is worth to have a PRIME prop which is really satisfied only by >>prime numbers. True. However, I find it more effective if you do something like: absprop PRIME (p:int) extern prfun prime_prop1 {p:nat} (pf: PRIME (p)): [p >= 2] void extern prfun prime_prop2 {p:nat} {m,n:nat  m<=n} (pf1: PRIME p, pf2: MUL (m,n,p)): [m==1] void ... Basically, if you need a property about primes, just write a prfun in ATS to encode that property. If you don't trust the property, then try to prove it using simpler ones. For instance, I was thinking about constructing a proof in this way for FermatWiles theorem in the case where n = 4; but I have never had time ... Hongwei Computer Science Department Boston University 111 Cummington Street Boston, MA 02215 Email: hwxi@... Url: http://www.cs.bu.edu/~hwxi Tel: +1 617 358 2511 (office) Fax: +1 617 353 6457 (department) 
From: Guillaume Brunerie <guillaume.brunerie@en...>  20100204 04:06:01
Attachments:
Message as HTML

2010/2/3 Hongwei Xi <hwxi@...> > > If you do: > > val [p : int] (_  _ : int p) = test () > > then you should have no problem. Actually I have this problem is a more complicated example. I have to write a function returning (as a proof component) something whose (complicated) type has several quantifiers. I first calculate this term in a "let prfn pf […] in […]" , then I return it. The problem is probably that I declare the type of 'pf' in the "let prfn pf […] in", and as the return type of the function, so the type checker has to prove that one is a subtype of the other : problem. But I don’t know which type annotation I could suppress, the two seems mandatory… >>When I remove the assertion [p >= 2] in the prop "Test", the code is > >>successfully typechecked. > >>About asserting props, it is said in the FAQ (end of the first question) > >>that asserting types are not very useful in practice, but I think that at > >>least asserting props are. For example the prop PRIME is given in the > >>examples as : > >> > >>propdef PRIME (p:int) = // if p >= 2 > >> {x,y:nat  x <= y} MUL (x, y, p) <> [x==1] void > >> > >>but asserting props would make the compiler check that every prime number > is > >>>= 2, by writing : > >> > >>propdef PRIME (p:int) = [p >= 2] > >> {x,y:nat  x <= y} MUL (x, y, p) <> [x==1] void > >> > >>I think it is worth to have a PRIME prop which is really satisfied only > by > >>prime numbers. > > True. However, I find it more effective if you do something like: > > absprop PRIME (p:int) > > extern > prfun prime_prop1 {p:nat} (pf: PRIME (p)): [p >= 2] void > > extern > prfun prime_prop2 > {p:nat} {m,n:nat  m<=n} > (pf1: PRIME p, pf2: MUL (m,n,p)): [m==1] void > > ... > > Basically, if you need a property about primes, just write a prfun > in ATS to encode that property. If you don't trust the property, then > try to prove it using simpler ones. For instance, I was thinking about > constructing a proof in this way for FermatWiles theorem in the case > where n = 4; but I have never had time ... Those "extern prfun" seems to me unnatural. In my opinion, the keyword "extern" is there to tell the typechecker "I’ll implement this function elsewhere so trust me, this function will exist." So the "extern prfun" seems to me some "hack", it is accepted by the type checker because the type checker only needs the types, but also by the ATS to C compiler, because proof functions are erased after type checking. This allow writing programs which seems to be proved (are well typed), but which actually depend on unimplemented prfuns, ie potentially wrong assumptions. I noticed that also in listquicksort.dats, there are some unimplemented prfuns, so is this really a totally proved quicksort implementation ? I solved the first two Project Euler’s problems (http://projecteuler.net) in ATS (I don’t have a website yet but I’m working on it, for the moment you can find the code for the first problem at " http://www.eleves.ens.fr/home/brunerie/p1_dats.html";, and the like for the problem 2). I’m working on the problem 3 but it is much more difficult than the first two. I tried to write the code in three parts : 1) write a prop encoding the problem 2) write the type of the function pn which must solve the problem, and implement the function "main" 3) implement the function pn I would like that, after reading only the first two parts, the reader could be certain that if the code compiles, then the program terminates and gives the correct result, whatever is written in the third part; the idea being that the proved implementation can be very complicated but if ATS/Anairiats accepts it and if the type is correct, then the program should be correct. The idea to declare the PRIME prop abstract and to write prfun for the needed properties looks interesting, but that means that I should write extern prfuns only in the first part (the "human verified part") but not in the third (the "machine verified part") because there this would be cheating. In this context, I’m not sure this would be a satisfactory solution. "extern prfun" is useful sometimes, I use it for example in the problem 3 for debugging, to check that some parts of the program are correct without having to prove anything at once, but I consider that a problem is solved only if there is no more "extern" in the code. Perhaps I have not the good point of view, or at least not the same as yours. Cheers, Guillaume Brunerie 
From: Hongwei Xi <hwxi@cs...>  20100204 16:18:11

>>Actually I have this problem is a more complicated example. >>I have to write a function returning (as a proof component) something whose >>(complicated) type has several quantifiers. I first calculate this term in a >>"let prfn pf [...] in [...]" , then I return it. >>The problem is probably that I declare the type of 'pf' in the "let prfn pf >>[...] in", and as the return type of the function, so the type checker has to >>prove that one is a subtype of the other : problem. But I don't know which >>type annotation I could suppress, the two seems mandatory... There are many simple ways to get around this issue. If you put your code somewhere, I will be happy to take a look. >>Those "extern prfun" seems to me unnatural. >>In my opinion, the keyword "extern" is there to tell the typechecker "I'll >>implement this function elsewhere so trust me, this function will exist." >>So the "extern prfun" seems to me some "hack", it is accepted by the type >>checker because the type checker only needs the types, but also by the ATS >>to C compiler, because proof functions are erased after type checking. This >>allow writing programs which seems to be proved (are well typed), but which >>actually depend on unimplemented prfuns, ie potentially wrong assumptions. >>I noticed that also in listquicksort.dats, there are some unimplemented >>prfuns, so is this really a totally proved quicksort implementation ? The problem with providing all the proofs is the heavy cost it incurs; the programmer spends a lot of time proving things that are "obviously" true. But I really don't know how to address this issue properly. >>I solved the first two Project Euler's problems (http://projecteuler.net) in >>ATS (I don't have a website yet but I'm working on it, for the moment you >>can find the code for the first problem at " >>http://www.eleves.ens.fr/home/brunerie/p1_dats.html";, and the like for the >>problem 2). I'm working on the problem 3 but it is much more difficult than >>the first two. I took a look. Pretty nice! >>I tried to write the code in three parts : >>1) write a prop encoding the problem >>2) write the type of the function pn which must solve the problem, and >>implement the function "main" >>3) implement the function pn >> >>I would like that, after reading only the first two parts, the reader could >>be certain that if the code compiles, then the program terminates and gives >>the correct result, whatever is written in the third part; the idea being >>that the proved implementation can be very complicated but if ATS/Anairiats >>accepts it and if the type is correct, then the program should be correct. That is what I thought as well when I started the ATS project. But this approach seems too costly when applied to large and realistic problems. >>The idea to declare the PRIME prop abstract and to write prfun for the >>needed properties looks interesting, but that means that I should write >>extern prfuns only in the first part (the "human verified part") but not in >>the third (the "machine verified part") because there this would be >>cheating. In this context, I'm not sure this would be a satisfactory >>solution. >> >>"extern prfun" is useful sometimes, I use it for example in the problem 3 >>for debugging, to check that some parts of the program are correct without >>having to prove anything at once, but I consider that a problem is solved >>only if there is no more "extern" in the code. We could require that all the extern proof functions in a program be implemented before the program can run. I may add a flag to control this. >>Perhaps I have not the good point of view, or at least not the same as >>yours. We all have different views :) My view was similar to yours, but it has since changed. Cheers, Hongwei Computer Science Department Boston University 111 Cummington Street Boston, MA 02215 Email: hwxi@... Url: http://www.cs.bu.edu/~hwxi Tel: +1 617 358 2511 (office) Fax: +1 617 353 6457 (department) 
From: Guillaume Brunerie <guillaume.brunerie@en...>  20100204 18:03:51
Attachments:
Message as HTML

2010/2/4 Hongwei Xi <hwxi@...> > > There are many simple ways to get around this issue. If you put > your code somewhere, I will be happy to take a look. This is in the problem 3 of Project Euler ( http://www.eleves.ens.fr/home/brunerie/p3_dats.html), I have an (asserting) prop Prime, and I have to prove that k is the smallest prime factor of n (in the function iter, when r = 0). I first prove that k is prime (well, actually there is an extern prfun, but it has to be proved latter), then I return this proof along with the other proof terms (k divides n and n has no prime factor smaller than k). The type of ` k_is_prime ' is first declared when it is "proved", and then the compiler must check that the proof that k is the smallest prime factor of n is correct. > The problem with providing all the proofs is the heavy cost it incurs; > the programmer spends a lot of time proving things that are "obviously" > true. But I really don't know how to address this issue properly. Yes, I undersand. In the problem 3 I’m working on, I have to prove things like "if n = 2 * k then n / k = 2" which seems obvious, but even there I must not forget the condition k <> 0. And this is easy to forget such condition with an "extern prfun". > I took a look. Pretty nice! Thank you :) > >>I tried to write the code in three parts : > >>1) write a prop encoding the problem > >>2) write the type of the function pn which must solve the problem, and > >>implement the function "main" > >>3) implement the function pn > >> > >>I would like that, after reading only the first two parts, the reader > could > >>be certain that if the code compiles, then the program terminates and > gives > >>the correct result, whatever is written in the third part; the idea being > >>that the proved implementation can be very complicated but if > ATS/Anairiats > >>accepts it and if the type is correct, then the program should be > correct. > > That is what I thought as well when I started the ATS project. But this > approach seems too costly when applied to large and realistic problems. > >>The idea to declare the PRIME prop abstract and to write prfun for the > >>needed properties looks interesting, but that means that I should write > >>extern prfuns only in the first part (the "human verified part") but not > in > >>the third (the "machine verified part") because there this would be > >>cheating. In this context, I'm not sure this would be a satisfactory > >>solution. > >> > >>"extern prfun" is useful sometimes, I use it for example in the problem 3 > >>for debugging, to check that some parts of the program are correct > without > >>having to prove anything at once, but I consider that a problem is solved > >>only if there is no more "extern" in the code. > > We could require that all the extern proof functions in a program be > implemented before the program can run. I may add a flag to control this. Yes, I think it would be a good idea to have a flag controlling whether or not unimplemented proof functions are allowed. And what is "praxi" ? If this if for introducing axioms, why not use praxi instead of "extern prfun" ? Another thing which would be useful, I think, would be to have a symbol (like "_") which would be a proof of everything. We could then write things like that : fun f (a : int) : ( (* complicated prop with several components *)  int) = let prval pf1 = (* proof of the first component *) in ((pf1, _, _, _)  a + 1) end in order to be able to check easily some parts of the proof (but obviously this has to be refused when compiling to C and/or display a warning during typechecking saying that some components have not been proven yet) Other question : As a prop must always be pure, is there a difference between > and <> in props ? Guillaume Brunerie 
From: Hongwei Xi <hwxi@cs...>  20100205 14:00:20
Attachments:
problem3.dats

On Thu, 4 Feb 2010, Guillaume Brunerie wrote: >>This is in the problem 3 of Project Euler ( >>http://www.eleves.ens.fr/home/brunerie/p3_dats.html), I have an (asserting) >>prop Prime, and I have to prove that k is the smallest prime factor of n (in >>the function iter, when r = 0). I first prove that k is prime (well, >>actually there is an extern prfun, but it has to be proved latter), then I >>return this proof along with the other proof terms (k divides n and n has no >>prime factor smaller than k). The type of ` k_is_prime ' is first declared >>when it is "proved", and then the compiler must check that the proof that k >>is the smallest prime factor of n is correct. I can easily follow your proof. In the attached file, I gave an incomplete implementation. Usually, I go with a topdown approach, laying out a blueprint first by introducing absprops abundantly. BTW, You can change something like [n > 0] (...) into (() > [n > 0] void, ...) so as to circumvent the problem you reported earlier. >>Yes, I think it would be a good idea to have a flag controlling whether or >>not unimplemented proof functions are allowed. Okay, I have put this on the todolist. >>And what is "praxi" ? If this if for introducing axioms, why not use praxi >>instead of "extern prfun" ? The original plan is to use praxi to introduce axioms requiring no proofs. With prfun, a proof can be postponed but still required. >>Another thing which would be useful, I think, would be to have a symbol >>(like "_") which would be a proof of everything. >>We could then write things like that : >> >>fun f (a : int) : ( (* complicated prop with several components *)  int) = >>let >> prval pf1 = (* proof of the first component *) >>in >> ((pf1, _, _, _)  a + 1) >>end >>in order to be able to check easily some parts of the proof (but obviously >>this has to be refused when compiling to C and/or display a warning during >>typechecking saying that some components have not been proven yet) For this, you can have something like extern prfun oralce {P:prop} (): P and then replace _ with oracle(). >>Other question : >>As a prop must always be pure, is there a difference between > and <> in >>props ? There should be no difference. Sometimes, you also see <prf>. Cheers, Hongwei Computer Science Department Boston University 111 Cummington Street Boston, MA 02215 Email: hwxi@... Url: http://www.cs.bu.edu/~hwxi Tel: +1 617 358 2511 (office) Fax: +1 617 353 6457 (department) 
From: Guillaume Brunerie <guillaume.brunerie@en...>  20100206 16:46:30
Attachments:
Message as HTML

2010/2/5 Hongwei Xi <hwxi@...> > > I can easily follow your proof. > > In the attached file, I gave an incomplete implementation. Usually, > I go with a topdown approach, laying out a blueprint first by > introducing absprops abundantly. > Thank you :) We have indeed not the same approach. For example, I would directly define MOD and DIV in terms of MUL instead of using absprops and extern proof functions. > BTW, You can change something like > > [n > 0] (...) > > into > > (() > [n > 0] void, ...) > > so as to circumvent the problem you reported earlier. Thank you, it works. > >>Yes, I think it would be a good idea to have a flag controlling whether > or > >>not unimplemented proof functions are allowed. > > Okay, I have put this on the todolist. > > >>And what is "praxi" ? If this if for introducing axioms, why not use > praxi > >>instead of "extern prfun" ? > > The original plan is to use praxi to introduce axioms requiring no proofs. > With prfun, a proof can be postponed but still required. > > >>Another thing which would be useful, I think, would be to have a symbol > >>(like "_") which would be a proof of everything. > >>We could then write things like that : > >> > >>fun f (a : int) : ( (* complicated prop with several components *)  int) > = > >>let > >> prval pf1 = (* proof of the first component *) > >>in > >> ((pf1, _, _, _)  a + 1) > >>end > >>in order to be able to check easily some parts of the proof (but > obviously > >>this has to be refused when compiling to C and/or display a warning > during > >>typechecking saying that some components have not been proven yet) > > For this, you can have something like > > extern prfun oralce {P:prop} (): P > > and then replace _ with oracle(). I tried to do something like extern prval oracle {P : prop} : P but it didn’t worked. With a function it works :) > >>Other question : > >>As a prop must always be pure, is there a difference between > and <> > in > >>props ? > > There should be no difference. Sometimes, you also see <prf>. Should something like prfn f (a : () > void) : void = a () work ? It doesn’t, the compiler complains that 'a' can have effects and that this is disallowed in a proof function. But shouldn’t 'a' be considered as a prop, ie that 'a' implicitely would be pure and total ? Thank you for all your answers :) Cheers, Guillaume Brunerie 
From: Hongwei Xi <hwxi@cs...>  20100207 02:05:19

On Sat, 6 Feb 2010, Guillaume Brunerie wrote: >>Should something like >> >>prfn f (a : () > void) : void = a () >> >>work ? >>It doesn't, the compiler complains that 'a' can have effects and that this >>is disallowed in a proof function. >>But shouldn't 'a' be considered as a prop, ie that 'a' implicitely would be >>pure and total ? The argument of a proof function needs to be a value; but it does not have to be a proof value. For instance, an integer value can be passed to a proof function. If you write: prfn f (a : () <prf> void) : void = a () Then the compiler knows that 'a' is a proof function and should not complain. Cheers, Hongwei Computer Science Department Boston University 111 Cummington Street Boston, MA 02215 Email: hwxi@... Url: http://www.cs.bu.edu/~hwxi Tel: +1 617 358 2511 (office) Fax: +1 617 353 6457 (department) 