Update apply-reduction-relation* to be sensitive to alpha-equivalence

[howell]

Also add an immutable alpha hash constructor and update hashes in
the gui to use the form provided by binding-forms.rkt

Fixes #96

[wilbowma]

I just ran the microbenchmarks in redex-test/redex/tests/binding-performance-test.rkt with this branch. The eval tests seem to run a fair bit slower. I also tried replacing the judgment form cache with make-alpha-hash, and experienced similar slow downs.

[wilbowma]

For reference, measurements here: https://gist.github.com/wilbowma/99bcbc4c97f2b970091b9f43754782b2

[wilbowma]

I pushed a fork of this branch to https://github.com/wilbowma/redex/tree/alpha-caches, which includes using an alpha hash for judgment forms. The judgment form slow downs are in fact much more significant. Some factors over 10x

[rfindler]

Are you measuring this slowdown on languages that have binding forms specified or on ones that don't?

[wilbowma]

.. That's a good question. I'll have to take a look at the tests.

[wilbowma]

Both with and without judgment forms are slower. If you look at the logs I posted in the above gist, compare the last test in baseline.log and judgment-cache.log. complex-ho is run in both stlc+lists with and without binding forms. Both are significantly slower.

[rfindler]

It shouldn't be hard to avoid the overhead for judgment forms that are on languages without binding forms. (Just check and use a regular hash.) For the others, well, I am not sure there is an easy solution. Robby

…

On Sat, May 27, 2017 at 11:08 AM William J. Bowman ***@***.***> wrote: Both with and without judgment forms are slower. If you look at the logs I posted in the above gist, compare the last test in baseline.log and judgment-cache.log. complex-ho is run in both stlc+lists with and without binding forms. Both are significantly slower. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#102 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAYWsAjnwZgfMJw3ty3Mcx6mYo7ifcXhks5r-Ep6gaJpZM4Nm7YZ> .

[wilbowma]

Eek. I was hoping this would help performance. I've got some pathological cases where variables get freshened tens of thousands of times, and they seem to defeat the cache.

[rfindler]

Performance bottlenecks in redex can be hard to spot. I can take a look (no today sadly) if you supply some code that seems unreasonably slow. Robby

…

On Sat, May 27, 2017 at 11:22 AM William J. Bowman ***@***.***> wrote: Eek. I was hoping this would *help* performance. I've got some pathological cases where variables get freshened tens of thousands of times, and they seem to defeat the cache. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#102 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAYWsOkhigISrBAPSnUrE86_DK0Sg2-Cks5r-E3ggaJpZM4Nm7YZ> .

[wilbowma]

I'll try to get you some code later. Will my CIC model do? I know I can reproduce the behavior there, but it's awfully complex.

[rfindler]

Yes that is fine. Robby

…

On Sat, May 27, 2017 at 11:59 AM William J. Bowman ***@***.***> wrote: I'll try to get you some code later. Will my CIC model do? I know I can reproduce the behavior there, but it's awfully complex. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#102 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAYWsNdoa6JaMMtlP8AfjHgaBO594hfgks5r-FZmgaJpZM4Nm7YZ> .

[wilbowma]

I'm going to move this discussion to a separate PR. I tested @howell's PR against my extensive development and do get performance improvements (nearly 2x!). Maybe my changes to judgments are broken.

[wilbowma]

@howell, looking over this PR, it appears that some caches are still hashes. E.g., line 1708 in reduction-semantics.rkt, and line 1719

[wilbowma]

Looks like those are the metafunction caches, and performance dies similar to judgment forms when I change them.

[wilbowma]

As the make-*-custom-hash interface is deprecated, perhaps this is a good time to redefine these using define-custom-hash-types.

[howell]

Ah, I missed that these were deprecated.

The define-custom-hash-types interface is a bit awkward for this use case. The functions for computing equality and hashing need to close over the language binding table and match pattern, which aren't provided until we actually make a hash. So the result would look like

(define (make-α-hash language-bf-table match-pattern)
  (define-custom-hash-types this-lang-α-hash
    (λ (x y) (α-equal? language-bf-table match-pattern x y))
    (λ (x) (α-equal-hash-code language-bf-table match-pattern x))
    (λ (x) (α-equal-secondary-hash-code language-bf-table match-pattern x)))
  (make-mutable-this-lang-α-hash))

It's a bit awkward, but maybe still better than using a deprecated version?

[wilbowma]

Except it will be worse, since define-custom-hash-types defines 7 names. You need to abstract all 7 definitions over the bf-table and match-pattern.. it's a bit gross.
Makes me want a macro that is like splicing-let, but instead of splicing in definitions, it .. splices in additional arguments? Essentially, allows eta expanding a bunch of definitions with respect to a set of arguments ..?

(splicing-lambda (x y)
  (define-values (f g h) (values (lambda (z) x) (lambda (z) y) (lambda (z) z))))
(check-equal? (f 1 2 3) 1)
(check-equal? (g 1 2 3) 2)
(check-equal? (h 1 2 3) 3)

[wilbowma]

1. I found a bug in this; see https://github.com/wilbowma/redex/tree/pr-102
2. Can we merge this? I'm running into massive performance problems again and had to manually install this patch.

[wilbowma]

(By the way, the bug I found suggests there are no tests for apply-reduction-relation* using an IO judgment form in the test suite)

[rfindler]

In tl-judgment-form.rkt, these are tests of IO-judgment-forms being passed to apply-reduction-relation, line 518:

(let ()
  (define-judgment-form empty-language
    #:mode (J O I)
    [------------- "smaller"
     (J any (any))]
    
    [----------------- "bigger"
     (J ((any any)) any)])
  
  (test (judgment-form? J) #t)
  (test (IO-judgment-form? J) #t)
  (test (apply-reduction-relation J '(2))
        (judgment-holds (J any (2)) any))
  (test (apply set (apply-reduction-relation/tag-with-names J '(3)))
        (set (list "smaller" 3)
             (list "bigger" '(((3) (3)))))))

[rfindler]

Rereading the conversation I'm not really clear what is going on here. Looking at the commit diff, it seems like the changes are good ones, however, so I'll go ahead and merge it. If there is something else that needs doing, please let me know.

[wilbowma]

Well, the early conversion was a bit of topic and moved to #103.
This PR, except for the bug I fixed in https://github.com/wilbowma/redex/tree/pr-102, looks good to me, and really helps performance on some of my models. There's one minor issue: it's using a deprecated inference for creating a custom hash.

[rfindler]

That part seems to already be in redex. I'll work thru the diff and push what was clearly intended.

[rfindler]

Thanks for bringing this back to my attention. I took the liberty of putting your name on the revised commit, @howell .

[wilbowma]

Huzzah! Thanks!