[plt-scheme] Redex generating terms

From: David Van Horn (dvanhorn at ccs.neu.edu)
Date: Fri Apr 2 18:09:35 EDT 2010

Given the following definitions:

#lang scheme
(require redex)

(define-language L
   [a (a ...)])

(define (depth x)
   (cond [(cons? x) (add1 (apply max (map depth x)))]
         [else 0]))

I'm surprised the following can produce a number greater than 5:

(for/fold ([n 0])
   ([i (in-range 100)])
   (max n (depth (generate-term L a 5))))

But the height of the generated terms can be far larger than 5, and 
consequently checking even trivial properties a small number of times is 
infeasible.  For example, this consumes all available memory on my machine:

(redex-check L a ((lambda (x) #t) (term a))
              #:attempts 30)

Is this a bug in Redex, or am I misunderstanding the purpose of the size 
argument for generate-term?  And how can I work around this to test 
properties of this language?

Actually, I was able to answer my own question.  Everything works fine 
with the equivalent grammar:

(define-language L
   [a () (a ...)])

Is this intended or is there a bug in term generation?


Posted on the users mailing list.