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

adjust let poly bug #4 so that the check procedure catches

Browse Source 
errors and treats them as failing to satisfy the property

This bug disables the occurs check and, thanks to the now
tighter contracts on the uh function, this can cause it to
signal an error. Here's the example:

  (term (unify (x → (list int)) ((list x) → x)))

found by in-order enumeration (so naturally it had ||
variables in it, not 'x's originally)

This leads to this trace in the uh function:

  (uh ((x → (list int)) ((list x) → x) ·) ·)
  (uh (x (list x) ((list int) x ·))       ·)
  (uh ((list int) (list x) ·)             (x (list x) ·))
  (uh (int x ·)                           (x (list x) ·))
  (uh (x int ·)                           (x (list x) ·))
  (uh ·                                   (x int (int (list int) ·)))

whereby the third step sets up a problem (that's where the
occurs check should have aborted the program) but instead, a
few steps later when we get a substitution for 'x', it
causes the second argument to not have the form of
variables-for-types substitution.

I don't think this can happen when the occurs check is in place
because the variable elimination step makes sure that we don't
set ourselves up to change the domain of anything in the second
argument to 'uh' (except possibly when the occurs check fails,
of course).

Here's an example that shows this:

 (unify (q → q) (y → int)))
 (uh ((q → q) (y → int) ·) ·)
 (uh (q y (q int ·))       ·)
 (uh (y int ·)             (q y ·))
 (uh ·                     (y int (q int ·)))

In the second to last step we don't have (q int ·), we have
(y int ·) because the variable elimination step changes the
q to a y.
This commit is contained in:
Robby Findler 2014-04-02 07:26:14 -05:00
parent ec77c70b79
commit b87ebbfe8f
2 changed files with 40 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -8,7 +8,33 @@
< [(uh (x τ G) Gx) ⊥ (where #t (in-vars-τ? x τ))]
---
> [(uh (x τ G) Gx) ⊥ (where #t (in-vars? x τ))]
552a555,557
541,552c543,558
< (let ([t-type (type-check M)])
< (implies
< t-type
< (let loop ([Σ+M `(· ,M)] [n 100])
< (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
< (and (consistent-with? t-type new-type)
< (or (v? (list-ref Σ+M 1))
< (let ([red-res (apply-reduction-relation red Σ+M)])
< (and (= (length red-res) 1)
< (let ([red-t (car red-res)])
< (or (equal? red-t "error")
< (zero? n) (loop red-t (- n 1)))))))))))))
---
> (with-handlers ([exn:fail? (λ (x) #f)])
> (let ([t-type (type-check M)])
> (implies
> t-type
> (let loop ([Σ+M `(· ,M)] [n 100])
> (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0)))
> (and (consistent-with? t-type new-type)
> (or (v? (list-ref Σ+M 1))
> (let ([red-res (apply-reduction-relation red Σ+M)])
> (and (= (length red-res) 1)
> (let ([red-t (car red-res)])
> (or (equal? red-t "error")
> (zero? n) (loop red-t (- n 1))))))))))))))
>
> (define small-counter-example (term ((λ x (x x)) hd)))
> (test-equal (check small-counter-example) #f)

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

@ -540,6 +540,7 @@ reachable from the given term.
(define (check M)
(or (not M)
(with-handlers ([exn:fail? (λ (x) #f)])
(let ([t-type (type-check M)])
(implies
t-type
@ -551,7 +552,7 @@ reachable from the given term.
(and (= (length red-res) 1)
(let ([red-t (car red-res)])
(or (equal? red-t "error")
(zero? n) (loop red-t (- n 1)))))))))))))
(zero? n) (loop red-t (- n 1))))))))))))))
(define small-counter-example (term ((λ x (x x)) hd)))
(test-equal (check small-counter-example) #f)