Recursion inside well founded dataprops: any implicite termination metrics?

[Yannick Duchêne]

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} .<i>. (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.

[gmhwxi]

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.

[Yannick Duchêne]

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.

[Hongwei Xi]

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

dataprop D =  D of (D -> D)

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

[Yannick Duchêne]

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

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)