convert flip lambda into SKI terms -


i'm having trouble converting lambda flip ski combinators (i hope makes sense). here conversion:

/fxy.fyx /f./x./y.fyx /f./x.s (/y.fy) (/y.x) /f./x.s f (/y.x) /f./x.s f (k x) /f.s (/x.s f) (/x.k x) /f.s (/x.s f) k /f.s (s (/x.s) (/x.f)) k /f.s (s (k s) (k f)) k s (/f.s (s (k s) (k f))) (/f.k) s (/f.s (s (k s) (k f))) (k k) s (s (/f.s) (/f.s (k s) (k f))) (k k)  s (s (k s) (/f.s (k s) (k f))) (k k) s (s (k s) (s (/f.s (k s)) (/f.k f))) (k k) s (s (k s) (s (/f.s (k s)) k)) (k k) s (s (k s) (s (s (/f.s) (/f.k s)) k)) (k k) s (s (k s) (s (s (k s) (/f.k s)) k)) (k k) s (s (k s) (s (s (k s) (s (/f.k) (/f.s))) k)) (k k) s (s (k s) (s (s (k s) (s (k k) (k s))) k)) (k k)

if understand in b, c, k, w system, c flip , it's definition in ski terms s (s (k (s (k s) k)) s) (k k). answer isn't same c combinator... here rules used conversions:

k y = /x.y  - k combinator (skk) = /x.x  -  combinator (s (/x.f) (/x.g)) = (/x.fg)  -  s combinator y = (/x.yx)  -  eta reduction /x./y.f = /xy.f  - currying note s rule can convert longer expressions - example, λ x.abcdeg can converted setting f = abcde.

what missing?

once answer being accepted revised , figured out wrong.

your final result correct, although not "official" answer in text book, possible different ski terms equivalent same lambda expression.

s [s (k s) (s (s (k s) (s (k k) (k s))) k)] [k k] f x y -> s (k s) (s (s (k s) (s (k k) (k s))) k) f (k k f) x y -> k s f (s (s (k s) (s (k k) (k s))) k f) (k k f) x y -> s [s (s (k s) (s (k k) (k s))) k f] (k k f) x y -> s [s (k s) (s (k k) (k s))] k f x (k k f x) y -> s [k s] [s (k k) (k s)] f (k f) x (k k f x) y -> k s f (s (k k) (k s) f) (k f) x (k k f x) y -> s [s (k k) (k s) f] [k f] x (k k f x) y -> s [k k] [k s] f x (k f x) (k k f x) y -> k k f (k s f) x (k f x) (k k f x) y -> k (k s f) x (k f x) (k k f x) y -> k s f (k f x) (k k f x) y -> s [k f x] [k k f x] y -> k f x y (k k f x y) -> f y (k k f x y) -> f y (k x y) -> f y x

the above derive, based on left reduction order, proves final term equivalent c combinator.


Comments

Post a Comment

Popular posts from this blog

cakephp - simple blog with croogo -

i not problem, made simple blog in croogo, problem is not adding or modifying or delete, because arabic language ?? function add in controller `public function admin_add() { $this->set('title_for_layout', __('add part')); if (!empty($this->request->data)) { $this->part->create(); if ($this->part->save($this->request->data)) { $this->session->setflash(__('the part has been saved'), 'default', array('class' => 'success')); $this->redirect(array('action' => 'index'));//, $this->part->id)); } else { $this->session->setflash(__('the part not saved. please, try again.'), 'default', array('class' => 'error')); } } }` => model `class part extends appmodel { public $name = 'part'; var $belongst...
Read more

How to group boxplot outliers in gnuplot -

i have large set of data points. try plot them boxplot, of outliers exact same value , represented on line beside each other. found how set horizontal distance between outliers in gnuplot boxplot , doesn't much, apparently not possible. is possible group outliers together, print 1 point , print number in brackets beside indicate how many points there are? think make more readable in graph. for information, have 3 boxplots 1 x value , times 6 in 1 graph. using gnuplot 5 , played around pointsize, doesn't reduce distance anymore. hope can help! edit: set terminal pdf set output 'dat.pdf' file0 = 'dat1.dat' file1 = 'dat2.dat' file2 = 'dat3.dat' set pointsize 0.2 set notitle set xlabel 'x' set ylabel 'y' header = system('head -1 '.file0); n = words(header) set xtics ('' 1) set [i=1:n] xtics add (word(header, i) i) set style data boxplot plot file0 using (1-0.25):1:(0.2) boxplot lw 2 lc rgb '#8b0000...
Read more

bash - Performing variable substitution in a string -

i have string contains use of variable, , i'd substitute variable's value string. right best have is #!/bin/bash foo='$name; echo bar' name="the name" expanded="$(eval echo "$foo")" echo "$expanded" which has obvious defects: prints the name bar while i'd print the name; echo bar instead of eval can bash's regex matching bash's string replacement: foo='$name; echo bar' name="the name" [[ "$foo" =~ \$([[:alnum:]]+) ]] && s="${!bash_rematch[1]}" && expanded="${foo/\$${bash_rematch[1]}/$s}" echo "$expanded" name; echo bar
Read more