Cheat Sheet

Syntax

<term>        ::= <atom> | <combination>
<atom>        ::= <constant> | <variable>
<combination> ::= (<term><term>)

eg. constants: I, K, S, etc.

eg. variables: x, y, z

eg. combination: Ix, yz, ((yz)(Ix))

Given distinct terms p, q, r, s, the following properties hold:

• non-commutative: pq != qp
• non-associative: p(qr) != (pq)r
• left-associative: pqrs == (((pq)r)s)

Typically, we omit parens where possible: ((yz)(Ix)) as above is simply yz(Ix).

Check out the parse tree for this term: S(BBS)(KK)SI

Reduction Rules

The combinators have the follwing reduction properties. Given arbitrary terms, p, q, r, s:

Ip     -> p
Kpq    -> p
Bpqr   -> p(qr)
Cpqr   -> prq
Spqr   -> pr(qr)
Wpq    -> pqq
B'pqrs -> pq(rs)
C'pqrs -> p(qs)r
S'pqrs -> p(qs)(rs)

If a term begins with one of these patterns the head can be reduced to form a new term. e.g:

Bpqrstuv -> p(qr)stuv

The term S(KS)Kpqr reduces as follows:

S(KS)Kpqr
KSp(Kp)qr
S(Kp)qr
S(Kp)qr
Kpr(qr)
p(qr)

Running:

As in a typical project: sbt test and sbt compile will test and compile your code. With utest, you can run test-only -- Tests --trace=false in sbt to supress the stack trace.

More

Check out this page to learn more about combinatory logic and bracket abstraction algorithms.