ATS2 syntax: praxi does not look like an axiomatization

Google Group
1

Using the same as in Prfn and prfun in ATS2
https://groups.google.com/forum/#!topic/ats-lang-users/8h5pqG6N0J0, I
can’t figure the syntax to be used with praxi. I can get it validated by
patscc, except not as an axiom, but as a proof, like with prfn and
prfun, while praxi should not be the same, I believe:
praxi three_is_beautiful (): BEAUTIFUL 3
patscc complains “the keyword [=] is needed”, which seems to suggest it
expects a proof. Indeed, if I do this:
praxi three_is_beautiful (): BEAUTIFUL 3 = B_3
then patscc accepts it.

What disturbs me, is this: if praxi is for axiomatizing, then why a proof
is needed? (I know axiomatizations are a dangerous beast to deal‑with with
care, but I still wish to understand)

The documentation gives its own other example in Example: Verified Fast
Exponentiation
http://www.ats-lang.org/DOCUMENT/INT2PROGINATS/HTML/x3168.html, which
does not compile neither:
praxi mul_istot {x, y: elt} (): [xy: elt] MUL (x, y, xy)
The same, it complains about a missing “=” which seems to mean it expects a
proof, not an axiom.

I can’t figure the syntax to be used, nor I can guess if axiomatization is
still allowed in ATS2 as it seems it was in ATS1.

2

Yes.On Wednesday, August 6, 2014 5:47:18 PM UTC-4, Yannick Duchêne wrote:

Le mercredi 6 août 2014 23:44:36 UTC+2, Brandon Barker a écrit :

Marginally related - what does the LF in ATS/LF stand for?

My guess is : Logical Framework (an area of type theory).

3

Indeed, I’m stupid. I have to do this:

patsopt -tc -s $SATS_FILE

I made the erroneous assumption patsopt take care of file extension.Le vendredi 8 août 2014 03:23:53 UTC+2, Yannick Duchêne a écrit :

Le vendredi 8 août 2014 02:54:55 UTC+2, gmhwxi a écrit :

arith_prf.sats: it is a SATS-file. So no ‘extern’ is needed.

I must be doing something wrong when I’m checking SATS files so, because
I get an error even trying the same in a SATS file. Here is what I do:

patsopt -tc -d $SATS_FILE

(may be I should open another thread for this different aspect)

4

Marginally related - what does the LF in ATS/LF stand for?

My guess is : Logical Framework (an area of type theory).

5

You need the keyword ‘extern’:

extern praxi three_is_beautiful : () → BEAUTIFUL (3)

What’s funny to my eyes, is what’s in
ATS2-Postiats-0.1.1/prelude/SATS/arith_prf.sats, on line 56 and 57:

praxi mul_make : {m,n:int} () - MUL (m, n, mn)
praxi mul_elim : {m,n:int} {p:int} MUL (m, n, p) - [p == mn] void

There is no extern and patscc loads the prelude without a complaint. If I
want to type check this file however (the same if I copy/paste this sample
in a SATS file), it complains the syntax is incorrect.

Does patscc or patsopt make a special case of files in prelude?

6

Does that mean prfun, prfn and praxi are the same in that regards?

praxi and prfun are treated the same in ATS/Postiats. prfn is a special
case of prfun.

Why was it abandoned in ATS2? (I feel it would be nice to be able to

enforce it when one want)

Well, not worth it :slight_smile:

However, you can still enforce it from the outside if there is really a
need.On Wednesday, August 6, 2014 5:38:43 PM UTC-4, Yannick Duchêne wrote:

Le mercredi 6 août 2014 23:33:41 UTC+2, gmhwxi a écrit :

You need the keyword ‘extern’:

extern praxi three_is_beautiful : () → BEAUTIFUL (3)

We posted the same at the same time (cheese).

In general, you need ‘extern’ when declaring a function in a DATS-file.

If you use praxi to introduce a proof function, then you basically
indicate that the proof function is not to be implemented (or proven).

By the way, even if you use ‘prfun’ to introduce a function, ATS2 does
not enforce
that the proof function be implemented. In ATS1, there was a way to
enforce it, but
it has been abandoned in ATS2.

Does that mean prfun, prfn and praxi are the same in that regards?

Why was it abandoned in ATS2? (I feel it would be nice to be able to
enforce it when one want)

7

You need the keyword ‘extern’:

extern praxi three_is_beautiful : () → BEAUTIFUL (3)

