alpha-equivalence-normal-form.rkt (2816B)
1 #lang racket 2 (let () 3 ;; Given an order-independent let 4 (let ([x 'b] 5 [y 'a]) 6 (cons x y)) 7 8 ;; e.g. represented roughly as: 9 (list 'let 10 (set (cons 'x ''b) (cons 'y ''a)) ;; bindings 11 (list 'cons 'x 'y)) ;; body 12 13 ;; Can we devise an α-equivalence normal form? 14 15 ;; Let's sort the right-hand side of the let bindings, and number them in that 16 ;; order. x gets renamed to var1, and y gets renamed to var0, given the order 17 ;; ('a, 'b) 18 (let ([var0 'a] 19 [var1 'b]) 20 (cons var1 var0)) 21 22 ;; The idea roughly amounts to transforming sets into lists by sorting their 23 ;; contents, knowing that the sort operation must not depend on unrenamed 24 ;; variables. Given a letrec, what can we do? 25 26 (let ([x 'b] 27 [y 'a]) 28 (letrec ([f (λ (v) (f (cons v x)))] 29 [g (λ (v) (g (cons v y)))]) 30 '…)) 31 32 ;; In the example above, x and y can be renamed first, giving var1 and var0 33 ;; respectively. Then it becomes possible to sort f and g, as they differ 34 ;; by their references to var1 and var0 respectively, and these have already 35 ;; been assigned a new number. 36 37 (letrec ([f (λ (v) (f v))] 38 [g (λ (v) (f v))]) 39 '…) 40 41 ;; Here, we have no difference in the values, but there is a difference in the 42 ;; way these values refer to the bingings: f refers to itself, while g refers to 43 ;; f. Topologically sorting that graph would give a cannon order. 44 45 (letrec ([f (λ (v) (g v))] 46 [g (λ (v) (f v))]) 47 '…) 48 49 ;; Here, there is no difference in the values, and swapping them gives a new 50 ;; graph isomorphic to the original. Another more complex case follows: 51 52 (letrec ([f (λ (v) (g v))] 53 [g (λ (v) (h v))] 54 [h (λ (v) (f v))]) 55 '…) 56 57 ;; In these cases, the order we assign to each variable does not matter, as they 58 ;; are strictly symmetric (in the sense that the bound values are at run-time 59 ;; observarionally identical). 60 61 ;; What general solution can we find? 62 ;; * What if we topo-sort bindings which cannot be distinguished by their values 63 ;; * then, within each SCC, if there are some values which are isomorphic to 64 ;; each other, they can be grouped together for the purpose of numbering. 65 ;; this operation can be repeated. 66 ;; * By alternating these two steps, do we systematically get a 67 ;; topologically-sorted DAG, where some nodes are a group of nodes which were 68 ;; isomorphic one level down? 69 ;; 70 ;; Relevant: 71 ;; @inproceedings{babai1983canonical, 72 ;; title={Canonical labeling of graphs}, 73 ;; author={Babai, L{\'a}szl{\'o} and Luks, Eugene M}, 74 ;; booktitle={Proceedings of the fifteenth annual ACM symposium on Theory of computing}, 75 ;; pages={171--183}, 76 ;; year={1983}, 77 ;; organization={ACM} 78 ;; } 79 (void))