; ordinals.scm
; 93-02-06

(define (CNF ord)
  (cond ((null? ord) ord)
        ((non-eps-form? ord)
         (let ((lexp (CNF (non-eps-form-to-lexp ord)))
               (rest (CNF (non-eps-form-to-rest ord))))
           (cond ((null? rest)
                  (if (cap-omega? lexp) lexp
                      (if (theta-form? lexp) lexp
                          (cons-non-eps lexp rest))))
                 ((non-eps-form? rest)
                  (let ((lexp1 (non-eps-form-to-lexp rest))
                        (rest1 (non-eps-form-to-rest rest)))
                    (if (less? lexp lexp1) rest
                        (cons-non-eps lexp rest))))
                 ((or (cap-omega? rest) (theta-form? rest))
                  (if (less? lexp rest) rest
                      (cons-non-eps lexp rest)))
                 (else (error "not an ordinal" rest)))))
        ((cap-omega? ord) ord)
        ((theta-form? ord) (cons-theta (CNF (theta-form-to-arg ord))))))

(define (less? CNF1 CNF2)
  (cond ((null? CNF1)
         (cond ((null? CNF2) #f)
               ((non-eps-form? CNF2) #t)
               ((cap-omega? CNF2) #t)
               ((theta-form? CNF2) #t)
               (else (error "not an ordinal" CNF2))))
        ((non-eps-form? CNF1)
         (let ((lexp1 (non-eps-form-to-lexp CNF1))
               (rest1 (non-eps-form-to-rest CNF1)))
           (cond ((null? CNF2) #f)
                 ((non-eps-form? CNF2)
                  (let ((lexp2 (non-eps-form-to-lexp CNF2))
                        (rest2 (non-eps-form-to-rest CNF2)))
                    (if (equal? lexp1 lexp2) (less? rest1 rest2)
                        (if (less? lexp1 lexp2) #t
                            (if (less? lexp2 lexp1) #f)))))
                 ((cap-omega? CNF2) (less? lexp1 CNF2))
                 ((theta-form? CNF2) (less? lexp1 CNF2))
                 (else (error "not an ordinal" CNF2)))))
        ((cap-omega? CNF1)
         (cond ((null? CNF2) #f)
               ((non-eps-form? CNF2)
                (less? CNF1 (non-eps-form-to-lexp CNF2)))
               ((cap-omega? CNF2) #f)
               ((theta-form? CNF2) #f)
               (else (error "not an ordinal" CNF2))))
        ((theta-form? CNF1)
         (cond ((null? CNF2) #f)
               ((non-eps-form? CNF2)
                (less? CNF1 (non-eps-form-to-lexp CNF2)))
               ((cap-omega? CNF2) #t)
               ((theta-form? CNF2) 
                (let ((arg1 (theta-form-to-arg CNF1))
                      (arg2 (theta-form-to-arg CNF2)))
                  (cond ((equal? arg1 arg2) #f)
                        ((less? arg1 arg2) (less? (star arg1) CNF2))
                        ((less? arg2 arg1)
                         (let ((star2 (star arg2)))
                           (or (equal? CNF1 star2) (less? CNF1 star2)))))))
               (else (error "not an ordinal" CNF2))))))

(define (E-Omega CNF)
  (cond ((null? CNF) '())
        ((non-eps-form? CNF)
         (append (E-Omega (non-eps-form-to-lexp CNF))
                 (E-Omega (non-eps-form-to-rest CNF))))
        ((cap-omega? CNF) (list CNF))
        ((theta-form? CNF) (list CNF))
        (else (error "not a CNF" CNF))))

(define (ordmax CNFs)
  (if (null? CNFs) '()
      (let ((prev (ordmax (cdr CNFs)))
            (first (car CNFs)))
        (if (less? first prev) prev first))))

(define (star CNF) (ordmax (E-Omega CNF)))

(define (non-eps-form? x)
  (and (pair? x) (not (eq? 'theta (car x)))))

(define non-eps-form-to-lexp car)
(define non-eps-form-to-rest cdr)

(define (cons-non-eps ord1 ord2) (cons ord1 ord2))

(define (cap-omega? x) (eq? 'cap-omega x))

(define (theta-form? x) 
  (and (pair? x) (eq? 'theta (car x)) (pair? (cdr x))))

(define theta-form-to-arg cadr)

(define (cons-theta x) (list 'theta x))

(define (plus CNF1 CNF2)
  (cond ((null? CNF1) CNF2)
        ((null? CNF2) CNF1)
        ((non-eps-form? CNF1) 
         (let ((lexp1 (non-eps-form-to-lexp CNF1))
               (rest1 (non-eps-form-to-rest CNF1)))
           (if (null? rest1)
               (cond ((non-eps-form? CNF2)
                      (let ((lexp2 (non-eps-form-to-lexp CNF2)))
                        (if (less? lexp1 lexp2) CNF2
                            (cons-non-eps lexp1 CNF2))))
                     ((or (cap-omega? CNF2) (theta-form? CNF2))
                      (if (less? lexp1 CNF2) CNF2
                          (cons-non-eps lexp1 CNF2)))
                     (else (error "not a CNF" CNF2)))
               (plus (cons-non-eps lexp1 null) (plus rest1 CNF2)))))
        ((or (cap-omega? CNF1) (theta-form? CNF1))
         (cond ((non-eps-form? CNF2)
                (let ((lexp2 (non-eps-form-to-lexp CNF2)))
                  (if (less? CNF1 lexp2) CNF2
                      (cons-non-eps CNF1 CNF2))))
               ((or (cap-omega? CNF2) (theta-form? CNF2))
                (if (less? CNF1 CNF2) CNF2
                    (cons-non-eps CNF1 CNF2)))
               (else (error "not a CNF" CNF2))))
        (else (error "not a CNF" CNF1))))

(define (times CNF1 CNF2)
  (cond ((null? CNF1) null)
        ((null? CNF2) null)
        ((non-eps-form? CNF2)
         (let ((lexp2 (non-eps-form-to-lexp CNF2))
               (rest2 (non-eps-form-to-rest CNF2)))
           (if (null? rest2)
               (if (null? lexp2) CNF1
                   (cond ((non-eps-form? CNF1)
                          (let ((lexp1 (non-eps-form-to-lexp CNF1)))
                             (cons-non-eps (plus lexp1 lexp2) null)))
                         ((or (cap-omega? CNF1) (theta-form? CNF1))
                          (cons-non-eps (plus CNF1 lexp2) null))
                         (else (error "not a CNF" CNF1))))
               (plus (times CNF1 (cons-non-eps lexp2 null))
                     (times CNF1 rest2)))))
        ((or (cap-omega? CNF2) (theta-form? CNF2))
         (cond ((non-eps-form? CNF1)
                (let ((lexp1 (non-eps-form-to-lexp CNF1)))
                  (cons-non-eps (plus lexp1 CNF2) null)))
               ((or (cap-omega? CNF1) (theta-form? CNF1))
                (cons-non-eps (plus CNF1 CNF2) null))
               (else (error "not a CNF" CNF1))))
        (else (error "not a CNF" CNF2))))

; Beispielsordinalzahlen:

(define null '())
(define eins (cons-non-eps null null))
(define zwei (cons-non-eps null eins))
(define drei (cons-non-eps null zwei))
(define vier (cons-non-eps null drei))
(define omega (cons-non-eps eins null))
(define omega-square (cons-non-eps zwei null))
(define epsilon0 (cons-theta null))