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