[plt-scheme] redex is great

Hi Robby,
This does the job. Now
(term(curry((((λ(z)(z z))(λ(x y)(x(x y))))a)z)))
is reduced to (a(a(a(a z))) without any bifurcation.
May be the code should be simplified, but in this form it exposes my way of thinking.
I thought you might like to see the results of your appreciated help. Thanks very much.
Jos

;leftmost order β reduction

(define-language cλ
 (T (L (V) T) (T T) V) ; lambda terms
 (L λ lambda) ; lambda symbols
 (V (variable-except λ lambda))
 (N (L (V) N) M) ; normal forms
 (M V (M N)) ; normal form but not an abstraction
 (H
  (L (V) H)
  (M H)
  (side-condition (H_1 T) (not (term (abstr? H_1))))
  hole))

(define reductor
 (reduction-relation cλ
  (--> ; β contraction
   (in-hole H ((λ (V_1) T_1) T_2))
   (in-hole H (subst (V_1 T_2) T_1)))))

(define-extended-language bλ cλ
 (T .... any))
 
(define-metafunction bλ abstr? : T -> any
 ((abstr? (λ (V) T)) #t)
 ((abstr? T) #f))

----- Original Message ----- 
From: "Robby Findler" <robby at eecs.northwestern.edu>
To: "Jos Koot" <jos.koot at telefonica.net>
snip
You should define a language that consists of the contexts in which
you are allowed to reduce (say "L"). Mark the places where you can
reduce an application by 'hole' in that language.

Then, when you write

  (in-hole L ((λ x T_1) T_2))

that pattern will only match when the entire term matches an "L" and
the place where the "hole" was matches to "((λ x T_1) T_2)".

> Apparently I do not yet quite understand the working of
> `hole' and `in-hole'. I'll study on it.

In general, when you match (in-hole P1 P2) you match P1 and you expect
there to be a hole somewhere in P1. At that place, you match P2.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20090222/5d8d38bc/attachment.html>