From posting-system@google.com Tue Mar 25 22:13:38 2003 Date: Tue, 25 Mar 2003 14:13:34 -0800 From: oleg-at-pobox.com Newsgroups: comp.lang.functional Subject: Re: Lambda Calculus Question References: <13383d7a.0303250443.2ed626d@posting.google.com> Message-ID: <7eb8ac3e.0303251413.75dd88f0@posting.google.com> Status: OR The question seems to be about a term "switch n" such that switch 0 -> id switch n test1 stmt1 test2 stmt2 ... test_n stmt_n default -> stmt_i for the first i such that test_i -> true -> default otherwise Here n is a Church numeral, test_i are Church Booleans, stmt_i and default are arbitrary terms. Furthermore, we are required to use iteration rather than unrestricted recursion. Let us first consider a related term switch' such that switch' 0 -> id switch' n default test1 stmt1 test2 stmt2 ... test_n stmt_n -> stmt_i we can re-write the last line of the specification as switch' n = \default test stmt -> if test then (switch' (n-1) stmt) else (switch' (n-1) default) or, switch' n = \default test stmt -> (switch' (n-1)) (if test then stmt else default) Now we can replace recursion with the precise iteration do_times n f seed = iterate f seed !! n switch' n = do_times n f id where f seed = \def test stmt -> seed $if test then stmt else def This code however has a small flaw: it reduces to a stmt_i for the _last_ i such that test_i is true. When we transform switch' into the desired switch, the flaw disappears: switch n = do_times n f id id where f seed = \def test stmt -> seed$ if test then (const (def stmt)) else def Note the extra 'id', which plays the role of the initial 'def'. If test_i fails, that 'def' propagates further (and, at the end, will be applied to 'default'). The first successful test_i replaces 'def' with the 'const stmt_i' function, which now propagates all the way to the end. There, 'const stmt_i' is applied to 'default', and we get the desired result 'stmt_i'. We can re-write this Haskell-like code in Lambda-calculus, keeping in mind that 'do_times' is actually a Church numeral. We use the notation of the lambda calculator embedded in Haskell, as described on this site. The re-writing is straightforward. We should stress that the code employs neither the Y combinator, nor any arithmetic operations on the numeral 'n'. > module LC_switch where > import Lambda_calc > import LC_basic > import Prelude hiding ((^),and,or,not,succ,abs) > import qualified Prelude (and) > > combK = x^y^ x > > switch cn = cn # f # combI # combI > where > f = seed^ def^ test^ stmt^ seed # > (lif # test # (combK # (def#stmt)) # def) > [seed,def,test,stmt] = map make_var ["seed","def","test","stmt"] > > test1 = eval $(switch c0)#x -- result: x > test2 = eval$ (switch c2)#true#x#true#y#z -- result: x > test3 = eval $(switch c2)#false#x#true#y#z -- y > test4 = eval$ (switch c2)#false#x#false#y#z -- z > test5 = eval $(switch c3)#true#x#false#y#true#z#h -- x > test6 = eval$ (switch c3)#false#x#false#y#true#z#h -- z > test7 = eval \$ (switch c3)#false#x#false#y#(zerop#c1)#z#h -- h