The thread of the errors in the docs

[Yannick Duchêne]

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]

Thank you very much for opening this thread. It is a VERY good idea!

[Yannick Duchêne]

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.

[Hongwei Xi]

The polynomial should be lam x => x * x - x - 110. Fixed.

--
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/92d37708-5bbb-4640-ad1f-354e75802fb5%40googlegroups.com.

[Yannick Duchêne]

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 :

[Hongwei Xi]

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.

--
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/94b73663-3d66-4a5d-9da5-3764d6bd1391%40googlegroups.com.

[Hongwei Xi]

Just want to add that using ndiv (division for natural numbers) also works.

You can write

ndiv(diff, 2)

or

(diff \ndiv 2)

[Yannick Duchêne]

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 :

[Hongwei Xi]

Fixed. Thanks!

--
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/f3dc8364-8b56-4646-b23e-37f5b5bb1f77%40googlegroups.com.

[Yannick Duchêne]

Le samedi 7 février 2015 15:41:00 UTC+1, gmhwxi a écrit :

Fixed. Thanks!

Thanks too! :p

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.

[Hongwei Xi]

Fixed. Thanks!

--

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/be35a807-b960-4dd3-8773-259a2f6ab988%40googlegroups.com.

[Yannick Duchêne]

Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :

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

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]

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.

[Yannick Duchêne]

Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :

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

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>. (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, https://groups.google.com/forum/#!topic/ats-lang-users/MsaDGpgDp0I , seems either `:<>` has to be removed from `ifact` or `:<>` added to `imul2`.

[Yannick Duchêne]

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 :

[Hongwei Xi]

Fixed. Thanks!

--

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/1409a3c0-1abb-4b65-9942-bec61f64042d%40googlegroups.com.

[Yannick Duchêne]

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 :

[…]

[gmhwxi]

This is fine. It just incurs a little bit extra typechecking.

[Yannick Duchêne]

Le mercredi 28 janvier 2015 18:49:32 UTC+1, Yannick Duchêne a écrit :

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

[…]

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

[Hongwei Xi]

Fixed. Thanks!

--
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/dc10bab4-ad2f-4f28-819f-9a87f478b074%40googlegroups.com.

[Yannick Duchêne]

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 :

[…]

[Hongwei Xi]

This section has not been written yet. I will find some time to do it.

--

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/4b1809f7-2099-4943-ae98-1c2064666d72%40googlegroups.com.

[Yannick Duchêne]

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]

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 (...) = ...