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 .<2n>. and .<2n+1>. vs ., and
.<n+1>, other than giving some intuition to the reader?
When you call loop_read(count, 1), 1 <= count needs to be proven.
&& may not have the type you expected. Try to change && to *.On Wed, Nov 4, 2015 at 12:43 AM, Mike Jones proc...@gmail.com wrote:
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)–
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
https://groups.google.com/d/msgid/ats-lang-users/4a51f42f-1b5e-437f-93ef-a231672c6f77%40googlegroups.com?utm_medium=email&utm_source=footer
.
But isn’t <2n+1-1> the same as <2n>?
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 has a special meaning or variables can be
paired with a number?On Tuesday, November 3, 2015 at 9:18:22 AM UTC-7, gmhwxi wrote:
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 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’.On Tuesday, November 3, 2015 at 11:00:27 AM UTC-5, Mike Jones wrote:
In the book, chapter 9, Termination-Checking for Recursive Functions,
code iseven and isoddThere 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 .<2n>. and .<2n+1>. vs ., and
.<n+1>, other than giving some intuition to the reader?
You use 10-n as your metric.
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=2n-1 and the metric attached to
isevn is 2n. 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>.
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)
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 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’.On Tuesday, November 3, 2015 at 11:00:27 AM UTC-5, Mike Jones wrote:
In the book, chapter 9, Termination-Checking for Recursive Functions, code
iseven and isoddThere 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 .<2n>. and .<2n+1>. vs ., and
.<n+1>, other than giving some intuition to the reader?
b1 * b2 = b1 && b2 but the former gives you a more accurate type.On Wed, Nov 4, 2015 at 9:37 AM, Mike Jones proc...@gmail.com wrote:
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)–
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
https://groups.google.com/d/msgid/ats-lang-users/3b014e31-90a7-4db2-bd59-f67a2c9c7263%40googlegroups.com?utm_medium=email&utm_source=footer
.
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)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=2n-1 and the metric attached to
isevn is 2n. So termination metric does go down.
This I don’t quite understand. I see that when n-1 is substituted into ,
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?
isodd(n-1) is in the body of isevn(n); the metric
attached to isodd is 2*(n-1)+1=2n-1 and the metric attached to
isevn is 2n. 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.On Tuesday, November 3, 2015 at 7:55:32 PM UTC-5, Mike Jones wrote:
But isn’t <2n+1-1> the same as <2n>?
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 has a special meaning or variables can be
paired with a number?On Tuesday, November 3, 2015 at 9:18:22 AM UTC-7, gmhwxi wrote:
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 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’.On Tuesday, November 3, 2015 at 11:00:27 AM UTC-5, Mike Jones wrote:
In the book, chapter 9, Termination-Checking for Recursive Functions,
code iseven and isoddThere 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 .<2n>. and .<2n+1>. vs ., and
.<n+1>, other than giving some intuition to the reader?