Lambda Calculus Question 
Author Message
 Lambda Calculus Question

Basically, I made a switch statement in LC as in the following:

  switch :=     Y (\sw? value taken num ->
                    (Zero? num) value
                    (\test_i stmt_i ->
                      (And (Not Taken) test_i)
                        (sw? (K stmt_i) True)
                        (sw? value taken)
                      (pred num)
                    )
                  ) I F

I'm sure this is nothing revolitionary (which means I must be getting
to a question...).  Here's how it works:
        switch N case_1 stmt_1 ... case_n stmt_n default_case
        - return stmt_i for the first true case_i, or default_case if no such
case_i exists

so switch 0 is the identity function and thus returns the
default_case.

Any representation of naturals will work as long as you have the Zero?
predicate and the predecessor function.  My question is thus:

"Given a church numeral C_n, is there a statement SW that works
similar to switch by supplying some succ and zero to C_n so that the
same effect is gathered."

I realize that  (\C_n -> C_n I switch)  is a valid answer, but what
I'm asking for a solution that uses the iterative nature of using
church numerals to consume the input and return the answer...

Thank you any help / solution / guidance :-)

~Matthew Maycock



Sat, 10 Sep 2005 20:43:00 GMT  
 Lambda Calculus Question

Quote:

> I realize that  (\C_n -> C_n I switch)  is a valid answer, but what
> I'm asking for a solution that uses the iterative nature of using
> church numerals to consume the input and return the answer...

Here is one solution that seems to work. It could probably be
simplified quite a bit.

let switch =
  \num
         (zero? num I
      (num
                  \next \x
                         (x false \found? \value \pred \stmt
                                (next true
                                  (found? \a value (pred \a stmt I))
              (found?
                                         (next false true value)
                                         (pred (next false true stmt)
                                                (next false false value)))))
         \a true false false I))

and usage

(switch 3
  false a
  true b
  true c
  d) --> b

This kind of structure is fairly error prone though, since adding
clauses requires changing the numeral. I usually have explicit
statements to signify whether the clause is the last (default) one.
e.g.

let cond =
  (Y \f \a
         (a I \a (a
                (Y \f \a
                  \b (b \b a
                         \b \b (f a)))
      \a f)))

let case =
  \a I

let else =
  K

and then use something like

(Y \self \f \x
  (cond
    case (null? x)
           null
    case (pair? (car x))
           (cons (self f (car x))
                 (self f (cdr x)))
    else
                (cons (f (car x))
                                (self f (cdr x)))))

--
aki helin



Sun, 11 Sep 2005 00:26:44 GMT  
 Lambda Calculus Question
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

Furthermore, we are required to use iteration rather than an
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 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. The flaw can be easily rectified

switch' n = do_times n f id
  where
       f seed = \def test stmt ->
                seed $ if test then (const (def stmt)) else def

Now the first successful test_i causes threading of the corresponding
stmt_i all the way to the end.

We can now turn switch' to the required switch:

switch n = do_times n f id id
  where
     f seed = \def test stmt -> seed $ if test then (const (def stmt)) else def

We can re-write this Haskell-like code in Lambda-calculus, keeping in
mind that 'do_times' is actually a Church numeral. As the code below
shows, the re-writing is straightforward. The code is written in the
notation of a lambda calculator embedded in Haskell:

        http://pobox.com/~oleg/ftp/Computation/lambda-calc.html

Quote:
> 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



Sun, 11 Sep 2005 06:13:34 GMT  
 
 [ 3 post ] 

 Relevant Pages 

1. Question: lambda calculus (what is the advantage)?

2. lambda calculus implementation

3. Introduction to lambda calculus ?

4. Lambda Calculus Problem!

5. Negativism and division in lambda-calculus

6. Lambda calculus + Church numerals

7. Typed lambda calculus, recursion and halting

8. lambda calculus: delta rules

9. Need help on Lambda calculus reduction please.

10. Q: reduction strategies in lambda calculus

11. Lambda-Calculus

12. Introduction to Lambda Calculus

 

 
Powered by phpBB® Forum Software