[plt-scheme] redex

Jos,

On Wed, Jan 21, 2009 at 6:19 AM, Jos Koot <jos.koot at telefonica.net> wrote:
> However, when I try:
>
> (traces red (term ((λ (x) (x x x)) (λ (x) (x x x)))))
>
> I get:
>
> Welcome to DrScheme, version 4.1.4.1-svn17jan2009 [3m].
> Language: Module; memory limit: 1000 megabytes.
> syntax: incompatible ellipsis match counts for template in: ...
> No indication where.
>
> I carefully checked all ellipses, but cannot find any improper use.

This simpler term has the same behavior:

   (term ((λ (y) y) 1 2))

The error message isn't very helpful, but here's what's happening.
This term matches the "βv" rule with `x' bound to '(y) and `v' bound
to '(1 2):

> (redex-match λv (in-hole E ((λ (x ...) e) v ...)) (term ((λ (y) y) 1 2)))
(#(struct:match (#(struct:bind E #(struct:hole))
                          #(struct:bind e y)
                          #(struct:bind v (1 2))
                          #(struct:bind x (y)))))

This rule's right-hand side requires `x' and `v' to be bound to
equal-length lists because it "zips" them into a new list with "(x v)
...". This syntax-case expression has the same problem (but a better
error message):

(syntax-case #'((a b) (1 2 3)) ()
  [((x ...) (v ...))
   #'((x v) ...)])

The "βv" rule should probably be written

   (--> (in-hole E ((λ (x ..._1) e) v ..._1))
          (in-hole E (subst-n (x v) ... e))
          "βv")

so it doesn't fire when the argument count doesn't match the parameter count.

> I also noticed that
> (traces red (term (((λ x (λ y x)) y) z)))
> does not contract.
> That's due to the capture avoidance.

First, you're missing the parens around the parameter names; i.e., you
want (term (((λ (x) (λ (y) x)) y) z)). But more to the point, "βv"
applies only when the arguments are values, and according to the λv
grammar, a variable is not a value:

   (v (λ (x ...) e) number +)

HTH,
Casey