trying to compute 4x4 Laver table

[tromp]

How do I make this program work?

import Base#

laver(a:Nat, b:Nat) : Nat if a==0 then b else if b==3 then a-1 else laver(laver(a,b+1),a-1)

main : Nat laver(3,1)

When run with fm -d main/main I always get (node:67386) UnhandledPromiseRejectionWarning: RangeError: Maximum call stack size exceeded

Changing Nat to Number gives (node:67400) UnhandledPromiseRejectionWarning: TypeError: Cannot read property '0' of undefined

[LoPoHa]

If you typecheck first (with -t) you get something like the following error:

[ERROR]
Type mismatch.
- Found type... Number
- Instead of... Nat
- When checking 0
- With context:
- a : Nat
- b : Nat
- On line 4, col 11, file test.fm:
   1| import Base#
   2| 
   3| laver(a:Nat, b:Nat) : Nat
   4|   if a == 0 then 
   5|     b 
   6|   else if b == 3 then 
   7|     a-1
   8|   else 

To solve this (with if) we need to change the Nat to Number. (Btw. 3 and 1 are not Nat, the syntax sugar for Nat is to add an n after the number, e.g. 3n)

Now we get the following error:

[ERROR]
Attempted to use if on a non-numeric value.
- When checking if Equal(Number, a, 0) then b else if Equal(?_test/line5_1, b, 3) then a - 1 else laver(laver(a, b + 1), a - 1)
- With context:
- a : Number
- b : Number
- On line 9, col 27, file test.fm:
   5|     b 
   6|   else if b == 3 then 
   7|     a-1
   8|   else 
   9|     laver(laver(a,b+1),a-1)
  10| 
  11| main : Number
  12|   laver(3,1)

The problem here is that == is a syntax sugar for equal (see for example here: https://github.com/moonad/Formality/blob/master/DOCUMENTATION.md#example-proving-equalities)

But if you want to use if you need 3 =, since if uses Number to compare values. (see documentation)

The final program (which typechecks) looks like so:

import Base#

laver(a: Number, b: Number) : Number
  if a === 0 then 
    b 
  else if b === 3 then 
    a-1
  else 
    laver(laver(a,b+1),a-1)

main : Number
  laver(3,1)

and evaluating it with -d results in 2.

tl;dr: you should run the typechecker -t first, to check if the term is ok. to be fair: running any execution command should do this. :)

disclaimer: I'm not associated with the project, but i hope this helps.

[tromp]

Thanks for the fixes. I tried an 8x8 table with

`import Base#

mx Base: Number 7

laver(a: Number, b: Number) : Number if a === 0 then b else if b === mx then a-1 else laver(laver(a,b+1),a-1)

main : Number laver(mx,1) `

but it took forever to run, so I just killed it after 45 mins. Am I right in concluding that the benefits of optimal evaluation do not include automatic memoization? There's at most 8*8 different invocations of laver(a,b) which should be exhausted in no time with caching of previous results.

Btw, the typechecker runs out of resources on the following variation:

`import Base#

mx : Number 3

iterate(n: Number, f: Number -> Numner, x : Number) : Number if n === 0 then x else iterate(n-1, f, f(x))

laver(a: Number, b: Number) : Number if a === 0 then b else let f = x -> laver(x, a-1) in iterate(mx*b, f, 0)

main : Number laver(0,mx) `

[emturner]

been playing around with this today - I found the following:

import Base#

mx : Number
    7

laverp(p: Pair(Number, Number)) : Pair(Number, Number)
    case p | pair =>
        if p.fst === 0 then
            pair(__ p.snd, 0)
        else if p.snd === mx then
            pair(__ p.fst - 1, 0)
        else
            let inner = laverp(pair(__ p.fst, p.snd + 1))
            case inner | pair =>
                laverp(pair(__ inner.fst, p.fst - 1))

main : Number
    let result = laverp(pair(__ mx 1))
    case result | pair => result.fst

is this correct? not sure if I've made a mistake

fm -o laver/main gives (after less than a second):

2
{"loop":146086,"rwts":73042,"mlen":75519}

[tromp]

is this correct?

The answer should be 3, since laver(0,x)=x Anyway, I don't recognize my program in there:( Not sure what the pairs are doing. And I don't understand this syntax with , eg in pair( mx 1)

[emturner]

okay, weird... - do you have a table of all the expected outputs? tried looking up the laver tables but the 4x4 is completely different to your formula.

