Embedded read-back produces name clashes

[codedot]

trafficstars

The current implementation of the embedded read-back mechanism produces name clashes for some terms on all three optimal algorithms: abstract, optimal, and standard. The shortest closed λ-term that demonstrates this behavior is a triple η-expansion of the self-application combinator, namely

λx.ω (λy.x (λz.y z)), where ω = λx.x x.

However, the term does not produce a name clash when using the non-optimal algorithm closed as shown below:

$ npm i -g @alexo/lambda
+ @alexo/[email protected]
$ lambda 'x: (w: w w) (y: x (z: y z))'
v1: v1 (v2: v1 (v2: v2 v2))
$ lambda 'x: (w: w w) (y: x (z: y z))' -a optimal
v1: v1 (v2: v1 (v2: v2 v2))
$ lambda 'x: (w: w w) (y: x (z: y z))' -a standard
v1: v1 (v2: v1 (v2: v2 v2))
$ lambda 'x: (w: w w) (y: x (z: y z))' -a closed
v1: v1 v1