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

 Page 1 of 1 [ 3 post ]

Relevant Pages