In general, you need ‘extern’ when declaring a function in a DATS-file.

If you use praxi to introduce a proof function, then you basically
indicate that the proof function is not to be implemented (or proven).

By the way, even if you use ‘prfun’ to introduce a function, ATS2 does not
enforce
that the proof function be implemented. In ATS1, there was a way to enforce
it, but
it has been abandoned in ATS2.On Wednesday, August 6, 2014 5:16:04 PM UTC-4, Yannick Duchêne wrote:

Using the same as in Prfn and prfun in ATS2
https://groups.google.com/forum/#!topic/ats-lang-users/8h5pqG6N0J0, I
can’t figure the syntax to be used with praxi. I can get it validated by
patscc, except not as an axiom, but as a proof, like with prfn and
prfun, while praxi should not be the same, I believe:
praxi three_is_beautiful (): BEAUTIFUL 3
patscc complains “the keyword [=] is needed”, which seems to suggest it
expects a proof. Indeed, if I do this:
praxi three_is_beautiful (): BEAUTIFUL 3 = B_3
then patscc accepts it.

What disturbs me, is this: if praxi is for axiomatizing, then why a
proof is needed? (I know axiomatizations are a dangerous beast to deal‑with
with care, but I still wish to understand)

The documentation gives its own other example in Example: Verified Fast
Exponentiation
http://www.ats-lang.org/DOCUMENT/INT2PROGINATS/HTML/x3168.html, which
does not compile neither:
praxi mul_istot {x, y: elt} (): [xy: elt] MUL (x, y, xy)
The same, it complains about a missing “=” which seems to mean it expects
a proof, not an axiom.

I can’t figure the syntax to be used, nor I can guess if axiomatization is
still allowed in ATS2 as it seems it was in ATS1.

8

You need the keyword ‘extern’:

extern praxi three_is_beautiful : () → BEAUTIFUL (3)

We posted the same at the same time (cheese).

In general, you need ‘extern’ when declaring a function in a DATS-file.

If you use praxi to introduce a proof function, then you basically
indicate that the proof function is not to be implemented (or proven).

By the way, even if you use ‘prfun’ to introduce a function, ATS2 does not
enforce
that the proof function be implemented. In ATS1, there was a way to
enforce it, but
it has been abandoned in ATS2.

Does that mean prfun, prfn and praxi are the same in that regards?

Why was it abandoned in ATS2? (I feel it would be nice to be able to
enforce it when one want)

9

arith_prf.sats: it is a SATS-file. So no ‘extern’ is needed.On Thu, Aug 7, 2014 at 8:52 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

Le mercredi 6 août 2014 23:33:41 UTC+2, gmhwxi a écrit :

You need the keyword ‘extern’:

extern praxi three_is_beautiful : () → BEAUTIFUL (3)

What’s funny to my eyes, is what’s in
ATS2-Postiats-0.1.1/prelude/SATS/arith_prf.sats, on line 56 and 57:

praxi mul_make : {m,n:int} () - MUL (m, n, mn)
praxi mul_elim : {m,n:int} {p:int} MUL (m, n, p) - [p == mn] void

There is no extern and patscc loads the prelude without a complaint. If
I want to type check this file however (the same if I copy/paste this
sample in a SATS file), it complains the syntax is incorrect.

Does patscc or patsopt make a special case of files in prelude?

–
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/fc87478c-4bf8-431f-a954-3b120c38104d%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/fc87478c-4bf8-431f-a954-3b120c38104d%40googlegroups.com?utm_medium=email&utm_source=footer
.

10

Or do

patscc -tcats $SATS_FILE

patscc can take care of the .sats extension properly.On Thursday, August 7, 2014 9:25:36 PM UTC-4, Yannick Duchêne wrote:

Indeed, I’m stupid. I have to do this:

patsopt -tc -s $SATS_FILE

I made the erroneous assumption patsopt take care of file extension.

Le vendredi 8 août 2014 03:23:53 UTC+2, Yannick Duchêne a écrit :

Le vendredi 8 août 2014 02:54:55 UTC+2, gmhwxi a écrit :

arith_prf.sats: it is a SATS-file. So no ‘extern’ is needed.

I must be doing something wrong when I’m checking SATS files so, because
I get an error even trying the same in a SATS file. Here is what I do:

patsopt -tc -d $SATS_FILE

(may be I should open another thread for this different aspect)

