[racket] Redex: exponential runtime with certain judgments

I've pushed a fix for the specific issue in this program but, in
general, there is a problem here that Redex can't solve on it's own.

The issue is that the judgment-form you have has more than one way to
establish the same fact and that ambiguity can have exponential
blowup.

Here's a simple example of the issue in a case where Redex is still
going to be slow.

#lang racket
(require redex)

(define-language L)

(define-judgment-form L
  #:mode (K I)
  [(K (any_2 ...))
   -------------- one
   (K (natural_1 any_2 ...))]
  [(K (any_2 ...))
   -------------- two
   (K (number_1 any_2 ...))])

(time (judgment-holds (K (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14))))
(time (judgment-holds (K (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))))

In this case, each smaller list has two options and so we get roughly
2^14 or 2^15 different ways to (fail to) make this derivation, and
they take a while to go thru.

This next example is closer to how your code actually does the
multiple derivations -- it actually builds them inside an ellipsis and
in a way that Redex has a chance to notice that it's got the same
result twice:

;; this one exists to have an ellipsis
(define-judgment-form L
  #:mode (J I)
  [(D any_x) ...
   --------------
   (J (any_x ...))])

;; this one exists to have redundancy
(define-judgment-form L
  #:mode (D I)
  [----------- nat
   (D natural)]
  [----------- num
   (D number)])

(time (judgment-holds (J (0 1 2 3 4 5 6 7 8 9 10 11 12 13))))
(time (judgment-holds (J (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14))))

I've improved this case (but the related case where you use
show-derivations instead of judgment-holds will still be slow because
there are legitimately a LOT of answers that Redex has to actually
construct in that case).

Robby

On Fri, Jul 25, 2014 at 1:10 AM,  <dfeltey at ccs.neu.edu> wrote:
> I'm attaching a model of the simply typed lambda calculus which demonstrates the issue. The file includes a language definition, the necessary judgment forms, and a few macros for generating and timing programs of a given size.
>
> I hope this helps.
> Thanks
> Dan
>
>
>
> ----- Original Message -----
> From: "Robby Findler" <robby at eecs.northwestern.edu>
> To: "Daniel Feltey" <dfeltey at ccs.neu.edu>
> Cc: "Racket Users" <users at racket-lang.org>
> Sent: Friday, July 25, 2014 1:16:10 AM GMT -05:00 US/Canada Eastern
> Subject: Re: [racket] Redex: exponential runtime with certain judgments
>
> It's hard for me to see what exactly is going on -- would you have the
> time to make a simple form of your judgment form and an input that
> demonstrates the issue?
>
> Thanks,
> Robby
>
> On Thu, Jul 24, 2014 at 11:53 PM, Daniel Feltey <dfeltey at ccs.neu.edu> wrote:
>> I've been implementing a type system with subtyping using Redex's judgment forms and noticed that checking whether my typing judgment would hold was taking longer than seemed reasonable (5 - 10 minutes in some cases).
>>
>> Ultimately I tracked the bug down to a clause in the subtyping judgment that had the form:
>>
>> (< tau tau)
>>
>> Where tau is the grammar term that could represent any type in my language, and both uses of tau are in input positions. Removing this rule brought down the 10 minute runtime mentioned above to under half a second.
>>
>> Is this behavior expected in the case of judgment-form clauses similar to the above, it seemed natural to me to include a rule like this in my subtyping judgment and I definitely didn't expect this to be the main reason for my model performing so poorly.
>>
>> Thanks
>> Dan
>> ____________________
>>   Racket Users list:
>>   http://lists.racket-lang.org/users