Skip to content

Instantly share code, notes, and snippets.

@xatier

xatier/gist:4316737

Created December 17, 2012 08:39
Show Gist options
  • Save xatier/4316737 to your computer and use it in GitHub Desktop.
Save xatier/4316737 to your computer and use it in GitHub Desktop.
Download ZIP
QAQ
Raw
gistfile1.txt
1.
a) \f.\a.\b.\c.c (f a) (f b)
f = t1
a = t2
f a = t3
=> t1 = t2 -> t3
b = t4
f b = t5
=> t1 = t4 -> t5
=> t2 = t4, t3 = t5
c = t6
c (f a) = t7
=> t6 = t5 -> t7
c (f a) (f b) = t8
=> t7 = t5 -> t8
\f.\a.\b.\c.c (f a) (f b) = t9
=> t9 = t1 -> t2 -> t4 -> t6 -> t8
=> (t4 -> t3) -> t4 -> t4 -> (t5 -> (t5 -> t8)) -> t8
- fun ff f a b c = c (f a) (f b);
val ff = fn : ('a -> 'b) -> 'a -> 'a -> ('b -> 'b -> 'c) -> 'c
b) \f.\a.\b.b f (f a b)
b = t1
f = t2
b f = t3
=> t2 = t1 -> t3 --- 1
a = t4
f a = t5
=> t2 = t4 -> t5 --- 2
(1) & (2)
=> t1 = t4, t3 = t5 -- 3
f a b = t6
=> t5 = t1 -> t6
(3)
=> t3 = t1 -> t6 --- 4
b f (f a b) = t7
=> t3 = t6 -> t7 --- 5
(4) & (5)
=> t1 = t6, t6 = t7 = t1
\f.\a.\b.b f (f a b) = t8
=> t2 -> t4 -> t1 -> t7 -> t8
note: 會 circular
- fun ff f a b = b f (f a b);
stdIn:22.13-28.3 Error: operator is not a function [circularity]
operator: 'Z
in expression:
(f a) b
c) fix = \f.f (\x.fix f x)
f = t1
fix = t2
fix f = t3
=> t2 = t1 -> t3
x = t4
fix f x = t5
=> t3 = t4 -> t5
\x.fix f x = t6
=> t6 = t4 -> t5
f (\x.fix f x) = t7
=> t1 = t5 -> t7
fix = \f.f (\x.fix f x) = t2
=> t2 = t1 -> t7
=> t3 = t7
t2 = t1 -> t3 = t1 -> (t4 -> t5)
2.
fun flodr f a [] = a
| foldr f a (x::xs) = f(x, foldr f a xs);
fun flodl f a [] = a
| flodl f a (x::xs) = flodl f (f(a, x)) xs;
a) lemma: x + (y X z) = (x + y) X z
proof: y + (flodl X z xs) = flodl X (y + z) xs, for any list xs.
base case: xs = []
lhs
= y + (foldl X z []) # apply rule of foldl
= y + z
rhs
= foldl X (y + z) [] # apply rule of foldl
= (y + z)
= rhs
hypothesis
y + (flodl X z xs) = flodl X (y + z) xs, for list xs.
induction case: xs = a::as
lhs
= y + (foldl X z (a::as))
= y + (foldl X (z X a) as) # apply rule of foldl
= flodl X (y + (z X a)) as # by induction hypothesis
rhs
= flodl X (y + z) (a::as) # apply rule of flodl
= flodl X ((y + z) X a) as # apply the lemma:
= flodl X (y + (z X a)) as
= lhs
Q.E.D.
b) lemma (a): x + (y X z) = (x + y) X z
theorem: x + a = a X x
proof: flodr + a xs = flodl X a xs, for any list xs
base case: xs = []
lhs
= flodr + a [] # the definition of flodr
= a
rhs
= flodl X a [] # the definition of flodl
= a
hypothesis
flodr + a xs = flodl X a xs, for any list xs
induction case: xs = b::bx
lhs
= flodr + a (b::bs)
= b + (foldr + a bs) # rule of foldr
= b + (foldl X a bs) # by induction hypothesis
= flodl X (b + a) bs # the definition of foldl
rhs
= flodl X a (b::bs)
= flodl X (a X b) bs # by the theorem
= flodl X (b + a) bs
= lhs
Q.E.D.
c) + is associative and a is the identity of +
proof: foldr + a xs = foldl + a xs, for any list xs
base case: xs = []
# by the definition of foldr and foldl
foldr + a [] = a = foldl + a xs
hypothesis
foldr + a xs = foldl + a xs, for any list xs
induction case: xs = x::as
lhs
= foldr + a xs # by b)
= foldl X a xs
= foldl X a (x::xs) # by rule of foldl
= foldl X (a + x) xs # a is the identity of +
= foldl X x xs
rhs
= foldl + a (x::xs)
= foldl + (a + x) xs # again, a is the identity of +
= foldl + x xs
= fold X x xs # from b)
= lhs
d)
define
val sumr = foldr + 0;
val suml = foldl + 0;
proof: sumr xs = suml xs
base case: xs = []
sumr [] = foldr + 0 [] = 0
suml [] = foldl + 0 [] = 0
hypothesis
sumr xs = suml xs
induction case: xs = x::xs
lhs
= sumr x::xs
= foldr + 0 (x::xs) # by c)
= foldl + 0 (x::xs)
= foldl + (0 + x) xs
= foldl + x xs
rhs
= suml x::xs
= foldl + 0 (x::xs) # apply rule of foldl
= foldl + (0 + x) xs
= foldl + x xs
= lhs
e) define
fun revr xs = foldr (fn (x, xs) => xs@[x]) [] xs;
fun revl xs = foldl (fn (xs, x) => x::xs) [] xs;
proof: revr xs = revl xs, for any list xs
goal: revr is +, revl is X in theorem b
x + a = a X x
obviously, xs@[x] == x::xs
x + (y X z) = (x + y) X z
lhs
= x + (z::y)
= z::y@[x]
rhs
= (y@[z]) X z
= z::y@[x]
= lhs
Q.E.D
f)
fun revl xs = foldl (fn (x, xs) => x ::xs) [] xs;
3.
a) n2c
- fun n2c 0 f x = x
= | n2c n f x = f(n2c (n - 1) f x);
val n2c = fn : int -> ('a -> 'a) -> 'a -> 'a
- n2c 10 (fn x => x+1) 0;
val it = 10 : int
b) c2n
- fun c2n n = n (fn x => x+1) 0;
val c2n = fn : ((int -> int) -> int -> 'a) -> 'a
- (c2n o n2c) 7;
val it = 7 : int
c) ++
- fun ++ 0 0 f x = x
= m 0 f x = f((m-1) 0 f x)
= 0 n f x = f(0 (n-1) f x)
= m n f x = f((m-1) 0 f x);
infix 6 ++
d) **
Q__Q
4.
a)
+----+ +----+ +----+ +----+
|succ|->|succ|->|succ|->|zero|
+----+ +----+ +----+ +----+
b)
- fun n2N 0 = Zero
= | n2N n = Succ (n2N (n-1));
val n2N = fn : int -> Nat
- n2N 10;
val it = Succ (Succ (Succ (Succ (Succ #)))) : Nat
c)
fun N2n Zero = 0
| N2n Succ xs = 1 + N2n xs
d, e)
Q__Q
f)
fun !!! Zero = 1
| !!! Succ xs = 1 * !!! xs
g)
fun ! 0 = 0
| ! n = N2n(n2N(n-1) *** n2N(1))
5.
Q__Q
6.
a)
X(2) # ctor
X(1) # ctor
X(1) # dtor
X(2) # dtor
b)
run time stack:
+------------+
|ctor X::X(2)|
+------------+
| q(2) |
+------------+
| p(2) |
+------------+
| main() |
+------------+
type_info: catch table
+------------+ +---+
| X | | | --> { p(2-1); }
+------------+ +---+
| int | | | --> { cout << c; }
+------------+ +---+
exception table: heap:
+--------+ +-----------+
| X(2) | ----> X ---> | +-------+ |
+--------+ | |int(2) | |
| +-------+ |
+-----------+
c)
run time stack:
+------------+
| q(0) |
+------------+
| p(0) |
+------------+
| p(1) |
+------------+
| p(2) |
+------------+
| main() |
+------------+
type_info: catch table
+---+
| | --> { p(1-1); }
+---+
| | --> { cout << c; }
+------------+ +---+
| X | | | --> { p(2-1); }
+------------+ +---+
| int | | | --> { cout << c; }
+------------+ +---+
exception table: heap:
+--------+ +-----------+
| X(2) | ----> instance X(2) -> | +-------+ |
+--------+ | |int(2) | |
| X(1) | | +-------+ |
+--------+ | |
\ ---> instance X(1) -> | +-------+ |
| |int(1) | |
| +-------+ |
+-----------+
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment