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

headredex reduction

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/>