Termination Checking

[Mike Jones]

In the book, chapter 9, Termination-Checking for Recursive Functions, code iseven and isodd 

There is a comment that the metrics (n,0) and (n,1) can also be used.

Is this a generic statement of theory, or is there a way to specify this in the statics of the example? If it is expressible, how do the constants 0/1 apply?

Is there any real difference between .<2*n>. and .<2*n+1>. vs .<n>, and .<n+1>, other than giving some intuition to the reader?

[gmhwxi]

Yes, you can do it like this:

fun isevn{n:nat} .<n,0>.
  (n: int n): bool = if n = 0 then true else isodd (n-1)
and isodd{n:nat} .<n,1>.
  (n: int n): bool = not (isevn n)

It does not work if you use <n> and <n+1> because this means that the metric
attached to 'isodd' in the body of 'isevn' is <n+1-1>, which is the same as the one attached
to 'isevn'.

[Mike Jones]

But isn't <2*n+1-1> the same as <2*n>?

As for .<n, 0/1>, what does the 0/1 do? From the book, there is a lexical order of values that is applied to the function calls. But there is only one call in this case, so it is not clear what 0/1 applies to. Perhaps the last element in the <tuple> has a special meaning or variables can be paired with a number?

[gmhwxi]

isodd(n-1) is in the body of isevn(n); the metric
attached to isodd is 2*(n-1)+1=2*n-1 and the metric attached to
isevn is 2*n. So termination metric does go down.

Say that <n,0> and <n,1> are assigned to isevn(n) and isodd(n),
respectively. In the body of isodd(n), we have a call isevn(n).
Since <n,0> is less than <n,1>, termination metric does go down
in this case as well.

[Mike Jones]

Ok, I finally see how this works and how the metric works. Basically you substitute the value in the call into the metric and it needs to go down. But I assume this has to also be compared to the n = 0. Is it possible to make the metric go up, and then compare against n < 10?

isodd(n-1) is in the body of isevn(n); the metric
attached to isodd is 2*(n-1)+1=2*n-1 and the metric attached to
isevn is 2*n. So termination metric does go down.

This I don't quite understand. I see that when n-1 is substituted into <n>, it goes down. But the role of the constant is not clear. In what sense if a pair of values less than or greater than other than some lexical convention like when you alphabetize a word, where the 0/1 breaks a tie?

[Hongwei Xi]

You use 10-n as your metric.

On Tue, Nov 3, 2015 at 8:58 PM, Mike Jones <proc...@gmail.com> wrote:

Ok, I finally see how this works and how the metric works. Basically you substitute the value in the call into the metric and it needs to go down. But I assume this has to also be compared to the n = 0. Is it possible to make the metric go up, and then compare against n < 10?

isodd(n-1) is in the body of isevn(n); the metric
attached to isodd is 2*(n-1)+1=2*n-1 and the metric attached to
isevn is 2*n. So termination metric does go down.

Yes, 0/1 is for breaking a tie. For instance, <n, 1000000> is less than <n+1, 0>; <n, 0> is less than <n, 1>.

 

This I don't quite understand. I see that when n-1 is substituted into <n>, it goes down. But the role of the constant is not clear. In what sense if a pair of values less than or greater than other than some lexical convention like when you alphabetize a word, where the 0/1 breaks a tie?

 

Say that <n,0> and <n,1> are assigned to isevn(n) and isodd(n),
respectively. In the body of isodd(n), we have a call isevn(n).
Since <n,0> is less than <n,1>, termination metric does go down
in this case as well.

--
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/17ff9ac7-fa31-470a-a460-a5fab8edc53c%40googlegroups.com.

[Mike Jones]

I gave this a try, but found a tricky constraint problem:

    fun loop_read {c,i: nat | c <= 255; i <= c} .<c-i>. (cnt: int(c), idx: int(i)): void = let

      val data = i2c_read(an)

      val () = packetOutContentsExt[idx] := data

    in

      if (idx < cnt) then loop_read (cnt, idx + 1) else ()

    end

    val ()      = if ((ok = OK) && (count' > 0)) 

                  then case+ p of 

                       | NoPec() => loop_read(count, 1)

                       | Pec() => loop_read(count, 0)

The compile complains about the NoPec() case using 1. I can replace 1 with count or 0 and it works, but somehow it treats 1 differently. I tried casting 1 with natLte, etc, but no luck. Seems like the complier tries to do the right thing with constants, but not always. What is the secret sauce to make a 1 that is a nat so it satisfies i <= c ?

The error is:

error(3): unsolved constraint: C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(<=); S2EVar(2385->S2Eintinf(1)), S2EVar(2384->S2Evar(i$3922$3923$3924$3925(8097)))))

typechecking has failed: there are some unsolved constraints: please inspect the above reported error message(s) for information.

exit(ATS): uncaught exception: _2home_2hwxi_2Research_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)

[Hongwei Xi]

When you call loop_read(count, 1), 1 <= count needs to be proven.

&& may not have the type you expected. Try to change && to *.

--
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/4a51f42f-1b5e-437f-93ef-a231672c6f77%40googlegroups.com.

[Mike Jones]

This compiles. I guess the compiler can't deal with the &&.

But, how would I use '*'; multiplication is not compatible with the bool type.

    val ()      = if ok = OK 

                  then  if count' > 0

                        then case+ pec of 

                             | NoPec() => loop_read(count', 1)

                             | Pec() => loop_read(count', 0)

[Hongwei Xi]

* is overloaded.

b1 * b2 = b1 && b2 but the former gives you a more accurate type.

--
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/3b014e31-90a7-4db2-bd59-f67a2c9c7263%40googlegroups.com.