Permalink
Browse files

Manually playing with symbols for understanding.

  • Loading branch information...
1 parent 501e877 commit 778107ae13886b765d01eb3d23292cc48bfd9177 @luqui committed Jul 3, 2009
Showing with 76 additions and 0 deletions.
  1. +76 −0 notes/hnf_reduction_example.txt
@@ -0,0 +1,76 @@
+Y = \f. (\x. f (x x)) (\x. f (x x))
+power1 = \pow e b. (e == 0) 1 (b * pow (e-1) b)
+power = Y power1
+
+
+(\p. p 3 + p 4) (power 2)
+
+(\p. p 3 + p 4) ((\f. (\x. f (x x)) (\x. f (x x))) (\pow e b. (e == 0) 1 (b * pow (e-1) b)) 2)
+ [ - - ] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+let p = (\f. (\x. f (x x)) (\x. f (x x))) (\pow e b. (e == 0) 1 (b * pow (e-1) b)) 2 in p 3 + p 4
+ [ - -] ~~~~~~~~~~~~~
+let p = (\f. let g = \x. f (x x) in f (g g)) (\pow e b. (e == 0) 1 (b * pow (e-1) b)) 2 in p 3 + p 4
+ [ - - ] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+let p = (let r = \pow e b. (e == 0) 1 (b * pow (e-1) b) in let g = \x. r (x x) in r (g g)) 2 in p 3 + p 4
+ [ --- ]
+let p = (let g = \x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x) in (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (g g)) 2 in p 3 + p 4
+ [ --- ] ~~~
+let p = (let g = \x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x) in (\e b. (e == 0) 1 (b * g g (e-1) b))) 2 in p 3 + p 4
+ [ ~ ~ ] ~
+let p = (let g = \x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x) in (\b. (2 == 0) 1 (b * g g (2-1) b))) in p 3 + p 4
+ --------
+let p = (let g = \x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x) in (\b. False 1 (b * g g (2-1) b))) in p 3 + p 4
+ -------------------------
+let p = (let g = \x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x) in (\b. b * g g (2-1) b)) in p 3 + p 4
+ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -
+let p = \b. b * (\x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x)) (\x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x)) (2-1) b in p 3 + p 4
+ [ --- ] ~~~
+let p = \b. b * (\x e b. (e == 0) 1 (b * x x (e-1) b)) (\x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x)) (2-1) b in p 3 + p 4
+ [ ] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+let p = \b. b * (let r = \x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x) in \e b. (e == 0) 1 (b * r r (e-1) b)) (2-1) b in p 3 + p 4
+ [ ] ~~~~~
+let p = \b. b * (let r = \x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x) in let z = 2-1 in \b. (z == 0) 1 (b * r r (z-1) b)) b in p 3 + p 4
+ ---
+let p = \b. b * (let r = \x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x) in let z = 1 in \b. (z == 0) 1 (b * r r (z-1) b)) b in p 3 + p 4
+ ~ - -
+let p = \b. b * (let r = \x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x) in \b. (1 == 0) 1 (b * r r (1-1) b)) b in p 3 + p 4
+ --------
+let p = \b. b * (let r = \x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x) in \b. False 1 (b * r r (1-1) b)) b in p 3 + p 4
+ -------------------------
+let p = \b. b * (let r = \x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x) in \b. b * r r (1-1) b) b in p 3 + p 4
+ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -
+let p = \b. b * (\b. b * (\x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x)) (\x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x)) (1-1) b) b in p 3 + p 4
+ [ ] ~~~
+let p = \b. b * (\b. b * (\x e b. (e == 0) 1 (b * x x (e-1) b)) (\x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x)) (1-1) b) b in p 3 + p 4
+ [ ] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+let p = \b. b * (\b. b * (let r = \x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x) in \e b. (e == 0) 1 (b * r r (e-1) b)) (1-1) b) b in p 3 + p 4
+ [ ] ~~~~~
+let p = \b. b * (\b. b * (let r = \x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x) in let z = 1-1 in \b. (z == 0) 1 (b * r r (z-1) b)) b) b in p 3 + p 4
+ ---
+let p = \b. b * (\b. b * (let r = \x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x) in let z = 0 in \b. (z == 0) 1 (b * r r (z-1) b)) b) b in p 3 + p 4
+ ~ - -
+let p = \b. b * (\b. b * (let r = \x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x) in \b. (0 == 0) 1 (b * r r (0-1) b)) b) b in p 3 + p 4
+ --------
+let p = \b. b * (\b. b * (let r = \x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x) in \b. True 1 (b * r r (0-1) b)) b) b in p 3 + p 4
+ ------------------------
+let p = \b. b * (\b. b * (let r = \x. (\pow e b. (e == 0) 1 (b * pow (e-1) b)) (x x) in \b. 1) b) b in p 3 + p 4
+ [ ] ~
+let p = \b. b * (\b. b * 1) b in p 3 + p 4
+ [ ] ~
+let p = \b. b * (b * 1) in p 3 + p 4
+ ~~~~~~~~~~~~~~~ - -
+(\b. b * (b * 1)) 3 + (\b. b * (b * 1)) 4
+ [ - - ] ~
+(3 * (3 * 1)) + (\b. b * (b * 1)) 4
+ -------
+(3 * 3) + (\b. b * (b * 1)) 4
+-------
+9 + (\b. b * (b * 1)) 4
+ [ - - ] ~
+9 + (4 * (4 * 1))
+ -------
+9 + (4 * 4)
+ -------
+9 + 16
+------
+25

0 comments on commit 778107a

Please sign in to comment.