Multiple crashes

[Ekdohibs]

With some random terminating inputs, I get a lot of different errors:

• thread 'main' panicked at 'baam', src/eole/reduce.rs:215:53 with input:

(((a->((b->(c->(((d->(e->a)) (c c)) (f->(g->(h->(i->(j->(k->(l->((i c) (m->m)))))))))))) (n->(o->(p->(q->((r->o) (s->(t->(u->((v->(w->(x->(y->(z->y))))) (((((n s) (a1->(u (((p s) (b1->n)) t)))) s) (c1->((o t) (d1->q)))) (o o))))))))))))) (e1->(((f1->(f1 (e1 f1))) (g1->(((g1 ((h1->e1) (g1 e1))) ((i1->g1) (j1->e1))) (k1->e1)))) (l1->(((m1->m1) l1) e1))))) (n1->(o1->((p1->((q1->(r1->n1)) (((p1 p1) (s1->((t1->p1) o1))) (u1->(v1->n1))))) ((((w1->(x1->n1)) (y1->n1)) (z1->o1)) ((a2->((b2->(c2->a2)) n1)) o1)))))).

• thread 'main' panicked at 'baam', src/eole/reduce.rs:165:21 with input:

((a->((a a) (((a (b->(b a))) (a a)) (c->(d->(e->((f->(d d)) (g->(d d))))))))) (h->(((i->(((j->(k->h)) (l->i)) ((m->((m h) i)) (n->(h (o->i)))))) (((p->(p h)) (h (q->(r->(s->s))))) (h (t->h)))) (u->(((v->(w->(x->(((y->(z->(a1->(((((b1->y) x) ((c1->(d1->z)) (e1->z))) (v x)) (f1->(g1->(h1->(i1->v)))))))) u) (u ((w h) (w (j1->h)))))))) ((k1->(((l1->(m1->((n1->(o1->o1)) u))) k1) (p1->(q1->(k1 p1))))) (r1->(u (r1 u))))) (s1->(t1->(u1->((v1->((w1->(v1 w1)) (x1->u))) (h (y1->h))))))))))).

• thread 'main' panicked at 'Reaching an Abstraction by the body', src/eole/reduce.rs:202:41 with input:

(((a->(a ((b->(a b)) (a a)))) (((c->(c ((c c) ((d->(e->(f->c))) c)))) (g->(h->(i->((i h) (j->(k->(((l->(m->(n->((o->(p->m)) (h n))))) (q->i)) (((r->g) j) i))))))))) (s->s))) ((t->((u->(v->((w->(v u)) ((x->((y->(u (z->u))) v)) (u (v t)))))) (a1->(b1->(c1->(d1->((c1 a1) (e1->(f1->(g1->a1)))))))))) (h1->(h1 (((h1 (((i1->(i1 (j1->i1))) h1) (k1->(l1->(m1->(h1 m1)))))) (n1->((o1->(p1->(q1->(r1->(s1->(s1 h1)))))) n1))) ((t1->h1) ((h1 (u1->((v1->((w1->(v1 u1)) (v1 h1))) ((x1->x1) h1)))) (h1 (h1 h1))))))))).

• thread 'main' panicked at 'Reaching a fan out by an aux port', src/eole/reduce.rs:201:71 with input:

(((a->a) (b->((c->c) ((((b b) (d->(e->((f->(d e)) (g->d))))) (((b ((h->b) b)) (i->(j->(k->(l->(l (j (m->(n->((o->(o (i i))) (p->l))))))))))) b)) ((b (q->(r->q))) (s->b)))))) (t->((u->(((v->((w->u) (v v))) (x->(y->((z->((a1->(((z (b1->a1)) (c1->(d1->x))) (u z))) ((e1->(f1->(g1->(h1->z)))) x))) (i1->x))))) ((j1->(k1->(((t u) j1) u))) (l1->(t ((m1->u) (l1 (n1->(u u))))))))) (o1->((p1->((p1 (q1->(r1->(s1->p1)))) ((t1->t1) ((p1 p1) (o1 t))))) (u1->(u1 (((v1->t) (w1->(u1 w1))) (o1 t))))))))).

• thread 'main' panicked at 'baam', src/eole/reduce.rs:258:9 with input:

(a->(((((a a) a) (b->((c->(d->(c ((e->(f->d)) (a c))))) (a (g->(g (h->(b (a (g a)))))))))) ((i->((i (j->(k->(l->(m->(n->(o->i))))))) (p->(q->(r->(s->(t->p))))))) (((u->(v->(w->((x->(y->(u (z->(a1->(a1 (w z))))))) ((b1->(u a)) (a a)))))) (c1->((d1->((e1->(f1->(f1 e1))) (c1 (d1 c1)))) ((g1->((a ((c1 c1) c1)) (h1->(a (c1 a))))) (i1->(a c1)))))) ((j1->j1) ((k1->(a (a a))) (l1->l1)))))) ((m1->(n1->(o1->(p1->((q1->(r1->((s1->(t1->((u1->o1) (v1->(w1->m1))))) (x1->r1)))) ((y1->o1) n1)))))) (z1->z1)))).

