check-redundancy and the O(n^n) bubblesort

[MichaelBurge]

The following test code demonstrates a common issue.

#lang racket

(require redex/reduction-semantics)

(check-redundancy #t)

(define-language L
  [ xs ::= (n ...) ]
  [ n ::= natural ]
  )

(define-metafunction L
  bubblesort : xs -> xs
  [(bubblesort (n_1 ... n_2 n_3 n_4 ...))
   (bubblesort (n_1 ... n_3 n_2 n_4 ...))
   (side-condition (< (term n_2) (term n_3)))
   ]
  [(bubblesort xs) xs]
  )

(define (shuffle xs)
  (sort xs < #:key (λ (x) (random)) #:cache-keys? #t))


(define xs (shuffle (stream->list (in-range 100))))

(define-syntax-rule (time f)
  (begin
    (define t0 (current-seconds))
    (println f)
    (println (- (current-seconds) t0))
    ))

(for ([ i (in-range 100) ])
  (time (term (bubblesort ,(take xs i)))))

The bubblesort metafunction has an ambiguous pattern match. So redex will evaluate all possible normalization paths and check that they return the same result, which is O(n^(n^2))

The check-redundancy parameter is supposed to catch ambiguous matches, but I've never gotten any output from it.

Additionally, many metafunctions - such as AST simplifiers or bubblesorts - are expected to reduce to the same result no matter what order the pattern matches are taken in. Is there a way to commit to the first successful match, which in this example would reduce the runtime to O(n^3)?

[MichaelBurge]

The bubblesort example completes after making this change.

https://github.com/racket/redex/blob/master/redex-lib/redex/private/reduction-semantics.rkt#L1883

(unless (null? anss)
  (hash-set! ht (first anss) #t))
;(for-each (λ (ans) (hash-set! ht ans #t)) anss)

You could reduce it to O(n^2) if redex had a "resumable pattern-match": After swapping a pair of elements, the pattern-match could pick up where it left off in the new term rather than starting at the beginning. I think it would also greatly improve the performance of a "greedy" apply-reduction-relation*, since it still calculates each reduction O(n) times.