[plt-scheme] redex

Thanks for the suggestion, Casey. I've updated the webpage to use
..._1, like you say. (I'm also looking into better error messages, but
that's going to be longer term.)

Robby

2009/1/21 Casey Klein <clklein at cs.uchicago.edu>:
> 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
>