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