Circular language

circular.rkt

#lang racket
(require redex/reduction-semantics)

(define-language C
  (CON X
       nat?
       (or/c CON CON)
       (rec/c X CON)
       (cons/c CON CON)
       (CON -> CON))
  (X variable-not-otherwise-mentioned)
  
  (FLAT (side-condition (name x CON)
                        ;; That's right, we're defining the language
                        ;; in terms of a metafunction for the language
                        (term (flat? x)))))

(define-metafunction C
  flat? : CON -> #t or #f
  [(flat? nat?) #t]
  [(flat? (or/c CON_1 CON_2))
   ,(and (term (flat? CON_1))
         (term (flat? CON_2)))]
  [(flat? (rec/c X CON))
   (flat? (subst (subst nat? X CON) X CON))]
  [(flat? (cons/c CON_1 CON_2))
   ,(and (term (flat? CON_1))
         (term (flat? CON_2)))]
  [(flat? (CON_1 -> CON_2)) #f])

(define-metafunction C
  subst : CON X CON -> CON
  [(subst CON X nat?) nat?] 
  [(subst CON X X) CON]
  [(subst CON X X_1) X_1]
  [(subst CON X (or/c CON_1 CON_2))
   (or/c (subst CON X CON_1)
         (subst CON X CON_2))]
  [(subst CON X (rec/c X CON_1)) (rec/c X CON_1)]
  [(subst CON X (rec/c X_1 CON_1)) (rec/c X_1 (subst CON X CON_1))]
  [(subst CON X (cons/c CON_1 CON_2))
   (cons/c (subst CON X CON_1)
           (subst CON X CON_2))]
  [(subst CON X (CON_1 -> CON_2))
   ((subst CON X CON_1) -> (subst CON X CON_2))])

(define f? (redex-match C FLAT))
(define h? (negate f?))

(test-predicate h? '(rec/c X (nat? -> nat?)))
(test-predicate h? '(rec/c X (nat? -> X)))
(test-predicate h? '(rec/c X (X -> X)))
(test-predicate h? '(rec/c X (cons/c X (X -> X))))
(test-predicate f? '(rec/c X (or/c (cons/c X X) (cons/c X X))))
(test-predicate f? '(rec/c X (rec/c Y (or/c (cons/c X Y) (cons/c Y X)))))