The thread of the errors in the docs

Yannick_Duchene · January 28, 2015, 5:49pm

I don’t remember of any already existing one, so I’m opening this thread
where to report any errors in the docs, instead of opening a new thread for
each possible eventual errors (saying that, I don’t want to mean there are
many).

My first case.

In http://ats-lang.sourceforge.net/DOCUMENT/ATS2TUTORIAL/HTML/c309.html :

 val
 fact =
 fix f(x: int): int =>
   if x > 0 then x * fact(x-1) else 1
 (* end of [fact] *)

Sure it should be “f(x-1)” instead of “fact(x-1)”

gmhwxi · May 22, 2015, 2:00pm

This section has not been written yet. I will find some time to do it.On Thu, May 21, 2015 at 5:50 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

Yannick_Duchene · February 7, 2015, 12:27pm

A tiny thing, a typo here:
http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/c2843.html

“Within the ATS programming langauge system” (should be “language”)Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :

gmhwxi · February 6, 2015, 5:26pm

Thanks for pointing it out.

I have changed (diff / 2) into half(diff). The type assigned to integer
division in ATS2
is no longer strong enough for this example.On Fri, Feb 6, 2015 at 12:07 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

Yannick_Duchene · February 7, 2015, 3:38pm

Thanks too!

I found another typo, more annoying this one, as it ends into a
type‑checker error. In
http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x2905.html
“prfun mut_istot {m,n:int} (): [p:int] MUL (m, n, p)” the name “mut_istot”
should be “mul_istot” or else the proof function implementation which
follows fails.

Yannick_Duchene · February 6, 2015, 5:07pm

In http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x2528.html ,
about the second definition of the isqrt function, this sentence looks
strange to me: “The following code we obtain after proper modification does
pass typechecking”. Actually, it does not: both patscc --typecheck and
patscc -tcats tells about one unsolved constraint error and two unsolved
termination constraints errors.Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :

Yannick_Duchene · May 20, 2015, 5:08am

Unless I’ve missed something, I believe there is a repeated error in
http://ats-lang.sourceforge.net/DOCUMENT/ATS2TUTORIAL/HTML/HTMLTOC/c642.html
: n is never decremented.

At least, adding a termination metric, without touching the function’s
logic, makes ATS catch an error:
fun fact
{n: int} (n: int n): int = let
fun loop {n: int} .. (n: int n, res: int): int =
if n > 0 then loop (n, n * res) else res
// end of [loop]
in
loop (n, 1)
end // end of [fact]

This one is OK:
fun fact
{n: nat} (n: int n): int = let
fun loop {n: nat} .. (n: int n, res: int): int =
if n > 0 then loop (n - 1, n * res) else res
// end of [loop]
in
loop (n, 1)
end // end of [fact]

This seems to be the same with the two preceding functions.

Yannick_Duchene · May 14, 2015, 12:28pm

Not an error, just a comment.

On the page
http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x2110.html
, the definition of array_copy_from_list, starts like this:

implement
{a}(tmp)
array_copy_from_list
(A, xs) = let

Looking only at the declaration part, how a is used is not visible. It is
made visible later, making use of type inference:

  […] = let

//
fun loop
(
p: ptr, xs: list0 (a)
) : void =

Just wondered if ever this more easy to follow if x: list0 (a) was on the
outer declaration, so that the relation would be more obvious. Like this:

implement
{a}(tmp)
array_copy_from_list
(A, xs: list0 (a)) = let

(provided I’ve not missed anything and I’m saying something wrong, as I’m
not yet used to templates)Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :

Yannick_Duchene · February 10, 2015, 12:52pm

In
http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3166.html
, an invocation of imul2 is wrong. In val (pfmul | r1) = (i+1) imul2 r
should either be rewritten as val (pfmul | r1) = (i+1) \imul2 r or as
val (pfmul | r1) = imul2((i+1), r)Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :

Yannick_Duchene · December 11, 2015, 8:02pm

Not an error, rather what I believe may be misleading, if I understand
correctly.

In “Example: Verified Fast Exponentiation”
http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3252.html

An absprop MUL is defined, then follows the declaration of a dynamic
function mul_elt_elt, returning a proof of MUL(x, y, xy).

This function has no body, and indeed, there is no way for a dynamic
function to instantiate a MUL, as it’s an abstract proposition, thus, not
defining any dynamic constructor which would be usable from the body of a
dynamic function. This function declared with fun, behaves like a
praxi, and I though this may be better to use praxi.

I just wondered what about systematically use praxi is these cases, as it
underlines it’s axiomatic (and one should always be careful with axioms).

Or is there a reason for it to be declared with fun instead of praxi?
Especially in the documentation, praxi would be better, isn’t it?

