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)
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.
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?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.
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)
--
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.
val () = if ok = OK then if count' > 0 then case+ pec of | NoPec() => loop_read(count', 1) | Pec() => loop_read(count', 0)
--
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.