Skip to first unread message
Yannick Duchêne
Feb 9, 2015, 7:41:06 PM2/9/15
to ats-lan...@googlegroups.com
Basic questions, but I really have to ask… I'm not sure to really understand what `prfun`/`prfn` and `prval` do.
What's exactly the result of a proof function? Most seems to return void, but some returns a result. Is this a static value? Are proof functions simply static functions?
What happens when the result of a proof function is bound to a `prval` or especially matched with `()`? Does it makes ATS (the checker, not the language) store some confirmed hypotheses internally? If yes, then is there a way to “dump” these hypotheses?
How does a proof “returned” by a proof function differs from a proof returned along with a result from a dynamic function?
Brandon Barker
Feb 9, 2015, 7:53:47 PM2/9/15
to ats-lang-users
On Mon, Feb 9, 2015 at 7:41 PM, 'Yannick Duchêne' via ats-lang-users <ats-lan...@googlegroups.com> wrote:
Basic questions, but I really have to ask… I'm not sure to really understand what `prfun`/`prfn` and `prval` do.What's exactly the result of a proof function? Most seems to return void, but some returns a result. Is this a static value? Are proof functions simply static functions?
Yes, they are both static only.
What happens when the result of a proof function is bound to a `prval` or especially matched with `()`? Does it makes ATS (the checker, not the language) store some confirmed hypotheses internally? If yes, then is there a way to “dump” these hypotheses?How does a proof “returned” by a proof function differs from a proof returned along with a result from a dynamic function?
IIRC, they are the same, but a dynamic function can return both dynamics and statics. I think prfuns may be used to implement lemmas for the proof returned from a dynamic function.
--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/831de703-bfb8-4a02-8da3-f73de11fe62c%40googlegroups.com.
gmhwxi
Feb 9, 2015, 7:58:44 PM2/9/15
to ats-lan...@googlegroups.com
A proof-value is in the dynamics of ATS.
prfun/prfn/prval are used to form bindings between names and proof values.
The main difference between a proof-value and a program-value (that is, non-proof-value)
is that the former can never have any influence the construction of the latter. So therefore,
proof values are all erased after type-checking.
prfun/prfn/prval are used to form bindings between names and proof values.
The main difference between a proof-value and a program-value (that is, non-proof-value)
is that the former can never have any influence the construction of the latter. So therefore,
proof values are all erased after type-checking.
>>What's exactly the result of a proof function? Most seems to return
void, but some returns a result. Is this a static value? Are proof
functions simply static functions?
The result of a proof function is a proof value. Proof functions are not static functions; they are dynamic.
>>What happens when the result of a proof function is bound to a `prval` or especially matched with `()`? Does it makes ATS (the checker, not the language) store some confirmed hypotheses internally? If yes, then is there a way to “dump” these hypotheses?
Say we have
prfun lemma_fib{n:nat}{r:int}(FIB(n, r)): [n <= r+1] void // fib(n)+1 >= n
Suppose that pf is a proof-value of the prop FIB(N, R) for some N and R
The the following declaration adds (N <= R+1) to the internal store of currently available assumptions:
prval () = lemma_fib(pf)
prfun lemma_fib{n:nat}{r:int}(FIB(n, r)): [n <= r+1] void // fib(n)+1 >= n
Suppose that pf is a proof-value of the prop FIB(N, R) for some N and R
The the following declaration adds (N <= R+1) to the internal store of currently available assumptions:
prval () = lemma_fib(pf)
>>If yes, then is there a way to “dump” these hypotheses?
Yes. But not in a form that is readable.
>>How does a proof “returned” by a proof function differs from a proof returned along with a result from a dynamic function?
There is no difference.
Yannick Duchêne
Feb 9, 2015, 8:15:19 PM2/9/15
to ats-lan...@googlegroups.com
Le mardi 10 février 2015 01:58:44 UTC+1, gmhwxi a écrit :
A proof-value is in the dynamics of ATS.
That was good to ask… I was so wrong…
Thanks for the notice!
>>If yes, then is there a way to “dump” these hypotheses?
Yes. But not in a form that is readable.
I don't mind, this is still better than nothing :-P . Is this using a special keyword like `$showtype`?
Brandon Barker
Feb 9, 2015, 8:17:15 PM2/9/15
to ats-lang-users
On Mon, Feb 9, 2015 at 8:15 PM, 'Yannick Duchêne' via ats-lang-users <ats-lan...@googlegroups.com> wrote:
Le mardi 10 février 2015 01:58:44 UTC+1, gmhwxi a écrit :A proof-value is in the dynamics of ATS.That was good to ask… I was so wrong…
Wow, me too. So maybe I'm confused about what "dynamics" means. I was thinking it was anything that could have a representation in the generated code (e.g. C code).
Thanks for the notice!>>If yes, then is there a way to “dump” these hypotheses?
Yes. But not in a form that is readable.I don't mind, this is still better than nothing :-P . Is this using a special keyword like `$showtype`?
--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/243d6361-c934-4658-a338-75d550f4eab9%40googlegroups.com.
gmhwxi
Feb 9, 2015, 8:29:16 PM2/9/15
to ats-lan...@googlegroups.com
In the following file:
https://github.com/githwxi/ATS-Postiats/blob/master/prelude/basics_dyn.sats
you will find the following functions:
prfun prop_verify{b:bool | b} ():<prf> void
prfun prop_verify_and_add{b:bool | b} ():<prf> [b] void
Say at one point, you want to know if (i==j) holds. You
do this by adding the following line:
prval () = prop_verify{i==j}()
https://github.com/githwxi/ATS-Postiats/blob/master/prelude/basics_dyn.sats
you will find the following functions:
prfun prop_verify{b:bool | b} ():<prf> void
prfun prop_verify_and_add{b:bool | b} ():<prf> [b] void
Say at one point, you want to know if (i==j) holds. You
do this by adding the following line:
prval () = prop_verify{i==j}()
Yes. But not in a form that is readable.
>> I don't mind, this is still better than nothing :-P
It is really really not readable :)
What you see is millions of bytes of internal syntax trees. Try
the following command line on your own:
patsopt -tc --constraint-export -d ${PATSHOME}/doc/EXAMPLE/ATSLF/sqrt2_irrat.dats
What you see is millions of bytes of internal syntax trees. Try
the following command line on your own:
patsopt -tc --constraint-export -d ${PATSHOME}/doc/EXAMPLE/ATSLF/sqrt2_irrat.dats
gmhwxi
Feb 9, 2015, 8:35:43 PM2/9/15
to ats-lan...@googlegroups.com
I pasted an example of internal constraints:
http://pastebin.com/GDwNQPQi
It is incomplete. Just to give people an idea ...
Brandon Barker
Feb 9, 2015, 9:03:21 PM2/9/15
to ats-lang-users
So i and j are static variables in the above? Assuming so since we are using '=='.
--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/7b89dc49-9b1e-4378-9d58-be334d10d7ca%40googlegroups.com.
gmhwxi
Feb 9, 2015, 9:09:01 PM2/9/15
to ats-lan...@googlegroups.com
Yes.
Brandon Barker
Feb 9, 2015, 9:22:49 PM2/9/15
to ats-lang-users
Sorry, I missed a lot of your first e-mail the first time. Now that I got it all, I think I'm a lot more clear. It makes sense, but it is one of those things that is so different from what I think of when dealing with programming on a day to day basis, I hope I don't forget the distinction between static values and proof values several months hence.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/6ea99d1c-42f3-4b5e-8724-4eb3d0f1bc15%40googlegroups.com.
Yannick Duchêne
May 19, 2015, 10:15:46 PM5/19/15
to ats-lan...@googlegroups.com
Le mardi 10 février 2015 02:17:15 UTC+1, Brandon Barker a écrit :
On Mon, Feb 9, 2015 at 8:15 PM, 'Yannick Duchêne' via ats-lang-users <ats-lan...@googlegroups.com> wrote:
Le mardi 10 février 2015 01:58:44 UTC+1, gmhwxi a écrit :A proof-value is in the dynamics of ATS.That was good to ask… I was so wrong…Wow, me too. So maybe I'm confused about what "dynamics" means. I was thinking it was anything that could have a representation in the generated code (e.g. C code).
May be a way to help to remind what‑is‑what, is to refer to the “constraint language” instead of to the “static language” (and what's not the constraint language is the dynamic language). The Bluishcoder blog use the expressions “constraint language” before saying it is what's also named the “static language”.
Reply all
Reply to author
Forward
0 new messages