Q: reduction strategies in lambda calculus
Author Message Q: reduction strategies in lambda calculus

Hello,

I am wondering, if anybody knows literature, which discusses "monotonic"
reduction strategies of lambda terms in the sense defined below.

Definitions:
A reduction strategy (RS) (cf. Barendregt) is a function which maps lambda
terms to lambda terms, to which they can be reduced (w.r.t. the standard
reduction relation -*-> of lambda calculus).

A RS shall be called monotonic w.r.t. -*->,
if for every two lambda terms e and e' with e -*-> e', RS(e) -*-> RS(e') holds.

In this sense normal order reduction is monotonic. But applicative order
(AORS) is not, because

(\x. f x x) ((\y. y) z) -*-> f ((\y. y) z) ((\y. y) z)    -- by one

but:

AORS ((\x. f x x) ((\y. y) z)) = (\x. f x x) z
-*/->
AORS (f ((\y. y) z) ((\y. y) z)) = f z ((\y. y) z)

Motivation:
The monotonicity seemed to me a very reasonable property of reduction
strategies in implemenations of functional languages, until I realised
that applicative order reduction (s.a.) is not monotonic. Nevertheless it
is a nice property with nice implications. Especially it seems to be
connected with non-copying of redexes.

Can anybody point me to a discussion of this class of reduction
strategies, or convince me of there insignificance?

Thanks and regards,
Dirk Pape.

--
Dirk Pape          Freie Universit?t Berlin
www: < http://www.*-*-*.com/ ~pape/>

Tue, 04 Dec 2001 03:00:00 GMT

 Page 1 of 1 [ 1 post ]

Relevant Pages