suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Changed let-poly's unification algorithm

Browse Source 
to be simpler and clearer

This caused bug #6's counterexample to change
because the unification algorithm no longer calls
∨ so we have to find a different way to call it
This commit is contained in:
Robby Findler 2014-04-01 16:29:39 -05:00
parent ea3b5c0742
commit 20b7d959f3
16 changed files with 203 additions and 355 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/1.diff
View File

@ -6,7 +6,7 @@
< (tc-down (x y Γ) M (λ y κ) σ_ans)
---
> (tc-down (x y Γ) M (λ x κ) σ_ans)
571a572,574
552a553,555
>
> (define small-counter-example '(hd ((λ x x) 1)))
> (test-equal (check small-counter-example) #f)

2
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/2.diff
View File

@ -16,7 +16,7 @@
< [(where #t (not-v? M))
< (tc-down Γ ((λ x N) M) κ σ_2)
< ---------------------------------
571a567,572
552a548,553
>
> (define small-counter-example '(let ([x (new nil)])
> ((λ ignore

2
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/3.diff
View File

@ -6,7 +6,7 @@
< (where G (unify τ_2 (τ_1 → x)))
---
> (where G (unify τ_1 (τ_2 → x)))
571a572,574
552a553,555
>
> (define small-counter-example (term (1 cons)))
> (test-equal (check small-counter-example) #f)

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff
View File

@ -4,11 +4,11 @@
> (define the-error
> (string-append "misspelled the name of a metafunction in a side-condition, "
> "causing the occurs check to not happen"))
212c214
< [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
205c207
< [(uh (x τ G) Gx) ⊥ (where #t (in-vars-τ? x τ))]
---
> [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars? x τ))]
571a574,576
> [(uh (x τ G) Gx) ⊥ (where #t (in-vars? x τ))]
552a555,557
>
> (define small-counter-example (term ((λ x (x x)) hd)))
> (test-equal (check small-counter-example) #f)

4
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/5.diff
View File

@ -2,7 +2,7 @@
< (define the-error "no error")
---
> (define the-error "eliminate-G was written as if it always gets a Gx as input")
225,226c225,228
214,215c214,217
< [(eliminate-G x τ (σ_1 σ_2 G))
< ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))])
---
@ -10,7 +10,7 @@
> (τ (eliminate-τ x τ σ) (eliminate-G x τ G))]
> [(eliminate-G x τ (y σ G))
> (y (eliminate-τ x τ σ) (eliminate-G x τ G))])
560,571c562,577
541,552c543,558
< (let ([t-type (type-check M)])
< (implies
< t-type

6
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/6.diff
View File

@ -2,11 +2,11 @@
< (define the-error "no error")
---
> (define the-error "∨ has an incorrect duplicated variable, leading to an uncovered case")
240c240
229c229
< [(∨ boolean_1 boolean_2) #t])
---
> [(∨ boolean boolean) #t])
560,571c560,575
541,552c541,556
< (let ([t-type (type-check M)])
< (implies
< t-type
@ -34,5 +34,5 @@
> (or (equal? red-t "error")
> (zero? n) (loop red-t (- n 1))))))))))))))
>
> (define small-counter-example (term ((λ x x) 1)))
> (define small-counter-example (term (λ x (x x))))
> (test-equal (check small-counter-example) #f)

4
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/7.diff
View File

@ -9,13 +9,13 @@
< (let ([x E]) M))
---
> (v E))
306,307c307,308
287,288c288,289
< (--> (Σ (in-hole E (let ([x v]) M)))
< (Σ (in-hole E (subst M x v)))
---
> (--> (Σ (in-hole E (let ([x M]) N)))
> (Σ (in-hole E ((λ x N) M)))
571a573,575
552a554,556
>
> (define small-counter-example (term (let ((x (λ y y))) (x x))))
> (test-equal (check small-counter-example) #f)

65
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt
View File

@ -168,56 +168,45 @@ bring that type back, recurring on the continuation.
(define-metafunction stlc
unify : τ τ -> Gx or ⊥
[(unify τ σ) (uh (τ σ ·) · #f)])
[(unify τ σ) (uh (τ σ ·) ·)])
#|
Algorithm copied from _An Efficient Unification Algorithm_ by
Alberto Martelli and Ugo Montanari (section 2).
http://www.nsl.com/misc/papers/martelli-montanari.pdf
This isn't the eponymous algorithm; it is an earlier one
in the paper that's simpler.
Algorithm copied from Chapter 8 in _Handbook of Automated Reasoning_:
Unification Theory by Franz Baader and Wayne Synder
http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf
The 'uh' function iterates over a set of equations applying the
rules from the paper, moving them from the first argument to
the second argument and tracking when something changes.
It runs until there are no more changes. The (a), (b),
(c), and (d) are the rule labels from the paper.
rules from the paper, building up the result substitution in G_r.
|#
(define-metafunction stlc
uh : G G boolean -> Gx or ⊥
[(uh · G #t) (uh G · #f)]
[(uh · G #f) G]
uh : G Gx -> Gx or ⊥
;; (a)
[(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
[(uh · Gx) Gx]
;; (b)
[(uh (x x G) G_r boolean) (uh G G_r #t)]
;; orient
[(uh (τ x G) Gx) (uh (x τ G) Gx) (where #t (not-var? τ))]
;; (c) -- term reduction
[(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
[(uh ((list τ) (list σ) G) G_r boolean) (uh (τ σ G) G_r #t)]
[(uh ((ref τ) (ref σ) G) G_r boolean) (uh (τ σ G) G_r #t)]
[(uh (int int G) G_r boolean) (uh G G_r #t)]
;; trivial (other cases are covered by decomposition rule)
[(uh (x x G) Gx) (uh G Gx)]
;; (c) -- failure
[(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
;; decomposition
[(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) Gx) (uh (τ_1 σ_1 (τ_2 σ_2 G)) Gx)]
[(uh ((list τ) (list σ) G) Gx) (uh (τ σ G) Gx)]
[(uh ((ref τ) (ref σ) G) Gx) (uh (τ σ G) Gx)]
[(uh (int int G) Gx) (uh G Gx)]
;; (d) -- x occurs in τ case
[(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
;; symbol clash
[(uh (τ σ G) Gx) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
;; (d) -- x does not occur in τ case
[(uh (x τ G) G_r boolean)
(uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
(where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
;; occurs check
[(uh (x τ G) Gx) ⊥ (where #t (in-vars-τ? x τ))]
;; no rules applied; try next equation, if any.
[(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
;; variable elimination
[(uh (x τ G) Gx)
(uh (eliminate-G x τ G) (x τ (eliminate-G x τ Gx)))])
(define-metafunction stlc
eliminate-G : x τ G -> G
@ -253,14 +242,6 @@ It runs until there are no more changes. The (a), (b),
[(in-vars-τ? x x) #t]
[(in-vars-τ? x y) #f])
(define-metafunction stlc
in-vars-G? : x G -> boolean
[(in-vars-G? x ·) #f]
[(in-vars-G? x (x τ G)) #t]
[(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ)
(∨ (in-vars-τ? x τ)
(in-vars-G? x G)))])
(define-metafunction stlc
apply-subst-τ : Gx τ -> τ
[(apply-subst-τ · τ) τ]

65
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt
View File

@ -163,56 +163,45 @@ bring that type back, recurring on the continuation.
(define-metafunction stlc
unify : τ τ -> Gx or ⊥
[(unify τ σ) (uh (τ σ ·) · #f)])
[(unify τ σ) (uh (τ σ ·) ·)])
#|
Algorithm copied from _An Efficient Unification Algorithm_ by
Alberto Martelli and Ugo Montanari (section 2).
http://www.nsl.com/misc/papers/martelli-montanari.pdf
This isn't the eponymous algorithm; it is an earlier one
in the paper that's simpler.
Algorithm copied from Chapter 8 in _Handbook of Automated Reasoning_:
Unification Theory by Franz Baader and Wayne Synder
http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf
The 'uh' function iterates over a set of equations applying the
rules from the paper, moving them from the first argument to
the second argument and tracking when something changes.
It runs until there are no more changes. The (a), (b),
(c), and (d) are the rule labels from the paper.
rules from the paper, building up the result substitution in G_r.
|#
(define-metafunction stlc
uh : G G boolean -> Gx or ⊥
[(uh · G #t) (uh G · #f)]
[(uh · G #f) G]
uh : G Gx -> Gx or ⊥
;; (a)
[(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
[(uh · Gx) Gx]
;; (b)
[(uh (x x G) G_r boolean) (uh G G_r #t)]
;; orient
[(uh (τ x G) Gx) (uh (x τ G) Gx) (where #t (not-var? τ))]
;; (c) -- term reduction
[(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
[(uh ((list τ) (list σ) G) G_r boolean) (uh (τ σ G) G_r #t)]
[(uh ((ref τ) (ref σ) G) G_r boolean) (uh (τ σ G) G_r #t)]
[(uh (int int G) G_r boolean) (uh G G_r #t)]
;; trivial (other cases are covered by decomposition rule)
[(uh (x x G) Gx) (uh G Gx)]
;; (c) -- failure
[(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
;; decomposition
[(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) Gx) (uh (τ_1 σ_1 (τ_2 σ_2 G)) Gx)]
[(uh ((list τ) (list σ) G) Gx) (uh (τ σ G) Gx)]
[(uh ((ref τ) (ref σ) G) Gx) (uh (τ σ G) Gx)]
[(uh (int int G) Gx) (uh G Gx)]
;; (d) -- x occurs in τ case
[(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
;; symbol clash
[(uh (τ σ G) Gx) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
;; (d) -- x does not occur in τ case
[(uh (x τ G) G_r boolean)
(uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
(where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
;; occurs check
[(uh (x τ G) Gx) ⊥ (where #t (in-vars-τ? x τ))]
;; no rules applied; try next equation, if any.
[(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
;; variable elimination
[(uh (x τ G) Gx)
(uh (eliminate-G x τ G) (x τ (eliminate-G x τ Gx)))])
(define-metafunction stlc
eliminate-G : x τ G -> G
@ -248,14 +237,6 @@ It runs until there are no more changes. The (a), (b),
[(in-vars-τ? x x) #t]
[(in-vars-τ? x y) #f])
(define-metafunction stlc
in-vars-G? : x G -> boolean
[(in-vars-G? x ·) #f]
[(in-vars-G? x (x τ G)) #t]
[(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ)
(∨ (in-vars-τ? x τ)
(in-vars-G? x G)))])
(define-metafunction stlc
apply-subst-τ : Gx τ -> τ
[(apply-subst-τ · τ) τ]

65
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt
View File

@ -168,56 +168,45 @@ bring that type back, recurring on the continuation.
(define-metafunction stlc
unify : τ τ -> Gx or ⊥
[(unify τ σ) (uh (τ σ ·) · #f)])
[(unify τ σ) (uh (τ σ ·) ·)])
#|
Algorithm copied from _An Efficient Unification Algorithm_ by
Alberto Martelli and Ugo Montanari (section 2).
http://www.nsl.com/misc/papers/martelli-montanari.pdf
This isn't the eponymous algorithm; it is an earlier one
in the paper that's simpler.
Algorithm copied from Chapter 8 in _Handbook of Automated Reasoning_:
Unification Theory by Franz Baader and Wayne Synder
http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf
The 'uh' function iterates over a set of equations applying the
rules from the paper, moving them from the first argument to
the second argument and tracking when something changes.
It runs until there are no more changes. The (a), (b),
(c), and (d) are the rule labels from the paper.
rules from the paper, building up the result substitution in G_r.
|#
(define-metafunction stlc
uh : G G boolean -> Gx or ⊥
[(uh · G #t) (uh G · #f)]
[(uh · G #f) G]
uh : G Gx -> Gx or ⊥
;; (a)
[(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
[(uh · Gx) Gx]
;; (b)
[(uh (x x G) G_r boolean) (uh G G_r #t)]
;; orient
[(uh (τ x G) Gx) (uh (x τ G) Gx) (where #t (not-var? τ))]
;; (c) -- term reduction
[(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
[(uh ((list τ) (list σ) G) G_r boolean) (uh (τ σ G) G_r #t)]
[(uh ((ref τ) (ref σ) G) G_r boolean) (uh (τ σ G) G_r #t)]
[(uh (int int G) G_r boolean) (uh G G_r #t)]
;; trivial (other cases are covered by decomposition rule)
[(uh (x x G) Gx) (uh G Gx)]
;; (c) -- failure
[(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
;; decomposition
[(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) Gx) (uh (τ_1 σ_1 (τ_2 σ_2 G)) Gx)]
[(uh ((list τ) (list σ) G) Gx) (uh (τ σ G) Gx)]
[(uh ((ref τ) (ref σ) G) Gx) (uh (τ σ G) Gx)]
[(uh (int int G) Gx) (uh G Gx)]
;; (d) -- x occurs in τ case
[(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
;; symbol clash
[(uh (τ σ G) Gx) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
;; (d) -- x does not occur in τ case
[(uh (x τ G) G_r boolean)
(uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
(where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
;; occurs check
[(uh (x τ G) Gx) ⊥ (where #t (in-vars-τ? x τ))]
;; no rules applied; try next equation, if any.
[(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
;; variable elimination
[(uh (x τ G) Gx)
(uh (eliminate-G x τ G) (x τ (eliminate-G x τ Gx)))])
(define-metafunction stlc
eliminate-G : x τ G -> G
@ -253,14 +242,6 @@ It runs until there are no more changes. The (a), (b),
[(in-vars-τ? x x) #t]
[(in-vars-τ? x y) #f])
(define-metafunction stlc
in-vars-G? : x G -> boolean
[(in-vars-G? x ·) #f]
[(in-vars-G? x (x τ G)) #t]
[(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ)
(∨ (in-vars-τ? x τ)
(in-vars-G? x G)))])
(define-metafunction stlc
apply-subst-τ : Gx τ -> τ
[(apply-subst-τ · τ) τ]

65
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt
View File

@ -170,56 +170,45 @@ bring that type back, recurring on the continuation.
(define-metafunction stlc
unify : τ τ -> Gx or ⊥
[(unify τ σ) (uh (τ σ ·) · #f)])
[(unify τ σ) (uh (τ σ ·) ·)])
#|
Algorithm copied from _An Efficient Unification Algorithm_ by
Alberto Martelli and Ugo Montanari (section 2).
http://www.nsl.com/misc/papers/martelli-montanari.pdf
This isn't the eponymous algorithm; it is an earlier one
in the paper that's simpler.
Algorithm copied from Chapter 8 in _Handbook of Automated Reasoning_:
Unification Theory by Franz Baader and Wayne Synder
http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf
The 'uh' function iterates over a set of equations applying the
rules from the paper, moving them from the first argument to
the second argument and tracking when something changes.
It runs until there are no more changes. The (a), (b),
(c), and (d) are the rule labels from the paper.
rules from the paper, building up the result substitution in G_r.
|#
(define-metafunction stlc
uh : G G boolean -> Gx or ⊥
[(uh · G #t) (uh G · #f)]
[(uh · G #f) G]
uh : G Gx -> Gx or ⊥
;; (a)
[(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
[(uh · Gx) Gx]
;; (b)
[(uh (x x G) G_r boolean) (uh G G_r #t)]
;; orient
[(uh (τ x G) Gx) (uh (x τ G) Gx) (where #t (not-var? τ))]
;; (c) -- term reduction
[(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
[(uh ((list τ) (list σ) G) G_r boolean) (uh (τ σ G) G_r #t)]
[(uh ((ref τ) (ref σ) G) G_r boolean) (uh (τ σ G) G_r #t)]
[(uh (int int G) G_r boolean) (uh G G_r #t)]
;; trivial (other cases are covered by decomposition rule)
[(uh (x x G) Gx) (uh G Gx)]
;; (c) -- failure
[(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
;; decomposition
[(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) Gx) (uh (τ_1 σ_1 (τ_2 σ_2 G)) Gx)]
[(uh ((list τ) (list σ) G) Gx) (uh (τ σ G) Gx)]
[(uh ((ref τ) (ref σ) G) Gx) (uh (τ σ G) Gx)]
[(uh (int int G) Gx) (uh G Gx)]
;; (d) -- x occurs in τ case
[(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars? x τ))]
;; symbol clash
[(uh (τ σ G) Gx) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
;; (d) -- x does not occur in τ case
[(uh (x τ G) G_r boolean)
(uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
(where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
;; occurs check
[(uh (x τ G) Gx) ⊥ (where #t (in-vars? x τ))]
;; no rules applied; try next equation, if any.
[(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
;; variable elimination
[(uh (x τ G) Gx)
(uh (eliminate-G x τ G) (x τ (eliminate-G x τ Gx)))])
(define-metafunction stlc
eliminate-G : x τ G -> G
@ -255,14 +244,6 @@ It runs until there are no more changes. The (a), (b),
[(in-vars-τ? x x) #t]
[(in-vars-τ? x y) #f])
(define-metafunction stlc
in-vars-G? : x G -> boolean
[(in-vars-G? x ·) #f]
[(in-vars-G? x (x τ G)) #t]
[(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ)
(∨ (in-vars-τ? x τ)
(in-vars-G? x G)))])
(define-metafunction stlc
apply-subst-τ : Gx τ -> τ
[(apply-subst-τ · τ) τ]

65
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt
View File

@ -168,56 +168,45 @@ bring that type back, recurring on the continuation.
(define-metafunction stlc
unify : τ τ -> Gx or ⊥
[(unify τ σ) (uh (τ σ ·) · #f)])
[(unify τ σ) (uh (τ σ ·) ·)])
#|
Algorithm copied from _An Efficient Unification Algorithm_ by
Alberto Martelli and Ugo Montanari (section 2).
http://www.nsl.com/misc/papers/martelli-montanari.pdf
This isn't the eponymous algorithm; it is an earlier one
in the paper that's simpler.
Algorithm copied from Chapter 8 in _Handbook of Automated Reasoning_:
Unification Theory by Franz Baader and Wayne Synder
http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf
The 'uh' function iterates over a set of equations applying the
rules from the paper, moving them from the first argument to
the second argument and tracking when something changes.
It runs until there are no more changes. The (a), (b),
(c), and (d) are the rule labels from the paper.
rules from the paper, building up the result substitution in G_r.
|#
(define-metafunction stlc
uh : G G boolean -> Gx or ⊥
[(uh · G #t) (uh G · #f)]
[(uh · G #f) G]
uh : G Gx -> Gx or ⊥
;; (a)
[(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
[(uh · Gx) Gx]
;; (b)
[(uh (x x G) G_r boolean) (uh G G_r #t)]
;; orient
[(uh (τ x G) Gx) (uh (x τ G) Gx) (where #t (not-var? τ))]
;; (c) -- term reduction
[(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
[(uh ((list τ) (list σ) G) G_r boolean) (uh (τ σ G) G_r #t)]
[(uh ((ref τ) (ref σ) G) G_r boolean) (uh (τ σ G) G_r #t)]
[(uh (int int G) G_r boolean) (uh G G_r #t)]
;; trivial (other cases are covered by decomposition rule)
[(uh (x x G) Gx) (uh G Gx)]
;; (c) -- failure
[(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
;; decomposition
[(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) Gx) (uh (τ_1 σ_1 (τ_2 σ_2 G)) Gx)]
[(uh ((list τ) (list σ) G) Gx) (uh (τ σ G) Gx)]
[(uh ((ref τ) (ref σ) G) Gx) (uh (τ σ G) Gx)]
[(uh (int int G) Gx) (uh G Gx)]
;; (d) -- x occurs in τ case
[(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
;; symbol clash
[(uh (τ σ G) Gx) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
;; (d) -- x does not occur in τ case
[(uh (x τ G) G_r boolean)
(uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
(where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
;; occurs check
[(uh (x τ G) Gx) ⊥ (where #t (in-vars-τ? x τ))]
;; no rules applied; try next equation, if any.
[(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
;; variable elimination
[(uh (x τ G) Gx)
(uh (eliminate-G x τ G) (x τ (eliminate-G x τ Gx)))])
(define-metafunction stlc
eliminate-G : x τ G -> G
@ -255,14 +244,6 @@ It runs until there are no more changes. The (a), (b),
[(in-vars-τ? x x) #t]
[(in-vars-τ? x y) #f])
(define-metafunction stlc
in-vars-G? : x G -> boolean
[(in-vars-G? x ·) #f]
[(in-vars-G? x (x τ G)) #t]
[(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ)
(∨ (in-vars-τ? x τ)
(in-vars-G? x G)))])
(define-metafunction stlc
apply-subst-τ : Gx τ -> τ
[(apply-subst-τ · τ) τ]

67
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt
View File

@ -168,56 +168,45 @@ bring that type back, recurring on the continuation.
(define-metafunction stlc
unify : τ τ -> Gx or ⊥
[(unify τ σ) (uh (τ σ ·) · #f)])
[(unify τ σ) (uh (τ σ ·) ·)])
#|
Algorithm copied from _An Efficient Unification Algorithm_ by
Alberto Martelli and Ugo Montanari (section 2).
http://www.nsl.com/misc/papers/martelli-montanari.pdf
This isn't the eponymous algorithm; it is an earlier one
in the paper that's simpler.
Algorithm copied from Chapter 8 in _Handbook of Automated Reasoning_:
Unification Theory by Franz Baader and Wayne Synder
http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf
The 'uh' function iterates over a set of equations applying the
rules from the paper, moving them from the first argument to
the second argument and tracking when something changes.
It runs until there are no more changes. The (a), (b),
(c), and (d) are the rule labels from the paper.
rules from the paper, building up the result substitution in G_r.
|#
(define-metafunction stlc
uh : G G boolean -> Gx or ⊥
[(uh · G #t) (uh G · #f)]
[(uh · G #f) G]
uh : G Gx -> Gx or ⊥
;; (a)
[(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
[(uh · Gx) Gx]
;; (b)
[(uh (x x G) G_r boolean) (uh G G_r #t)]
;; orient
[(uh (τ x G) Gx) (uh (x τ G) Gx) (where #t (not-var? τ))]
;; (c) -- term reduction
[(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
[(uh ((list τ) (list σ) G) G_r boolean) (uh (τ σ G) G_r #t)]
[(uh ((ref τ) (ref σ) G) G_r boolean) (uh (τ σ G) G_r #t)]
[(uh (int int G) G_r boolean) (uh G G_r #t)]
;; trivial (other cases are covered by decomposition rule)
[(uh (x x G) Gx) (uh G Gx)]
;; (c) -- failure
[(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
;; decomposition
[(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) Gx) (uh (τ_1 σ_1 (τ_2 σ_2 G)) Gx)]
[(uh ((list τ) (list σ) G) Gx) (uh (τ σ G) Gx)]
[(uh ((ref τ) (ref σ) G) Gx) (uh (τ σ G) Gx)]
[(uh (int int G) Gx) (uh G Gx)]
;; (d) -- x occurs in τ case
[(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
;; symbol clash
[(uh (τ σ G) Gx) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
;; (d) -- x does not occur in τ case
[(uh (x τ G) G_r boolean)
(uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
(where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
;; occurs check
[(uh (x τ G) Gx) ⊥ (where #t (in-vars-τ? x τ))]
;; no rules applied; try next equation, if any.
[(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
;; variable elimination
[(uh (x τ G) Gx)
(uh (eliminate-G x τ G) (x τ (eliminate-G x τ Gx)))])
(define-metafunction stlc
eliminate-G : x τ G -> G
@ -253,14 +242,6 @@ It runs until there are no more changes. The (a), (b),
[(in-vars-τ? x x) #t]
[(in-vars-τ? x y) #f])
(define-metafunction stlc
in-vars-G? : x G -> boolean
[(in-vars-G? x ·) #f]
[(in-vars-G? x (x τ G)) #t]
[(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ)
(∨ (in-vars-τ? x τ)
(in-vars-G? x G)))])
(define-metafunction stlc
apply-subst-τ : Gx τ -> τ
[(apply-subst-τ · τ) τ]
@ -571,5 +552,5 @@ reachable from the given term.
(or (equal? red-t "error")
(zero? n) (loop red-t (- n 1))))))))))))))
(define small-counter-example (term ((λ x x) 1)))
(define small-counter-example (term (λ x (x x))))
(test-equal (check small-counter-example) #f)

65
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt
View File

@ -169,56 +169,45 @@ bring that type back, recurring on the continuation.
(define-metafunction stlc
unify : τ τ -> Gx or ⊥
[(unify τ σ) (uh (τ σ ·) · #f)])
[(unify τ σ) (uh (τ σ ·) ·)])
#|
Algorithm copied from _An Efficient Unification Algorithm_ by
Alberto Martelli and Ugo Montanari (section 2).
http://www.nsl.com/misc/papers/martelli-montanari.pdf
This isn't the eponymous algorithm; it is an earlier one
in the paper that's simpler.
Algorithm copied from Chapter 8 in _Handbook of Automated Reasoning_:
Unification Theory by Franz Baader and Wayne Synder
http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf
The 'uh' function iterates over a set of equations applying the
rules from the paper, moving them from the first argument to
the second argument and tracking when something changes.
It runs until there are no more changes. The (a), (b),
(c), and (d) are the rule labels from the paper.
rules from the paper, building up the result substitution in G_r.
|#
(define-metafunction stlc
uh : G G boolean -> Gx or ⊥
[(uh · G #t) (uh G · #f)]
[(uh · G #f) G]
uh : G Gx -> Gx or ⊥
;; (a)
[(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
[(uh · Gx) Gx]
;; (b)
[(uh (x x G) G_r boolean) (uh G G_r #t)]
;; orient
[(uh (τ x G) Gx) (uh (x τ G) Gx) (where #t (not-var? τ))]
;; (c) -- term reduction
[(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
[(uh ((list τ) (list σ) G) G_r boolean) (uh (τ σ G) G_r #t)]
[(uh ((ref τ) (ref σ) G) G_r boolean) (uh (τ σ G) G_r #t)]
[(uh (int int G) G_r boolean) (uh G G_r #t)]
;; trivial (other cases are covered by decomposition rule)
[(uh (x x G) Gx) (uh G Gx)]
;; (c) -- failure
[(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
;; decomposition
[(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) Gx) (uh (τ_1 σ_1 (τ_2 σ_2 G)) Gx)]
[(uh ((list τ) (list σ) G) Gx) (uh (τ σ G) Gx)]
[(uh ((ref τ) (ref σ) G) Gx) (uh (τ σ G) Gx)]
[(uh (int int G) Gx) (uh G Gx)]
;; (d) -- x occurs in τ case
[(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
;; symbol clash
[(uh (τ σ G) Gx) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
;; (d) -- x does not occur in τ case
[(uh (x τ G) G_r boolean)
(uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
(where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
;; occurs check
[(uh (x τ G) Gx) ⊥ (where #t (in-vars-τ? x τ))]
;; no rules applied; try next equation, if any.
[(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
;; variable elimination
[(uh (x τ G) Gx)
(uh (eliminate-G x τ G) (x τ (eliminate-G x τ Gx)))])
(define-metafunction stlc
eliminate-G : x τ G -> G
@ -254,14 +243,6 @@ It runs until there are no more changes. The (a), (b),
[(in-vars-τ? x x) #t]
[(in-vars-τ? x y) #f])
(define-metafunction stlc
in-vars-G? : x G -> boolean
[(in-vars-G? x ·) #f]
[(in-vars-G? x (x τ G)) #t]
[(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ)
(∨ (in-vars-τ? x τ)
(in-vars-G? x G)))])
(define-metafunction stlc
apply-subst-τ : Gx τ -> τ
[(apply-subst-τ · τ) τ]

65
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt
View File

@ -168,56 +168,45 @@ bring that type back, recurring on the continuation.
(define-metafunction stlc
unify : τ τ -> Gx or ⊥
[(unify τ σ) (uh (τ σ ·) · #f)])
[(unify τ σ) (uh (τ σ ·) ·)])
#|
Algorithm copied from _An Efficient Unification Algorithm_ by
Alberto Martelli and Ugo Montanari (section 2).
http://www.nsl.com/misc/papers/martelli-montanari.pdf
This isn't the eponymous algorithm; it is an earlier one
in the paper that's simpler.
Algorithm copied from Chapter 8 in _Handbook of Automated Reasoning_:
Unification Theory by Franz Baader and Wayne Synder
http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf
The 'uh' function iterates over a set of equations applying the
rules from the paper, moving them from the first argument to
the second argument and tracking when something changes.
It runs until there are no more changes. The (a), (b),
(c), and (d) are the rule labels from the paper.
rules from the paper, building up the result substitution in G_r.
|#
(define-metafunction stlc
uh : G G boolean -> Gx or ⊥
[(uh · G #t) (uh G · #f)]
[(uh · G #f) G]
uh : G Gx -> Gx or ⊥
;; (a)
[(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
[(uh · Gx) Gx]
;; (b)
[(uh (x x G) G_r boolean) (uh G G_r #t)]
;; orient
[(uh (τ x G) Gx) (uh (x τ G) Gx) (where #t (not-var? τ))]
;; (c) -- term reduction
[(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
[(uh ((list τ) (list σ) G) G_r boolean) (uh (τ σ G) G_r #t)]
[(uh ((ref τ) (ref σ) G) G_r boolean) (uh (τ σ G) G_r #t)]
[(uh (int int G) G_r boolean) (uh G G_r #t)]
;; trivial (other cases are covered by decomposition rule)
[(uh (x x G) Gx) (uh G Gx)]
;; (c) -- failure
[(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
;; decomposition
[(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) Gx) (uh (τ_1 σ_1 (τ_2 σ_2 G)) Gx)]
[(uh ((list τ) (list σ) G) Gx) (uh (τ σ G) Gx)]
[(uh ((ref τ) (ref σ) G) Gx) (uh (τ σ G) Gx)]
[(uh (int int G) Gx) (uh G Gx)]
;; (d) -- x occurs in τ case
[(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
;; symbol clash
[(uh (τ σ G) Gx) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
;; (d) -- x does not occur in τ case
[(uh (x τ G) G_r boolean)
(uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
(where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
;; occurs check
[(uh (x τ G) Gx) ⊥ (where #t (in-vars-τ? x τ))]
;; no rules applied; try next equation, if any.
[(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
;; variable elimination
[(uh (x τ G) Gx)
(uh (eliminate-G x τ G) (x τ (eliminate-G x τ Gx)))])
(define-metafunction stlc
eliminate-G : x τ G -> G
@ -253,14 +242,6 @@ It runs until there are no more changes. The (a), (b),
[(in-vars-τ? x x) #t]
[(in-vars-τ? x y) #f])
(define-metafunction stlc
in-vars-G? : x G -> boolean
[(in-vars-G? x ·) #f]
[(in-vars-G? x (x τ G)) #t]
[(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ)
(∨ (in-vars-τ? x τ)
(in-vars-G? x G)))])
(define-metafunction stlc
apply-subst-τ : Gx τ -> τ
[(apply-subst-τ · τ) τ]

8
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/tests.rkt
View File

@ -97,7 +97,7 @@
(test-equal (term (unify (list int) (list int)))
(term ·))
(test-equal (term (unify (int → x) (y → (list int))))
(term (y int (x (list int) ·))))
(term (x (list int) (y int ·))))
(test-equal (term (unify (int → x) (x → (list int))))
(term ⊥))
(test-equal (term (unify (x → (y → x))
@ -105,13 +105,13 @@
(term ⊥))
(test-equal (term (unify (x → (y → x))
(int → ((list int) → z))))
(term (x int (y (list int) (z int ·)))))
(term (z int (y (list int) (x int ·)))))
(test-equal (term (unify (x → (y → z))
(int → ((list int) → x))))
(term (x int (y (list int) (z int ·)))))
(term (z int (y (list int) (x int ·)))))
(test-equal (term (unify (x → (y → z))
(y → (z → int))))
(term (x int (y int (z int ·)))))
(term (z int (y int (x int ·)))))
(test-equal (term (unify x (x → y)))
(term ⊥))