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.

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

 Page 1 of 1 [ 4 post ]

Relevant Pages