Hindley's "Introduction to combinatory logic", exercise 6 chapter 2.

184 Views Asked by At

Can somebody help me with the following exercise?

Find a combinator X such that X = S(KK)(XS). Reduction rules are usual:

IX reduces to X (identity combinator)

KXY reduces to X

SXYZ reduces to XZ(YZ)

X reduces to X

if X reduces to Y, then ZX reduces to ZY

if X reduces to Y, then XZ reduces to YZ

if X reduces to Y and Y reduces to Z, then X reduces to Z.

and equality is the equivalence relation generated by reduction and inversion reduction, that is: equality is given by the previous rules with "=" in place of "reduces to" and with the additional rule

if X = Y, then Y = X

Combinatory abstraction is defined as follows:

[x]x denotes I

[x]M denotes KM, if M does not contain x

[x]Mx denotes M, if M does not contain x

[x]UV denotes S([x]U)([x]V), if the previous two cases cannot be applied.

The abstraction operator is not part of the syntax, but one can show that ([x]M)N reduces to [N/x]M for every M.

PS: parentheses goes from right to left, namely: XYZW has to be understood as ((XY)Z)W.

1

There are 1 best solutions below

0
On BEST ANSWER

The straightforward bute-force solution would be to let $\mathbf F$ be your favorite fixpoint combinator (such as the Y combinator) and set $$ X = \mathbf F (\lambda x.S(KK)(xS)) $$ Then use standard techniques to eliminate the lambda abstractions.