• thread 'main' panicked at 'Cannot pair fan out (110, 6) [(Vertex(9, Port(0)), CstrK(Abs("d", false))), (Vertex(15, Port(0)), CstrK(Abs("g", true)))]', src/eole/reduce.rs:276:25 (there are other related crashes with a similar error message with other inputs) with input:

(((a->(b->((c->(d->((c c) c))) ((e->(f->(g->(f ((g e) (h->(i->((j->(k->(g e))) g)))))))) (l->((m->(m ((n->n) ((o->a) (p->(m p)))))) (l (l a)))))))) ((q->(r->r)) ((s->(t->((u->(v->(s t))) (s (t (w->w)))))) ((x->x) (y->((z->z) y)))))) (a1->(((b1->(c1->((c1 a1) ((d1->(e1->((f1->(g1->g1)) ((e1 a1) b1)))) ((b1 b1) ((h1->b1) b1)))))) (i1->((j1->i1) ((a1 (a1 i1)) ((i1 i1) ((k1->k1) a1)))))) ((((a1 (l1->a1)) (a1 a1)) (a1 a1)) ((a1 ((m1->m1) ((n1->a1) a1))) (o1->(p1->((a1 a1) (o1 (p1 o1)))))))))).

Edit: alpha-renamed the terms to ones with more human-friendly variable names.

[HerrmannM]

Thank you so much for taking the time to test, this is extremely valuable!

I definitely have to put good messages in my assert (but at least I had them). I did not test things randomly, and so I guess I always write terms that reduce in a nice "tree structure" way. What happens here is that the "history" (a stack of nodes) get "corrupted". Some nodes are eliminated (either by the GC or some interactions) from the graph, but not the stack. When eliminated, they are nullified, and can be reused. Because the stack is not storing the node but its index, and that can be reused... well, anything goes.

I'm going to investigate that and fix asap.

What are you using to test randomly?

[HerrmannM]

Disabling the GC and snot reusing any nodes solve all the issue above. So we indeed have a corruption of the history triggering the assert crashes.

[Ekdohibs]

Without the GC (-m=none), I still get some "Cannot pair fan out" crashes, for instance with the following input:

((a->((b->((((c->((a (d->(e->e))) (c (c c)))) (f->b)) (a a)) ((g->b) ((h->(((((a a) (i->(b a))) (j->(k->(l->(m->(((m (b h)) a) b)))))) (h (n->((((o->(p->a)) a) ((q->a) n)) a)))) (r->((((s->(t->r)) (u->(v->(w->r)))) ((x->x) a)) ((b (a (r r))) a))))) (((y->(a (z->(y y)))) (a (a1->a))) (b1->a)))))) (c1->((a (d1->a)) (e1->((f1->((g1->(h1->(i1->((f1 (e1 i1)) (j1->(k1->(k1 a))))))) ((l1->e1) f1))) (m1->((e1 m1) (n1->n1))))))))) (o1->((o1 o1) (p1->(q1->(p1 ((o1 p1) (r1->p1)))))))).

All other crashes seem indeed fixed.

[Ekdohibs]

Also, I am using https://gist.github.com/Ekdohibs/500919f8657e21da0b4acc69531c83b2 (compile with ocamlopt -o eole_tester eole_tester.ml, create a directory named eole_test, and run the executable) to test: it generates random lambda-terms, reduces them (with some maximum number of reduction steps), and prints the term and its normal form inside a file if it normalizes.

[HerrmannM]

Sorry I was not precise enough. There are two ways nodes are collected and reused:

1. With the GC, and you disabled it with -m=none
2. Interacting nodes are always collected and reused. To avoid that, the code must be changed manually. See the new_node function in the file net.rs file line 382 https://github.com/HerrmannM/eole/blob/master/src/eole/net.rs#L382. Activate the line 386-387 and comment the rest of the function (lines 389-400). That will prevent any node to be reused.

I'll create a flag for the 2nd case.

Thank you for your code! Are you allowing me to put it in the repo? If so, do you want to be credited by your github user name or real name (or something else)?

To give you a bit of background, I mostly worked with the reduction in weak head normal form (flag -s lazy), comparing with BOHM. In that case, the reduction function is simpler, and no "history" is required. The reduction in normal form was "hacked" (as you can see with the "baam" messages) on top of it. Keeping the history in sync will require a bit more work, and probably will have a small impact on the performances of the normal reduction.

[Ekdohibs]

Even with the change to new_node, I get the "cannot pair fan out" crash with the above testcase. I still find it surprising that it is possible to avoid the bookkeeping usually associated with croissants and brackets... However, it seems that it still is exponential on fan operations, which is a bit surprising when you say that it is asymptotically faster than other evaluators :). Concerning my code, you can put it in the repo if you want: if you do so, I'd like to be credited as "Nathanaël Courant" in the file (with the diacritics, please).

[HerrmannM]

Yeah "conventional evaluators", but I'll tone down that a bit. Anyway, see #1, we have a counter example so we now know that it does not work! That's a relieve, but I'm still surprised that it could handle some form of recursion... I'll see how long I can keep working on that project, and if I can find an interesting typeable fragment. Thanks for your time and help!