Play with terms in chemlambda vs dirIC, chemSKI

I record here some differences in reduction between chemlambda and dirIC, then I’ll talk very briefly about chemSKI for SKI or SK calculus.

Chemlambda vs dirIC

Chemlambda and directed Interaction Combinators (dirIC) are not equal.

Play with div from https://github.com/tromp/AIT/blob/master/numerals/div.lam

Use https://mbuliga.github.io/quinegraphs/lambda2mol.html

As chemlambda or dirIC want only one term to be inputted, we have to build it progressively, so here is the process:

with all parantheses…

1tuple = (\x.(\f.(f x)))

id = (\x.x)

F = (\m.(\f.(\t.((((m (\x.(\f.(f x)))) (\c. f (c t))) (\x.x))))))

K = (\x.(\y.x))

div = (\n.(\m.(\f.(\x.(((n (\x.(\f.(f x)))) ((\x.(\y.x)) x)) ((n (((\m.(\f.(\t.((((m (\x.(\f.(f x)))) (\c. f (c t))) (\x.x)))))) m) f)) x))))))

we prepare the term

term = (((div number1) number2) a) b

replaced div

term = ((((\n.(\m.(\f.(\x.(((n (\x.(\f.(f x)))) ((\x.(\y.x)) x)) ((n (((\m.(\f.(\t.((((m (\x.(\f.(f x)))) (\c. f (c t))) (\x.x)))))) m) f)) x)))))) number1) number2) a) b

for

number1 = (\f.(\x.(f (f (f (f (f (f x)))))))) (ie Church 6)

number2 = (\f.(\x.(f (f (f x))))) (ie Church 3)

we get

term = ((((\n.(\m.(\f.(\x.(((n (\x.(\f.(f x)))) ((\x.(\y.x)) x)) ((n (((\m.(\f.(\t.((((m (\x.(\f.(f x)))) (\c. f (c t))) (\x.x)))))) m) f)) x)))))) (\f.(\x.(f (f (f (f (f (f x))))))))) (\f.(\x.(f (f (f x)))))) a) b

which works in chemlambda but not in dirIC.

For the term

term1 = (div number1) number2

we replace div, number1 and number2

term1 = ((\n.(\m.(\f.(\x.(((n (\x.(\f.(f x)))) ((\x.(\y.x)) x)) ((n (((\m.(\f.(\t.((((m (\x.(\f.(f x)))) (\c. f (c t))) (\x.x)))))) m) f)) x)))))) (\f.(\x.(f (f (f (f (f (f x))))))))) (\f.(\x.(f (f (f x)))))

works in chemlambda, not in dirIC.

For

number1 = (\f.(\x.(f (f (f (f (f (f (f x))))))))) (ie Church 7)

number2 = (\f.(\x.(f (f (f x))))) (ie Church 3)

we get

term1 = ((\n.(\m.(\f.(\x.(((n (\x.(\f.(f x)))) ((\x.(\y.x)) x)) ((n (((\m.(\f.(\t.((((m (\x.(\f.(f x)))) (\c. f (c t))) (\x.x)))))) m) f)) x)))))) (\f.(\x.(f (f (f (f (f (f (f x)))))))))) (\f.(\x.(f (f (f x)))))

works in chemlambda 7 div 3 = 2

_________________

ChemSKI for SKI or SK calculus

I does not matter which one is used, in the sense that if you don’t input any I combinator, then you don’t get any. There is a lot of waste, but now this is managed by waste rewrites.

Maybe relevant in the larger discussion chemSKI not Kind.

Examples:

Use https://mbuliga.github.io/chemski/chemski-with-tokens.html#PlayPlace

Down the page tromp.github.io is a minimal SK version of the Y combinator.

S S K (S (K (S S (S(S S K)))) K)

Applied to I should give a quine

((((S S) K) ((S (K ((S S) (S ((S S) K))))) K)) I)

Applied to S K K instead should work as well

((((S S) K) ((S (K ((S S) (S ((S S) K))))) K)) (S K K))

It does. ChemSKI rules rule!

Leave a comment