A student today pointed out the standard reduction definition for ISWIM on pg 225 in SEwPR is broken:
#lang racket (require redex) ;; iswim ;; definition from pg 217 (define-language iswim ((M N L K) X (λ X M) (M M) b (o2 M M) (o1 M)) (o o1 o2) (o1 add1 sub1 iszero) (o2 + - *) (b number) ((V U W) b X (λ X M)) (E hole (V E) (E M) (o V ... E M ...)) (X Y Z variable-not-otherwise-mentioned)) (define-metafunction iswim subst : any ... -> any) ;; iswim-standard ;; definition from pg 225 (define iswim-standard (reduction-relation iswim (v ((λ X M) V) (subst M X V) vω) (v (o b ...) (δ (o b ...)) δ) with [(--> (in-hole E M) (in-hole E N)) (v M N)])) Error message: "reduction-relation: shortcut name may not be a non-terminal in: M" Only posting this here since I couldn't find anything about it on the errata. Have a good day! Best, Andrew -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout.
