[racket] Alpha equivalence checking for Racket

From: Matthias Felleisen (matthias at ccs.neu.edu)
Date: Sun Dec 7 20:17:03 EST 2014

   
I guess you're on the right track but I'd expect #t for two alpha equivalent expressions: 

> > (alpha-equivalent? #'(λ (a) a) #'(λ (a) a))
> #f


Consider adding 
 (1) informal signatures to your functions 
 (2) a documentation line per function 
 (3) test cases (see rackunit)

You can check whether your tests are correct by running DrRacket's alpha renamer. 

-- Matthias





On Dec 7, 2014, at 6:25 PM, Adriaan Leijnse wrote:

> I've written a crude, incomplete and barely tested alpha equivalence
> checker for Racket syntax in case anyone's interested. It should work
> for most expression-level syntax. People have asked about
> functionality like this before [1], so I figure I'd share my code. Is
> this a good way to go about the problem or are there more concise
> solutions?
> 
> [1] http://lists.racket-lang.org/dev/archive/2011-March/005958.html
> 
> 
> #lang racket
> 
> (require syntax/parse
>         syntax/id-table
>         syntax/stx)
> 
> (define (alpha-equivalent? a b
>                           ;; Descend into syntax-quote forms
>                           #:do-syntax? [do-syntax? #t]
>                           ;; Expand before checking alpha-equivalence
>                           #:expand? [expand? #t])
>  (norm-equal? (normalize a
>                          #:do-syntax? do-syntax?
>                          #:expand? expand?)
>               (normalize b
>                          #:do-syntax? do-syntax?
>                          #:expand? expand?)))
> 
> (struct norm-id (i) #:transparent)
> (define (normalize stx
>                   #:do-syntax? [do-syntax? #t]
>                   #:expand? [expand? #t])
>  (define ctr 0)
>  (define (inc) (set! ctr (add1 ctr)) ctr)
>  (define env (make-free-id-table))
>  (define (put new-id)
>    (define new-nid (norm-id (inc)))
>    (dict-set! env new-id new-nid)
>    new-nid)
>  (define (get id)
>    (dict-ref env id id))
>  (define (put-λ-formals formals)
>    (syntax-parse #'formals
>      [(arg ...+ . restid)
>       `(,@(stx-map put #'(arg ...)) . ,(put #'restid))]
>      [restid
>       `(,(put #'restid))]))
>  (define (norm stx)
>    (syntax-parse stx
>      [((~literal #%expression) expr)
>       `(,#'#%expression ,(norm #'expr))]
>      [((~literal begin-for-syntax) form ...)
>       `(,#'begin-for-syntax ,(stx-map norm #'(form ...)))]
>      [((~literal #%provide) raw-provide-spec ...) ;; TODO
>       (error "Unimplemented" stx)]
>      [((~literal #%declare) declaration-keyword ...)
>       (error "Unimplemented" stx)] ;; TODO
>      [((~literal module) id module-path
>        ((~literal #%plain-module-begin) form ...))
>       `(,#'module ,'id ,'module-path
>          (,#'#%plain-module-begin ,@(stx-map norm #'(form ...))))]
>      [((~literal module*) id module-path
>        ((~literal #%plain-module-begin) form ...))
>       `(,#'module* ,'id ,'module-path
>          (,#'#%plain-module-begin ,@(stx-map norm #'(form ...))))]
>      [((~and define (~or (~literal define-values)
>                          (~literal define-syntaxes)))
>        (id ...)
>        expr)
>       `(,#'define
>          ,(stx-map put #'(id ...))
>          ,(norm #'expr))]
>      [((~literal #%require) raw-require-spec ...)
>       (error "Unimplemented" stx)] ;; TODO
>      [(~or d:keyword d:number d:boolean d:str d:char)
>       (syntax->datum #'d)]
>      [id:identifier
>       (get #'id)]
>      [((~literal #%plain-lambda) formals expr ...+)
>       `(,#'#%plain-lambda
>         ,@(put-λ-formals #'formals)
>         ,@(stx-map norm #'(expr ...)))]
>      [((~literal case-lambda) case ...)
>       (for/list ([c (syntax->list #'(case ...))])
>         (syntax-parse c
>           [(formals expr ...+)
>            `(,@(put-λ-formals #'formals)
>              ,@(stx-map norm #'(expr ...)))]))]
>      [((~literal if) p c a)
>       `(,#'if ,@(stx-map norm #'(p c a)))]
>      [((and begin~ (~or (~literal begin) (~literal begin0))) expr ...+)
>       `(,#'begin~ ,@(stx-map norm #'(expr ...)))]
>      [((~and let~ (~or (~literal let-values) (~literal letrec-values)))
>        (bindings ...)
>        expr
>        ...+)
>       (for/list ([b (syntax->list #'(bindings ...))])
>         (syntax-parse b
>           [[(id ...) _]
>            (stx-map put #'(id ...))]))
>       `(,#'let~
>         ,(for/list ([b (syntax->list #'(bindings ...))])
>            (syntax-parse b
>              [[(id ...) expr]
>               `(,(stx-map get #'(id ...)) ,(norm #'expr))]))
>         ,@(stx-map norm #'(expr ...)))]
>      [((~literal set!) id expr)
>       `(,#'set! ,(get #'id) ,(norm #'expr))]
>      [((~literal quote) datum)
>       `(,#'quote ,(syntax->datum #'datum))] ;; FIXME?
>      [(quote-syntax datum)
>       `(,#'quote-syntax ,(if do-syntax? (norm #'datum) #'datum))]
>      [((~literal with-continuation-mark) e1 e2 e3)
>       `(,#'with-continuation-mark ,@(stx-map norm #'(e1 e2 e3)))]
>      [((~literal #%plain-app) expr ...+)
>       `(,#'#%plain-app ,@(stx-map norm #'(expr ...)))]
>      [((~literal #%top) . id)
>       `(,#'#%top . #'id)] ;; FIXME?
>      [((~literal #%variable-reference) id)
>       `(,#'#%variable-reference ,(get #'id))]
>      [((~literal #%variable-reference) (#%top . id))
>       `(,#'#%variable-reference (,#'#%top . #'id))] ;; FIXME?
>      [((~literal #%variable-reference))
>       `(,#'#%variable-reference)]
>      [_ (error "Implementation error")]))
>  (norm (if expand?
>            (expand stx)
>            stx)))
> 
> (define (norm-equal? a b)
>  (match/values (values a b)
>    [((list x ...) (list y ...))
>     (if (= (length x) (length y))
>         (andmap norm-equal? x y)
>         #f)]
>    [((? identifier?) (? identifier?))
>     (free-identifier=? a b)]
>    [(_ _) (equal? a b)]))
> 
> ____________________
>  Racket Users list:
>  http://lists.racket-lang.org/users



Posted on the users mailing list.