11

Marginally related - what does the LF in ATS/LF stand for?

Brandon Barker
brandon…@gmail.comOn Wed, Aug 6, 2014 at 5:42 PM, Brandon Barker brandon...@gmail.com wrote:

Brandon Barker
brandon...@gmail.com

On Wed, Aug 6, 2014 at 5:38 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

Le mercredi 6 août 2014 23:33:41 UTC+2, gmhwxi a écrit :

You need the keyword ‘extern’:

extern praxi three_is_beautiful : () → BEAUTIFUL (3)

We posted the same at the same time (cheese).

In general, you need ‘extern’ when declaring a function in a DATS-file.

If you use praxi to introduce a proof function, then you basically
indicate that the proof function is not to be implemented (or proven).

By the way, even if you use ‘prfun’ to introduce a function, ATS2 does
not enforce
that the proof function be implemented. In ATS1, there was a way to
enforce it, but
it has been abandoned in ATS2.

I assume that typechecking would still fail if you implemented it
incorrectly, so this could be purposefully done
if there were safety concerns (i.e. assert 1=0).

Does that mean prfun, prfn and praxi are the same in that regards?

Why was it abandoned in ATS2? (I feel it would be nice to be able to
enforce it when one want)

–
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/2fb81e59-a327-49a3-bbab-02b2e5d7a437%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/2fb81e59-a327-49a3-bbab-02b2e5d7a437%40googlegroups.com?utm_medium=email&utm_source=footer
.

12

There is no wording on this in the documentations, I just noticed praxi
seems to always appears preceded by extern in ATS2 sources and sample
sources (not the with ones in the HTML documents though).

This works:
extern praxi three_is_beautiful (): BEAUTIFUL 3

I’m still unsure. Is this still handled as an axiomatization or does it
expects some external proof later?Le mercredi 6 août 2014 23:16:04 UTC+2, Yannick Duchêne a écrit :

Using the same as in Prfn and prfun in ATS2
https://groups.google.com/forum/#!topic/ats-lang-users/8h5pqG6N0J0, I
can’t figure the syntax to be used with praxi. I can get it validated by
patscc, except not as an axiom, but as a proof, like with prfn and
prfun, while praxi should not be the same, I believe:
praxi three_is_beautiful (): BEAUTIFUL 3
patscc complains “the keyword [=] is needed”, which seems to suggest it
expects a proof. Indeed, if I do this:
praxi three_is_beautiful (): BEAUTIFUL 3 = B_3
then patscc accepts it.

What disturbs me, is this: if praxi is for axiomatizing, then why a
proof is needed? (I know axiomatizations are a dangerous beast to deal‑with
with care, but I still wish to understand)

13

arith_prf.sats: it is a SATS-file. So no ‘extern’ is needed.

I must be doing something wrong when I’m checking SATS files so, because I
get an error even trying the same in a SATS file. Here is what I do:

patsopt -tc -d $SATS_FILE

(may be I should open another thread for this different aspect)

14

patopt -tc -s $SATS_FILEOn Thu, Aug 7, 2014 at 9:23 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

Le vendredi 8 août 2014 02:54:55 UTC+2, gmhwxi a écrit :

arith_prf.sats: it is a SATS-file. So no ‘extern’ is needed.

I must be doing something wrong when I’m checking SATS files so, because
I get an error even trying the same in a SATS file. Here is what I do:

patsopt -tc -d $SATS_FILE

(may be I should open another thread for this different aspect)

–
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/0e52497f-12eb-400b-b90c-e49ca31cb3cb%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/0e52497f-12eb-400b-b90c-e49ca31cb3cb%40googlegroups.com?utm_medium=email&utm_source=footer
.

15

Brandon Barker
brandon...@gmail.com

You need the keyword ‘extern’:

extern praxi three_is_beautiful : () → BEAUTIFUL (3)

We posted the same at the same time (cheese).

In general, you need ‘extern’ when declaring a function in a DATS-file.

If you use praxi to introduce a proof function, then you basically
indicate that the proof function is not to be implemented (or proven).

By the way, even if you use ‘prfun’ to introduce a function, ATS2 does
not enforce
that the proof function be implemented. In ATS1, there was a way to
enforce it, but
it has been abandoned in ATS2.

I assume that typechecking would still fail if you implemented it
incorrectly, so this could be purposefully done
if there were safety concerns (i.e. assert 1=0).