lambda calculus hw2

Fun Programming HW2.markdown

###predefines for Peter Sestoft's Lambda Calculus reducer http://www.itu.dk/~sestoft/lamreduce/lamframes.html

Nil =   (\c.\n.n);
isnil = (\l.l (\h.\t.fal) tru);
Cons =  (\h.\t.\c.\n.c h (t c n));
head = \l.l (\h.\t.h) l;
tail = \l.fst (l (\x.\p.pair
                     (snd p)
                     (Cons x (snd p)))
              (pair Nil Nil));


minus = \n.\m.m pred n;
equal = \n.\m.(iszero (add (minus m n) (minus n m)));
LE = \n.\m.iszero (minus n m);

map = (\f.\l.l (\x.Cons (f x)) Nil) ;
fix = Y;
Append = fix (\F.\l.\m.(isnil l) m (Cons (head l) (F (tail l) m)));
reverse = fix (\F.\l. (isnil l) Nil (Append (F (tail l)) (Cons (head l ) Nil)))
Flatten = fix (\F.\l.(isnil l) Nil (Append (head l) (F (tail l))));
flatMap = \f.\l. Flatten (map f l);
foldRight = fix (\F.\f.\z.\l. (isnil l) z (f (head l) (F f (tail l))));

Problem 1

code

subsets = \l.Cons Nil
                  (fix (\F.\l.(isnil l)
                                 Nil
                                 (Cons (Cons (head l) Nil)
                                       (Append (F (tail l))
                                               (map (Cons (head l))
                                                    (F (tail l)))))) l);
                           

example

subsets (Cons x(Cons y (Cons z)))
-> \c.\n.c (\c.\n.n) (c (\c.\n.c (x) (n)) (c (\c.\n.c (y) (n)) (c (\c.\n.c (z) (n)) (c (\c.\n.c (y) (c (z) (n))) (c (\c.\n.c (x) (c (y) (n))) (c (\c.\n.c (x) (c (z) (n))) (c (\c.\n.c (x) (c (y) (c (z) (n)))) (n))))))))
-> [[], [x], [y], [z], [y,z], [x, y], [x, z], [x, y, z]]

explain

subsets [1 2 3]
-> [] :: ([1] :: (subsets 2 3) :: map (Cons 1) (subsets 2 3))
                    |              | 
                    v              +-----------------------------------------------+                 
                   [2] :: (subsets 3) :: map (Cons 2) (subsets 3) --+              | 
                            |             |                         |              | 
                            v             v                         |              | 
                           [3]          [2 3]                       v              | 
                                                         [[2] [3] [2 3]]           v 
                                                                             [[1 2] [1 2 3] [1 3]]
-> [[] [1] [2] [3] [2 3] [1 2] [1 2 3] [1 3]]

Problem 2

(a)

code

remove = fix (\F.\x.\l.
                   (isnil l)
                      nil
                      ((equal (head l) x)
                             (F x (tail l))
                             (Cons (head l) (F x (tail l)))));

example

remove one (Cons one (Cons two (Cons one (Cons three Nil))))

(b)

code

insertAny = fix (\F.\n.\l.
                    (isnil l)
                           (Cons (Cons n Nil) Nil)
                           (Cons (Cons n l)
                                 (map (Cons (head l))
                                      (F n (tail l)))));
permutation = \l. foldRight  (\n.\m.flatMap (insertAny n) m) (Cons Nil Nil) l

example

permutation [1 2 3]
-> foldRight (\n.\m.flatMap (insertAny n) m) [[]] [1 2 3]
-> [[1 2 3] [2 1 3] [2 3 1] [1 3 2] [3 1 2] [3 2 1]]

explain

foldRight 從最末項和 initial value 開始處理。每個階段皆將一個項目插入到後面 list 的每個位置。

3:                                            -> flatMap (insertAny 3) [[]]
                                              -> [[3]]
                                                   v
2:                      -> flatMap (insertAny 2) [[3]]
                        -> [[2 3] [3 2]]
                                 v
1:-> flatMap (insertAny 1) [[2 3] [3 2]]
  -> [[1 2 3] [2 1 3] [2 3 1] [1 3 2] [3 1 2] [3 2 1]]

不使用 filter ，所以重複的項目也能正常處理

permutation [1 1 2]
-> [[1 1 2] [1 2 1] [1 1 2] [1 2 1] [2 1 1] [2 1 1]]

Problem 3

code

hasSubsequence = fix (\F.\l.\s.
                          (isnil s)
                              tru
                              (isnil l)
                                  fal
                                  ((equal (head l) (heal s))
                                         (F (tail l) (tail s))
                                         (F (tail l) s)))

Problem 4

code

succ_pair_fst = \p.pair  (succ (fst p)) (snd p);
manipulate_head = \f.\l.(Cons (f (head l)) (tail l));
RLE_recur = fix (\F.\l.\s.(isnil l)
                             s
                             ((equal (snd (head s)) (head l))
                                   (F (tail l) (manipulate_head succ_pair_fst s))
                                   (F (tail l) (Cons (pair one (head l)) s))))
RLE = \l. reverse (RLE_recur (tail l) (Cons (pair one (head l)) Nil))

explain

RLE [1 1 1 2 2 3]
-> reverse  (RLE_recur [1 1 2 2 3] [[1 . 1]])
             -> RLE_recur [[1 . 1]] [1 1 2 2 3]
             -> RLE_recur [[2 . 1]] [1 2 2 3]
             -> RLE_recur [[3 . 1]] [2 2 3]
             -> RLE_recur [[1 . 2][3 . 1]] [2 3]
             -> RLE_recur [[2 . 2][3 . 1]] [3]
             -> RLE_recur [[1 . 3][2 . 2][3 . 1]] []
-> reverse [[1 . 3][2 . 2][3 . 1]]
-> [[3 . 1][2 . 2][1 . 3]]

Problem 5

code

GCD = fix (\F.\a.\b.
              (iszero a)
                   b
                   ((iszero b)
                       a
                       ((LE a b)
                            (F a (minus b a))
                            (F (minus a b) b))))

Problem 6

code

truthvalues = fix (\F.\n. (iszero n)
                            (Cons Nil Nil)
                            (Append (map (Cons tru) (F (pred n)))
                                    (map (Cons fal) (F (pred n)))));

example

truthvalues two
-> \c.\n.c (\c.\n.c (\x.\y.x) (c (\x.\y.x) (n))) (c (\c.\n.c (\x.\y.x) (c (\x.\y.y) (n))) (c (\c.\n.c (\x.\y.y) (c (\x.\y.x) (n))) (c (\c.\n.c (\x.\y.y) (c (\x.\y.y) (n))) (n))))
-> [[tru tru] [tru fal] [fal tru] [fal fal]]