unsolved constraint and multiplication

[Nick]

Hello.

Please tell me what is best to do to avoid the "unsolved constraint" error for

fun fact {n: int | n >= 0} .<n>. (n: int(n)): [n: int | n > 0] int(n) = if n > 0 then n * fact(n - 1) else 1

When I replace the multiplication sign with an addition sign, there is no error.
And how to make ATS work with the multiplication sign?

% patscc fact_nat.dats && ./a.out 5
/home/nick/ats/fact_nat.dats: 331(line=16, offs=87) -- 346(line=16, offs=102): error(3): unsolved constraint: C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(>); S2EVar(5254->S2Eapp(S2Ecst(mul_int_int); S2Evar(n(8480)), S2Evar(n$8635$8636$8639(14302)))), S2Eintinf(0)))
typechecking has failed: there are some unsolved constraints: please inspect the above reported error message(s) for information.
exit(ATS): uncaught exception: _2tmp_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)


Thanks.

[Hongwei Xi]

extern
fun
mymul{m,n:pos}(m: int m, n: int n): [mn:pos] int(mn)

fun fact {n: int | n >= 0} .<n>. (n: int(n)): [n: int | n > 0] int(n) = if n > 0 then mymul(n, fact(n - 1)) else 1

You need to prove that positive times positive yields positive (which is given as mymul above).

To implement mymul, you need to use theorem-proving supported in ATS.

Please see:

https://ats-lang.github.io/FROZEN000/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/c3154.html

The real issue here is that doing this manually is too expensive to be practical.

--
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 view this discussion visit https://groups.google.com/d/msgid/ats-lang-users/99c8981a-5980-44ef-b79f-0c68a9a9daacn%40googlegroups.com.

[Nick]

> The real issue here is that doing this manually is too expensive to be practical.

What is the practical way then?

вторник, 3 марта 2026 г. в 17:07:33 UTC+2, hw...@bu.edu:

[Dambaev Alexander]

I will suggest to use tail-recursive like:

```
fn
  fact
  {n: nat}
  (n: int n
  ):<>
  [m: pos]
  int m = loop( 1, n) where {
    extern praxi
      MUL
      {n,m:pos}
      {mn: int | mn == m * n}
      ( n: int n
      , m: int m
      , mn: int mn
      ):<>
      [ mn: pos | ( mn == n*m ) ]
      void
    fun
      loop
      {n: nat }
      {acc: pos}
      .<n>.
      ( acc: int acc
      , n: int n
      ):<>
      [m: pos ]
      int m =
      if n = 0
        then
          if acc < 1 then 1 else acc
        else loop(newacc, newn) where {
          val newacc = acc * n
          prval _ = MUL(acc, n, newacc)
          val newn = n - 1
        }
  }
```

вт, 3 мар. 2026 г. в 16:08, Nick <kost...@gmail.com>:

To view this discussion visit https://groups.google.com/d/msgid/ats-lang-users/d144ae3f-3c74-40c0-a7a2-388cba736641n%40googlegroups.com.

[Dambaev Alexander]

 `if acc < 1 then 1 else acc` should be replaced with `acc` (it is a left over which I forgot to delete)

вт, 3 мар. 2026 г. в 16:35, Dambaev Alexander <ice.r...@gmail.com>:

[Hongwei Xi]

>> > The real issue here is that doing this manually is too expensive to be practical.

>> What is the practical way then?

Maybe by building more powerful constraint solvers. The current constraint solver in ATS2

is very weak.

To view this discussion visit https://groups.google.com/d/msgid/ats-lang-users/d144ae3f-3c74-40c0-a7a2-388cba736641n%40googlegroups.com.

[Nick]

Thanks.

вторник, 3 марта 2026 г. в 19:04:16 UTC+2, ice.r...@gmail.com: