What is difference between prfun and praxi?

[Kiwamu Okabe]

Hi all,

I am reading "Introduction to Programming in ATS" that is saying:

> http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x3245.html
> The keyword praxi indicates that mul_assoc is treated as a form of axiom, which is not expected to be implemented.

However, following "mul_nx0_0" proof-function is introduced without
any implementation.

https://github.com/githwxi/ATS-Postiats/blob/679835b7f7d4ffdbc34112f8f423e5c37ce43403/doc/BOOK/INT2PROGINATS/CODE/CHAP_THMPRVING/misc.dats#L142

What is difference between prfun and praxi?

Thank's,
--
Kiwamu Okabe at METASEPI DESIGN

[gmhwxi]

Originally, praxi is for axioms and prfun for proof functions that need to be implemented.

However, this is not enforced in the current implementation of ATS.

[Kiwamu Okabe]

Hi Hongwei,

On Fri, Mar 27, 2015 at 7:59 PM, Hongwei Xi <gmh...@gmail.com> wrote:
> Originally, praxi is for axioms and prfun is for proof functions that needs

> to be implemented.
> However, this is not enforced in the current implementation of ATS.

O.K. It's clear for me.

[Barry Schwartz]

Hongwei Xi <gmh...@gmail.com> skribis:

> Originally, praxi is for axioms and prfun is for proof functions that needs
> to be implemented.
> However, this is not enforced in the current implementation of ATS.

I am a bit curious if enforcement is in the plans.

I could see it as a ‘warning only’ stylistic check. My reasoning is
that proofs in ATS are more to ensure you did not make an error in
your statement than they are a formal requirement; thus there is no
fundamental difference between a praxi and a prfun.

[Shea Levy]

I would definitely appreciate a flag to actually check if prfuns are implemented. I understand why the default is as it is but I’d prefer the extra assurance from the compiler rather than having to adopt coding standards enforcing actually proving proofs.

~Shea

> --
> 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/20150327211206.GB3962%40crud.

[gmhwxi]

Enforcing this requires some form of global flow analysis.
I hope that someone will have the motivation to implement it someday.

My attitude towards the need for implementing a particular prfun is that it should
be programmer-centric: The programmer is in the position to make that decision
(rather than it is mandated by the typehecker).

This is also a kind of fairness issue for me. When writing code, one does all sorts
reasoning implicitly. If someone wants to introduce proof functions to make some reasoning
more explicit, why should the person be penalized with the requirement of constructing explicit
proofs for the introduced proof functions?

[gmhwxi]

There is such a flag in ATS1, but it is not really useful as turning it on almost always leads to
the output of a great number of warning/error messages. As I see it, one needs to re-build the basic
library support for ATS in order to make such a flag useful.

[Barry Schwartz]

gmhwxi <gmh...@gmail.com> skribis:

> This is also a kind of fairness issue for me. When writing code, one does
> all sorts
> reasoning implicitly. If someone wants to introduce proof functions to make
> some reasoning
> more explicit, why should the person be penalized with the requirement of
> constructing explicit
> proofs for the introduced proof functions?

I’d be perfectly happy with the choice of prfun vs praxi being
entirely stylistic, as long as one could count on that. My concern is
having code broken by a future version of ATS that enforces a
difference.

[gmhwxi]

I often use 'praxi' to indicate something that cannot be proven
within ATS. It refers to a form of truth that is external to ATS (e.g.,
the fact that the sun rises from the east)

I use prfun to indicate that a statement can be established based on
some existing ones (but I may not be willing to construct a proof for it).

In the future, if we really need to find a way to ensure that a declared proof
function must be given a proof, then we could always try to introduce another
keyword for doing so.

[Barry Schwartz]

gmhwxi <gmh...@gmail.com> skribis:

> I often use 'praxi' to indicate something that cannot be proven
> within ATS. It refers to a form of truth that is external to ATS (e.g.,
> the fact that the sun rises from the east)
>
> I use prfun to indicate that a statement can be established based on
> some existing ones (but I may not be willing to construct a proof for it).
>
> In the future, if we really need to find a way to ensure that a declared
> proof
> function must be given a proof, then we could always try to introduce
> another
> keyword for doing so.

That’s a good scheme. You probably can understand my concern that the
current phrasing implies likely that one day proofs would be forced.