| Name | Summary | Author | Created | Modified |
|---|---|---|---|---|
| working example | ilya.klyuchnikov | 23rd February 2011 15:47 | 23rd February 2011 15:47 | |
| Ackermann fo vs ho | sergei.romanenko | 19th January 2011 09:37 | 19th January 2011 09:50 | |
| multiplication of church numbers via foldn | ilya.klyuchnikov | 16th January 2011 09:35 | 16th January 2011 09:35 | |
| church numbers via foldn | ilya.klyuchnikov | 16th January 2011 09:32 | 16th January 2011 09:32 | |
| CEK machine | Semantics: big-step vs. small-step | sergei.romanenko | 16th June 2010 14:07 | 16th June 2010 14:09 |
| lemma1 | ilya.klyuchnikov | 12th June 2010 10:09 | 12th June 2010 10:09 | |
| abstract machines | ilya.klyuchnikov | 8th June 2010 19:33 | 8th June 2010 19:33 | |
| for paper | ilya.klyuchnikov | 22nd February 2010 22:17 | 22nd February 2010 22:17 | |
| t3 | ilya.klyuchnikov | 24th August 2009 17:26 | 24th August 2009 17:26 | |
| t2 | ilya.klyuchnikov | 24th August 2009 17:15 | 24th August 2009 17:15 | |
| t1 | ilya.klyuchnikov | 24th August 2009 17:14 | 24th August 2009 17:14 | |
| addition of Church numbers 2 | need postproc | ilya.klyuchnikov | 24th June 2009 08:42 | 24th June 2009 08:42 |
| lemma | for accumulat. param. destruction | ilya.klyuchnikov | 18th June 2009 08:14 | 18th June 2009 08:14 |
| even (doubleAcc x (S (S Z))) | ilya.klyuchnikov | 16th June 2009 12:26 | 16th June 2009 12:26 | |
| xxx1 | aaa | ilya.klyuchnikov | 3rd June 2009 15:26 | 15th June 2009 05:11 |
| xxx | xxx | ilya.klyuchnikov | 3rd June 2009 15:25 | 3rd June 2009 15:25 |
| even doubleAcc | accumulating parameter exploited | ilya.klyuchnikov | 3rd June 2009 14:03 | 3rd June 2009 14:03 |
| Unrolling repeat (failed) | repeat [T,F] = T : repeat[F,T] | sergei.romanenko | 5th May 2009 15:05 | 5th May 2009 15:11 |
| multiplication of Church numbers | unchurch(churchMult (church x) (church y)) = (mult x y) | ilya.klyuchnikov | 2nd May 2009 14:36 | 2nd May 2009 14:36 |
| predecessor function for Church numbers | unchurch(churchPred (church x)) = idNat (pred x) | ilya.klyuchnikov | 26th April 2009 12:09 | 28th April 2009 18:32 |
| addition of Church numbers | unchurch(churchAdd (church x) (church y)) = idNat (add x y) | ilya.klyuchnikov | 26th April 2009 11:14 | 26th April 2009 11:14 |
| church followed by unchurch | unchurch(church m) = idNat m | sergei.romanenko | 25th April 2009 13:21 | 25th April 2009 13:22 |
| Odd Even 3 | odd n = even (S n) | ilya.klyuchnikov | 23rd April 2009 21:39 | 23rd April 2009 21:39 |
| Odd Even 2 | or (even n) (odd n) = or (odd (S n)) (even (S n)) | ilya.klyuchnikov | 23rd April 2009 21:06 | 23rd April 2009 21:06 |
| Odd Even | or (even n) (odd n) = or (even (S (S n))) (odd (S (S n))) | ilya.klyuchnikov | 23rd April 2009 21:01 | 23rd April 2009 21:01 |
| Hughes lists 2 | (compose abs rep) xs = idList xs | ilya.klyuchnikov | 6th April 2009 09:34 | 6th April 2009 09:34 |
| Hughes lists | rep (append xs ys) zs = (compose (rep xs) (rep ys)) zs | ilya.klyuchnikov | 6th April 2009 09:26 | 6th April 2009 09:28 |
| Free theorem 4 | filter p (map f xs) = map f (filter (compose p f) xs) | ilya.klyuchnikov | 3rd April 2009 13:15 | 3rd April 2009 13:15 |
| Free theorem 3 | (compose (map f) join) xs = (compose join (map (map f))) xs | ilya.klyuchnikov | 3rd April 2009 12:30 | 3rd April 2009 12:30 |
| Free theorem 2 | map [f1, f2] (zip [l1, l2]) = zip [map f1, map f2] [l1, l2] | ilya.klyuchnikov | 3rd April 2009 12:23 | 3rd April 2009 12:27 |
| Free theorem 1 | map f (append xs ys) = append (map f xs) (map f ys) | ilya.klyuchnikov | 3rd April 2009 06:42 | 3rd April 2009 12:22 |
| Lemma | lemma | ilya.klyuchnikov | 3rd April 2009 09:29 | 3rd April 2009 09:29 |
| Map composition | map (compose f g) xs = (compose (map f)(map g)) xs | ilya.klyuchnikov | 3rd April 2009 09:18 | 3rd April 2009 09:18 |
| Associativity of list concatenation | app x (app y z) = app (app x y) z | ilya.klyuchnikov | 3rd April 2009 06:39 | 3rd April 2009 07:27 |
| Iterator property | iterate f (f x) = map f (iterate f x) | ilya.klyuchnikov | 3rd April 2009 06:44 | 3rd April 2009 07:26 |
| Equivalence of functions | compose (map f) unit = compose unit f | ilya.klyuchnikov | 3rd April 2009 06:50 | 3rd April 2009 07:26 |
| Non-commutativity of lazy addition | add (S x) y ≠ add x (S y) | ilya.klyuchnikov | 3rd April 2009 07:09 | 3rd April 2009 07:14 |
| Associativity of lazy addition | add x (add y z) = add (add x y) z | ilya.klyuchnikov | 3rd April 2009 07:14 | 3rd April 2009 07:14 |