1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
|
## 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: **I**_x_, _yz_, ((_yz_)(**I**_x_))
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_)(**I**_x_)) as above is simply _yz_(**I**_x_).
Check out the parse tree for this term: [S(BBS)(KK)SI](http://mshang.ca/syntree/?i=%5B*%20%5B*%20%5B*%20%5B*%20%5BS%5D%20%5B*%20%5B*%20%5BB%5D%20%5BB%5D%5D%20%5BS%5D%5D%5D%20%5B*%20%5BK%5D%20%5BK%5D%5D%5D%20%5BS%5D%5D%20%5BI%5D%5D%0A%0A)
#### 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](http://www.cantab.net/users/antoni.diller/brackets/intro.html)
to learn more about combinatory logic and bracket abstraction algorithms.
|