From ed7cb7df9d52f88e94ecf5996c43fb534a2624c9 Mon Sep 17 00:00:00 2001 From: Stewart Stewart Date: Tue, 11 Aug 2015 15:38:20 -0700 Subject: Added a cheat sheet to README.md --- README.md | 57 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) create mode 100644 README.md diff --git a/README.md b/README.md new file mode 100644 index 0000000..88e9705 --- /dev/null +++ b/README.md @@ -0,0 +1,57 @@ +## Cheat Sheet + +#### Syntax + ::= | + ::= | + ::= () + +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 +S(KS)Kpq +KSp(Kp)q +S(Kp)q +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. -- cgit v1.2.3