ATS2 syntax: praxi does not look like an axiomatization

[Yannick Duchêne]

Using the same as in Prfn and prfun in ATS2, 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, 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.

[gmhwxi]

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.

[Yannick Duchêne]

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?

[Yannick Duchêne]

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)

[Brandon Barker]

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.

[Brandon Barker]

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

Brandon Barker
brandon...@gmail.com

[Yannick Duchêne]

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).

 

[gmhwxi]

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 :)

However, you can still enforce it from the outside if there is really a need.

[gmhwxi]

Yes.

[Yannick Duchêne]

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} () -<prf> MUL (m, n, m*n)
praxi mul_elim : {m,n:int} {p:int} MUL (m, n, p) -<prf> [p == m*n] 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?

[Hongwei Xi]

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

--

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.

[Yannick Duchêne]

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)

[Hongwei Xi]

patopt -tc -s $SATS_FILE

--

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.

[Yannick Duchêne]

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.

[gmhwxi]

Or do

patscc -tcats $SATS_FILE

patscc can take care of the .sats extension properly.