Skip to content

Instantly share code, notes, and snippets.

@kmicinski
Created March 29, 2021 06:32
Show Gist options
  • Save kmicinski/56b331a10415251b871c3c6a1648a08c to your computer and use it in GitHub Desktop.
Save kmicinski/56b331a10415251b871c3c6a1648a08c to your computer and use it in GitHub Desktop.
#lang racket
(define (expr? e)
(match e
[(? symbol? x) #t]
[`(lambda (,(? symbol? x)) ,(? expr? e-body)) #t]
[`(,(? expr? e0) ,(? expr? e1)) #t]
[_ #f]))
(define (free-vars e)
(match e
[(? symbol? x) (set x)]
[`(lambda (,x) ,e-body) (set-remove (free-vars e-body) x)]
[`(,e0 ,e1) (set-union (free-vars e0) (free-vars e1))]))
;; use capture-avoiding substitution to replace x with e-tgt in e-source
;; follow
(define (subst e-source x e-tgt)
(match e-source
[(? symbol? y) #:when (equal? x y) e-tgt]
[(? symbol? y) y]
[`(,e0 ,e1) `(,(subst e0 x e-tgt) ,(subst e1 x e-tgt))]
[`(lambda (,y) ,e-body) #:when (equal? x y) e-source] ;; leave it alone
[`(lambda (,y) ,e-body) #:when (not (set-member? (free-vars e-tgt) y))
`(lambda (,y) ,(subst e-body x e-tgt))]
[_ (error "No capture-avoiding substitution possible.")]))
@ilyes256
Copy link

This my ocaml file let rec free_vars e =
match e with
| LId x -> Set.singleton x
| LLam (x, e_body) -> Set.remove x (free_vars e_body)
| LApp (e0, e1) -> Set.union (free_vars e0) (free_vars e1)

let rec substitute (m: lterm) (s: string) (n: lterm): lterm =
match m with
| LId x when x = s -> n
| LId x -> LId x
| LApp (e0, e1) -> LApp (substitute e0 s n, substitute e1 s n)
| LLam (y, e_body) when s = y -> m
| LLam (y, e_body) when s <> y && not (Set.mem y (free_vars n)) ->
LLam (y, substitute e_body s n)
| _ -> m

I am not sure how to solve No capture-avoiding substitution possible.I want to rename the variable But I am not sure how to do it

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment