Beta like reduction rules for lambda calculus 
Author Message
 Beta like reduction rules for lambda calculus

If anyone knows of any work on "beta like" reduction rules
for lambda calculus, I would really appreciate it if they
could mail me some references or any other pointers.

                       Thanks in advance,

                       Sundeep Oberoi



Fri, 10 Mar 1995 15:18:25 GMT  
 Beta like reduction rules for lambda calculus

Quote:

>If anyone knows of any work on "beta like" reduction rules
>for lambda calculus, I would really appreciate it if they
>could mail me some references or any other pointers.

Could you clarify what you mean by "beta like"?




Fri, 10 Mar 1995 22:54:57 GMT  
 Beta like reduction rules for lambda calculus

Quote:
>If anyone knows of any work on "beta like" reduction rules
>for lambda calculus, I would really appreciate it if they
>could mail me some references or any other pointers.

Well, consider the following notation to represent "assignments" to array
components (or when thinking of r as a "reference" operator -- to pointers
references):

                         let r(x) <- y in E

Define it as follows:

                  (lambda r.E) ( lambda z. if (z==x) y r(z) )

Then the following:

                 let ref(a) <- 1 in
                    let b = a in
                       let ref(b) <- 0 in
                           ref(a)

encodes the imperative language segment:

                   *a = 1; b = a; *b = 0; return *a;

Observe its Beta reduction:

              let ref(a) <- 1 in
                 let b = a in
                    let ref(b) <- 0 in
                        ref(a)
=
             lambda ref.(
                let b = a in
                   (lambda ref. ref(a)) (lambda z. if (z==b) 0 ref(z))
             ) (lambda x. if (x==a) 1: ref(x))
->           let b = a in
                (lambda ref. ref(a))
                   (lambda z. if (z==b) 0 (lambda x. if (x==a) 1: ref(x))(z))
->           (lambda ref. ref(a))
                (lambda z. if (z==a) 0 (lambda x. if (x==a) 1: ref(x))(z))
->           (lambda z. if (z==a) 0 (lambda x. if (x==a) 1: ref(x)) (z)) (a)
->           if (a==a) 0 (lambda x. if (x==a) 1: ref(x))(a)
->           if (true) 0 (lambda x. if (x==a) 1: ref(x))(a)
->           0

That's right:  0, not 1.  The a and b "alias".  Therefore, aliasing and
pointers are purely functional concepts, NOT imperative.

If you axiomatically define the <- operation, you'd might get a Beta reduction
along these lines (reducing from inside out for illustration here):

              let ref(a) <- 1 in
                 let b = a in
                    let ref(b) <- 0 in
                        ref(a)

->            let ref(a) <- 1 in
                 let b = a in
                    if (a==b) 0 ref(a)

->            let ref(a) <- 1 in
                 if (a==a) 0 ref(a)

->            let ref(a) <- 1 in
                 if (true) 0 ref(a)

->            let ref(a) <- 1 in 0

->            0

In many ways, "ref" behaves like a symbol table, or an environment.



Sat, 18 Mar 1995 21:52:15 GMT  
 
 [ 4 post ] 

 Relevant Pages 

1. Need help on Lambda calculus reduction please.

2. Q: reduction strategies in lambda calculus

3. Lambda calculus/Lisp - renaming and reduction help!

4. Need help on Lambda calculus reduction please.

5. Lambda calculus/Lisp - renaming and reduction help!

6. Need help on Lambda calculus reduction please.

7. lambda calculus: delta rules

8. Lambda Calculus Question

9. lambda calculus implementation

10. Introduction to lambda calculus ?

11. Lambda Calculus Problem!

12. Negativism and division in lambda-calculus

 

 
Powered by phpBB® Forum Software