all I did was wrap a, b => pair(Number; Number; a, b) - and then just pass that around instead. I got the same answers as you for the 4x4, so curious as to why the 8x8 is different.

pair(__ x, y) just elides the types of x & y :)

(I'm just playing around with formality at the moment, so sorry if I get anything wrong!)

[tromp]

See section 3.4 on page 7 of https://arxiv.org/pdf/1810.00548.pdf I compute the tables in this "Backwards notation" that maps the numbers 1-8 to 7-0. the laver function takes a pair of arguments, but produces only one value, so it's strange to see your function result being a pair as well. I guess you're not using the second part (always setting it to 0). This is a rather painful way to satisfy the type checker:-(

[LoPoHa]

It may be a "problem" with interaction combinator runtime.

From the documentation:

It evaluates your term using interaction combinators, making it suitable for innovative optimizations such as runtime fusion, as explained on this post, as well as not needing a garbage collector, being highly parallelizable, and having great computational characteristics in general. Elementary terms are those that only use lambda-bound variables more than once in a controlled manner. The type-checker will inform you if that's the case by appending a ℰ to its type. Right now, it might not always be able to tell; the elementarity checker is still ongoing work.

And a issue where running a (wrong term) with interaction nets resulting in a different value: https://github.com/moonad/Formality/issues/25

not sure about the following part: atm there is no box syntax/interference but it should come back sometime if i remember correctly.

I don't have time into locking into it right now, but working with Nat and cloning them manually should make it runable correctly on interaction nets.

not tested clone, but should give an idea:

clone(n : Nat) : Pair(Nat, Nat)
  case n
  | zero => pair(__ zero, zero)
  | succ => let p = clone(n.pred)
                 pair(__ succ(p.fst), succ(p.snd))

[emturner]

it's not so much about satisfying the type checker - it works fine with just number! It's more that (for whatever reason) it happens to just run quicker when taking in and returning a pair??

both -d & -o return 2 for (7, 1), which looking at the table seems right? just quickly tried a few more arguments - think they all match as well

the reason I was playing around with returning a pair, is that I want to try and implement memoization via a fixed point combinator. having laverp(pair) -> pair is just less overhead to think about!

[tromp]

Yes, 2 is correct for laver(7,1) I wrote "The answer should be 3, since laver(0,x)=x" because I thought you were translating my previously posted program that ended with laver(0,mx)". Sorry for the confusion.

I didn't think memoization cared about the results being of the same type as the arguments.

Btw, to what extent does the type checker help the efficiency of the interaction net reduction?

[LoPoHa]

oh, sry. i thought that -d and -o had different results.

your implementation and @tromp ones seems to be the same.

edit: ok, it seems it is correct according to the answer that came in simultaneously

[emturner]

oh sorry! should've realised :)

i completely agree that it shouldn't be necessary for memoization - really it was an accident that happens to work

@tromp it would be nice if we worked out why yours runs so slowly, when it seems much simpler!

EDIT:

ok, so the following also works :)

laverc(a: Number, b: Number) : Number
    case number_equal(a, 0) as x 
    | true => b
    | false => case number_equal(b, mx) as y
        | true => a - 1
        | false => laverc(laverc(a, b+1), a-1) 

running with mx = 7, laverc(mx, 1) gives: 2 {"loop":178452,"rwts":89225,"mlen":95931} which is still 16k more rewrites than the pair version, but a massive improvement!

there must be something going on in the if-then-else expression implementation?

[johnchandlerburnham]

Hi all, have played around with a few things:

-- Laver.fm
import Base#

mx : Number
  7

laver_when(a: Number, b: Number) : Number
  when
  | a === 0  => b
  | b === mx => a - 1
  else laver_when(laver_when(a,b + 1),a - 1)

iterate(n: Number, f: Number -> Number, x : Number) : Number
  if n === 0 then x
  else iterate(n - 1, f, f(x))

laver_iter(a: Number, b: Number) : Number
  if a === 0 then b
  else
    let f = (x) => laver_iter(x, a-1);
    iterate(mx * b, f, 0)

laver_case(a: Number, b: Number) : Number
  case number_equal(a, 0) as x
  | true => b
  | false => case number_equal(b, mx) as y
    | true => a - 1
    | false => laver_case(laver_case(a, b + 1), a - 1)

