Tail recursion in the FYFF model

gistfile1.rkt

#lang racket

(require redex
         redex/examples/delim-cont/grammar
         redex/examples/delim-cont/meta
         redex/examples/delim-cont/reduce)

;; nullary Z combinator
(define Z
  (term (λ (f)
          ((λ (x) (f (λ () (x x))))
           (λ (x) (f (λ () (x x))))))))

;; unary Z combinator
(define Z1
   (term (λ (f)
          ((λ (x) (f (λ (v) ((x x) v))))
           (λ (x) (f (λ (v) ((x x) v))))))))

;; recursively install handlers
(define default-handler
  (term (,Z1 (λ (f) (λ (th) (% 0 (th) f))))))

;; not safe for space due to repeated prompt installation
(traces
 :->
 (term (<>
        () []
        (,Z (λ (f)
              (%
               0
               (call/comp
                (λ (k) (abort 0 (λ () (f))))
                0)
               ,default-handler))))))