There are two others in “Linear Channels for Asynchronous IPC”
http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x4355.html

queue_isnil declared with fun, returning a proof of ISNIL(id, b) and
ISNIL is an absprop
queue_isful declared with fun, returning a proof of ISFUL(id, b) and
ISFUL is an absprop too.

Unless I’m wrong…Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :

gmhwxi · February 7, 2015, 4:01pm

Fixed. Thanks!On Sat, Feb 7, 2015 at 10:38 AM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

gmhwxi · January 28, 2015, 7:03pm

Thank you very much for opening this thread. It is a VERY good idea!On Wednesday, January 28, 2015 at 12:49:32 PM UTC-5, Yannick Duchêne wrote:

gmhwxi · December 12, 2015, 2:27am

Originally (that is, in ATS1), there is checking to ensure that each
declared
prfun is implemented; if a prfun is not implemented, it needs to be
declared as a praxi.
In ATS2, this kind of checking is abandoned (as it seems too unwieldy in
practice).
So, there is little difference between prfun and praxi in ATS2.

Even for an abstract prop, using prfun still makes sense as the abstract
prop can be
implemented at some point. Say you have an abstract prop FOO. You can do

assume FOO = …

implement
lemma_for_FOO (…) = …On Friday, December 11, 2015 at 3:02:17 PM UTC-5, Yannick Duchêne wrote:

gmhwxi · May 14, 2015, 2:10pm

This is fine. It just incurs a little bit extra typechecking.On Thursday, May 14, 2015 at 8:28:25 AM UTC-4, Yannick Duchêne wrote:

Yannick_Duchene · February 10, 2015, 12:28pm

Not an error, more an enhancement.

In
http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3121.html
, imul2 is given this signature:

fun imul2{i,j:int}
(i: int i, j: int j): [ij:int] (MUL(i, j, ij) | int ij)

After
http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3140.html
, if I check this in a DATS file…

extern fn imul2
{i,j:int}
(i: int i, j: int j): [ij:int] (MUL(i, j, ij) | int ij)

dataprop FACT(int, int) =
| FACTbas(0, 1)
| {n:nat} {r1,r:int} FACTind(n, r) of (FACT(n-1, r1), MUL(n, r1, r))

fun ifact {n:nat} .. (n: int(n)):<> [r:int] (FACT(n, r) | int r) =
if n = 0
then (FACTbas() | 1)
else
let
val (pf1 | r1) = ifact (n-1) // pf1: FACT(n-1, r1)
val (pfmul | r) = imul2 (n, r1) // pfmul: FACT(n, r1, r)
in (FACTind(pf1, pfmul) | r)
end

… I get the error or warning “some disallowed effects may be incurred: 1”
on line #15 (the one which invokes imul2).

After an another topic,
Redirecting to Google Groups , seems
either :<> has to be removed from ifact or :<> added to imul2.

gmhwxi · February 10, 2015, 2:36pm

Fixed. Thanks!On Tue, Feb 10, 2015 at 7:52 AM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

Yannick_Duchene · May 21, 2015, 9:50pm

I’m a bit unsure with this one, rather a doubt.

In
http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3658.html
, the wording suggest something is to come, but the page contains a single
sentence.Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :

Yannick_Duchene · February 9, 2015, 11:38pm

In
http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x3076.html
, in the sentence “ATS with theorem-proving systems such as Isabel and Coq
[…]”, Isabelle is misspelled: “le” is missing at the end.

gmhwxi · February 10, 2015, 12:40am

Fixed. Thanks!

I have never used Isabelle

Tried Nuprl a bit and Coq a bit, too.

My theorem-proving experience largely came from
using/implementing a system called TPS, which was
a project led by Prof. Peter Andrews at CMU.On Monday, February 9, 2015 at 6:38:39 PM UTC-5, Yannick Duchêne wrote:

Yannick_Duchene · February 1, 2015, 12:17pm

Unless I’ve missed something, there is one in
http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x794.html

It says “For instance, calling rtfind on the polynomial function lam x => x

x - x + 110 returns 11”. But x² - x + 110 = 0 has no solution in ℝ.
Testing the example returns the erroneous result 463410 on my 32 bits
machine.Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :

Topic		Replies	Views
Not such a great first experience malheureusement Google Group	8	429	July 16, 2014
ATS2 syntax: praxi does not look like an axiomatization Google Group	14	597	August 8, 2014
Frustrated with the documentation Google Group	7	397	August 17, 2014
Defining new static terms of ullint values? Google Group	16	701	August 6, 2014
Patscc-pp Google Group	14	849	February 11, 2016

The thread of the errors in the docs

Related topics