laver_pair(p: Pair(Number, Number)) : Pair(Number, Number)
  case p | pair => 
    when
    | p.fst === 0  => pair(__ p.snd, 0)
    | p.snd === mx => pair(__ p.fst - 1, 0)
    else
      let inner = laver_pair(pair(__ p.fst, p.snd + 1));
      case inner | pair => laver_pair(pair(__ inner.fst, p.fst - 1))

-- Λ ➜ fm -o Laver/main_pair
-- 2
-- {"loop":146086,"rwts":73042,"mlen":75519}
main_pair : Number
  let res = laver_pair(pair(__ mx,1))
  case res | pair => res.fst

-- Λ ➜ fm -o Laver/main_when1
-- 7
-- {"loop":42,"rwts":20,"mlen":36}
main_when0 : Number
  laver_when(0,mx)

-- Λ ➜ fm -o Laver/main_when1
-- (node:4521) UnhandledPromiseRejectionWarning: RangeError: Maximum call stack size exceeded
main_when1 : Number
  laver_when(mx,1)

-- Λ ➜ fm -o Laver/main_case0
-- 7
-- {"loop":88,"rwts":43,"mlen":55}
main_case0 : Number
  laver_case(0,mx)

-- Λ ➜ fm -o Laver/main_case1
-- 2
-- {"loop":178452,"rwts":89225,"mlen":95931}
main_case1 : Number
  laver_case(mx,1)

-- Λ ➜ fm -o Laver/main_iter0
-- 7
-- {"loop":34,"rwts":16,"mlen":40}
main_iter0 : Number
  laver_iter(0,mx)

-- Λ ➜ fm -o Laver/main_iter1
-- (node:5342) UnhandledPromiseRejectionWarning: RangeError: Maximum call stack size exceeded
main_iter1 : Number
  laver_iter(mx,1)

You can typecheck all the definitions this file at once with fm -t Laver/@

@tromp The iterate construction does pass typechecking, the issue in your code was a few syntax errors that the typechecker didn't give good errors on. Better error reporting is a big priority for us, right now it's very sub-optimal.

@LoPoHa Afaik, Number should automatically copy for the interaction-nets runtime. Not sure if that's implemented though. From my testing, it looks like the autocopying works on case but not on when.

If I add with b to laver_case to preserve affinity across branches,

laver_case(a: Number, b: Number) : Number
  case number_equal(a, 0) as x
  with b : Number
  | true => b
  | false => case number_equal(b, mx) as y
    with b : Number
    | true => a - 1
    | false => laver_case(laver_case(a, b + 1), a - 1)

it still works, but the number of rewrites goes up from 89225 to 102479, which makes sense because with desugars to a new lambda abstraction on the branches.

We used to have a cpy syntax to do copying explicitly, but it shouldn't be necessary now. So I think this is just a bug. @MaiaVictor, what do you think?

@emturner I suspect that your Pair construction works because it avoids this bug by wrapping the two Number arguments to laver_pair (bascially uncurrying them) in something that the i-net compiler knows how to optimize (datatypes, rather than Number). I expect that when we fix this bug, laver_when will be even faster than laver_pair, since it won't have the datatype overhead.

[VictorTaelin]

I don't have much time to check this right now, but this line: laver_case(laver_case(a, b + 1), a - 1) is calling a recursive function inside its own argument, so I suspect this program is not elementary. Our interaction net (-o) backend isn't compatible with non-elementary programs, so running it is unsafe and it can or can not work. I'm not sure why it works with pairs and not when, this deserves some attention. But regardless, if the debug mode is too slow, -o isn't an option, and you just want to run it, you can simply use IO, which uses native JavaScript closures:

main : IO(Unit)
  do {
    let n = laver_when(7, 1)
    print(number_to_string(10, n))
  }

Run this with fm -r file/main. It won't have soundness issues and should be fast (I wrote an article about it). @johnchandlerburnham perhaps we should add this to the documentation?

I don't know much about this algorithm to improve it, but chances are it can be expressed in a way that is compatible with inets. I can have a look in a future.

Edit: oh, well. The JS backend won't work for laver_when(10,1). But that has nothing to do with Formality, it actually blows up the JS stack, even if we write it by hand:

function laver_when(a, b) {
  if (a === 0) {
    return b;
  } else if (b === 7) {
    return a - 1;
  } else {
    return laver_when(laver_when(a, b + 1), a - 1);
  }
};

console.log(laver_when(10, 1)); // stack overflows

I guess that is a good excuse to start working in Haskell or at least Scheme backend?

[VictorTaelin]

Formality was refactored, is this issue still relevant?