[racket] Checking infinite loops

From: Joe Marshall (jmarshall at alum.mit.edu)
Date: Mon Oct 4 17:15:09 EDT 2010

On Mon, Oct 4, 2010 at 8:56 AM, Patrick Li <patrickli.2001 at gmail.com> wrote:
> So this seems rather positive. Through some clever search algorithms, or
> heuristics, we can have a infinite-loop checker that works well enough in
> practice.

Um, no.  You have to restrict the problem space, too.

For fun, here is a little program that may or may not have an infinite loop
in it:

(define (kernel s i)
  (list (not (car s))
        (if (car s)
            (cadr s)
            (cons i (cadr s)))
        (cons 'y (cons i (cons 'z (caddr s))))))

(define k0 '(t () (x)))

(define (mystery list)
  (let ((result (fold-left kernel k0 list)))
    (cond ((null? (cadr result)) #t)
          ((car result) (mystery (cadr result)))
          (else (mystery (caddr result))))))

Your task is to:
  1)  Show that an infinite loop is possible.   or
  2)  Show that an infinite loop is impossible.  or
  3)  Show that your clever search algorithms and heuristics
       would never encounter this kind of program (or one more complex)
       in practice.


Posted on the users mailing list.