Recursion inside well founded dataprops: any implicite termination metrics?

Google Group
1

Given this:

dataprop R(i:int) =
| R1(1)
| {i > 1} RN(i) of R(i-1)

One may have this:

prfun f {i:int; i >= 1} .. (pf:R(i)): int =
case+ pf of
| R1() => 1
| RN(pf’:R(i-1)) => f(pf’) + 1

However, given this:

dataprop R =
| R1
| RN of R

One can’t have this:

prfun f .<>. (pf:R): int =
case+ pf of
| R1() => 1
| RN(pf’) => f(pf’) + 1

Is there a way to have a termination metric for this?

I feel to guess the answer is likely “no”, and I feel to know why:
Isabelle/HOL, has something looking like dataprop which is checked to be
inductive (based on a well founded recursion). ATS does not check it (it
has general recursive definitions, not checked to be inductive
definitions), so that may be the reason why it can’t handle such a case
without an explicit index.

While I feel to guess the answer, I prefer to ask, in case of I just missed
something. If the answer is “yes”, then that would be nice as more natural.

2

ATS is not a formal theorem-proving system; its focus is on using
theorem-proving
to locate/fix bugs in programs. Theorem-proving in ATS is informal; it is
a bit like how
people construct mathematical proofs using pencil/paper.

Learning what can be expressed and what can’t be (or can be not the
expected way) , is a big part or learning ATS.

May be I’m expecting too much from dataprop. I will later start to look at
absprop and praxi more closely, and better see when use one or the other.Le mardi 22 décembre 2015 22:40:30 UTC+1, gmhwxi a écrit :

NON_SENSE is actually inductive. The following is a non-inductive
example:

dataprop D = D of (D → D)

So I need to review the definition (red-face)

3

In ATS, a dataprop needs to be defined inductively, but this requirement
is not
formally enforced. Still, for your example, explicit indexes are needed in
order to
establish termination in ATS.

So something like:

dataprop NON_SENSE =
| NON_SENSE_CONS of NON_SENSE

should never be written in ATS? (although it won’t complain)

ATS is not a formal theorem-proving system; its focus is on using
theorem-proving
to locate/fix bugs in programs. Theorem-proving in ATS is informal; it is
a bit like how
people construct mathematical proofs using pencil/paper.

This is reasonable.

4

NON_SENSE is actually inductive. The following is a non-inductive example:

dataprop D = D of (D → D)On Tue, Dec 22, 2015 at 4:38 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

Le mardi 22 décembre 2015 22:14:34 UTC+1, gmhwxi a écrit :

In ATS, a dataprop needs to be defined inductively, but this requirement
is not
formally enforced. Still, for your example, explicit indexes are needed
in order to
establish termination in ATS.

So something like:

dataprop NON_SENSE =
| NON_SENSE_CONS of NON_SENSE

should never be written in ATS? (although it won’t complain)

ATS is not a formal theorem-proving system; its focus is on using
theorem-proving
to locate/fix bugs in programs. Theorem-proving in ATS is informal; it is
a bit like how
people construct mathematical proofs using pencil/paper.

This is reasonable.

–
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 https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/8b89dfbb-a462-431b-a47e-5c654e90bf70%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/8b89dfbb-a462-431b-a47e-5c654e90bf70%40googlegroups.com?utm_medium=email&utm_source=footer
.

5

In ATS, a dataprop needs to be defined inductively, but this requirement is
not
formally enforced. Still, for your example, explicit indexes are needed in
order to
establish termination in ATS.

ATS is not a formal theorem-proving system; its focus is on using
theorem-proving
to locate/fix bugs in programs. Theorem-proving in ATS is informal; it is a
bit like how
people construct mathematical proofs using pencil/paper.On Tuesday, December 22, 2015 at 3:55:57 PM UTC-5, Yannick Duchêne wrote:

Given this:

dataprop R(i:int) =
| R1(1)
| {i > 1} RN(i) of R(i-1)

One may have this:

prfun f {i:int; i >= 1} .. (pf:R(i)): int =
case+ pf of
| R1() => 1
| RN(pf’:R(i-1)) => f(pf’) + 1

However, given this:

dataprop R =
| R1
| RN of R

One can’t have this:

prfun f .<>. (pf:R): int =
case+ pf of
| R1() => 1
| RN(pf’) => f(pf’) + 1

Is there a way to have a termination metric for this?

I feel to guess the answer is likely “no”, and I feel to know why:
Isabelle/HOL, has something looking like dataprop which is checked to be
inductive (based on a well founded recursion). ATS does not check it (it
has general recursive definitions, not checked to be inductive
definitions), so that may be the reason why it can’t handle such a case
without an explicit index.

While I feel to guess the answer, I prefer to ask, in case of I just
missed something. If the answer is “yes”, then that would be nice as more
natural.