search

HerrmannM / eole

Éole, a Lévy-optimal lambda calculus evaluator without oracle
GNU General Public License v3.0
110 stars 4 forks source link

Incorrect result on some inputs #3

Open Ekdohibs opened 4 years ago

Ekdohibs commented 4 years ago

With the following input, Eole produces an incorrect result:

(a->((b->((c->c) ((d->(e->(f->((((e d) f) (a (e e))) ((f (g->b)) (h->(i->(h (b (j->(b j))))))))))) b))) (k->((l->(((a (a k)) ((a l) (k a))) (m->((k (n->(o->m))) k)))) ((p->(q->(k a))) (r->(s->((t->r) (u->(a (v->r))))))))))).

The produced result is:

(a3->(e10->(f11->((((e10 (k8->(((a3 (a3 k8)) ((a3 (q57->(k8 a3))) (k8 a3))) (m48->((k8 (n49->(o69->m48))) k8))))) f11) (a3 (e10 e10))) ((f11 (g23->(k46->(((a3 (a3 k46)) ((a3 (q57->(k46 a3))) (k46 a3))) (m48->((k46 (n108->(o110->m48))) k46)))))) (h24->(i25->(h24 (((a3 (a3 (j111->(((a3 (a3 j111)) ((a3 (q57->(j111 a3))) (j111 a3))) (m48->((j111 (n178->(o182->m48))) j111)))))) ((a3 (q57->(((a3 (a3 a3)) ((a3 (q57->(a3 a3))) (a3 a3))) (m48->((a3 (n79->(o172->m48))) a3))))) (((a3 (a3 a3)) ((a3 (q57->(a3 a3))) (a3 a3))) (m48->((a3 (n168->(o175->m48))) a3))))) (m48->((((a3 (a3 (n75->(o170->m48)))) ((a3 (q57->(o130->m48))) (o84->m48))) (m48->m48)) (j80->(((a3 (a3 j80)) ((a3 (q57->(j80 a3))) (j80 a3))) (m48->((j80 (n160->(o171->m48))) j80)))))))))))))))

while the correct result is, according to https://crypto.stanford.edu/~blynn/lambda/:

λa e f.e(λk.a(a k)(a(λq.k a)(k a))(λm.k(λn o.m) k)) f(a(e e))(f(λg k.a(a k)(a(λq.k a)(k a))(λm.k(λn o.m) k))(λh i.h(a(a(λj.a(a j)(a(λq.j a)(j a))(λm.j(λn o.m) j)))(a(λq.a(a a)(a(λq.a a)(a a))(λm.a(λn o.m) a))(a(a a)(a(λq.a a)(a a))(λm.a(λn o.m) a)))(λm.a(a(λn o.m))(a(λq o.m)(λo.m))(λm1.m)(λj.a(a j)(a(λq.j a)(j a))(λm.j(λn o.m) j))))))

(input with the corresponding syntax:)

(\a -> ((\b -> ((\c -> c) ((\d -> (\e -> (\f -> ((((e d) f) (a (e e))) ((f (\g -> b)) (\h -> (\i -> (h (b (\j -> (b j))))))))))) b))) (\k -> ((\l -> (((a (a k)) ((a l) (k a))) (\m -> ((k (\n -> (\o -> m))) k)))) ((\p -> (\q -> (k a))) (\r -> (\s -> ((\t -> r) (\u -> (a (\v -> r)))))))))))

Note that Eole produces a (m48->m48) subterm near the end of the result, but that m48 is already bound in the same context. The correct result contains a (λm1.m) in that place, which is the correct one.

Besides, with the following input, Eole produces a result that is not even well-scoped.

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

The result produced by Eole is:

(c169->(x50->((((((x50 c169) (n172->(o154->(p39->n172)))) (p79->(c172->(d9->(e101->(f16->((f16 c169) (a179->(b184->(c87->(x134->((((((x134 c87) (n150->(o113->(p111->n150)))) (p13->(c173->(d149->(e74->(f147->((f147 c87) b184))))))) (d110->(e75->(f177->((f177 c116) b21))))) (a1146->(o125->(p22->(b1141->b1141))))) (y77->(z143->(o81->(p64->c87)))))))))))))))) (d161->(e158->(f122->((f122 c169) (a153->(b21->(c116->(x55->((((((x55 c116) (n133->(o130->(p114->n133)))) (p174->(c1131->(d43->(e86->(f71->((f71 c87) b184))))))) (d157->(e118->(f121->((f121 c116) b21))))) (a1148->(o40->(p84->(b178->b178))))) (y7->(z47->(o80->(p65->c116)))))))))))))) (a1164->(o137->(p53->(b1180->b1180))))) (y85->(z144->(o82->(p119->c169)))))))

The variables c116 and b21 are not bound at their first occurence.

HerrmannM commented 4 years ago

Thank you for that!

I'll see if this is related to #2 after I fixed it.

Ekdohibs commented 4 years ago

I think this is probably a separate problem: I get the same errors in the result, with the same test cases, in case the GC is disabled.

HerrmannM commented 4 years ago

Indeed, I narrowed down the issue to the readback with some minimum examples:

a->(b->b b) (k->a(m->k m)).

has the problem, but not

a->(b->b b) (k->(m->k m)).

Looking at the graphs (option -G), we see that in the second case, the duplication with the fans labelled 1 is completely done, whereas it is "held back" by the application in the first case. While performing the readback in the first case, the lambda is shared (correctly), not duplicated. When creating the lambda expression, the same name is (wrongly) used for each share. I'll correct that soon!

Ekdohibs commented 4 years ago

This would indeed fix the first case, but I don't see how it fixes the second error, where there is a variable that is not bound by a lambda in the readback. Also, both your examples are the same, is it intended?

HerrmannM commented 4 years ago

Copy/paste mistake, sorry about that. I edited the post. You are right, it won't fix the other cases, see my last reply on #2!