(module kappa mzscheme
        
 ; Lambda calculus with lazy-order evaluation
 ;
 ; term ::= smb
 ; term ::= abstr ::= (lambda (smb) term)
 ; term ::= abstr ::= (lambda (smb0 smb ...1) body) ==> (lambda (smb0) (lambda (smb ...) term)
 ; term ::= (term term)
 ; term ::= (term0 term1 term2 ...) ==> ((term0 term1) term2 ...)
 ; smb  ::= identifier
 ;
 ; Free symbols are permitted. They are self-evaluating. There is one semantical restriction: a free symbol must not appear as the operator of an application that requires evaluation. All uncurried applications and abstractions are implicitly curried, i.e uncurried notation is treated as an abbreviation of a fully curried form. Terms are evaluated in lazy order. For this purpose promises are used. In order to allow nested promises to be lifted, a struct-type prom is used. Forcing is required only in the following two cases:
 ; 1: where the body of an abstaction being applied consists of a bound symbol only.
 ; 2: where the operator of an application being expanded is a bound symbol.
        
 (provide
  (rename app #%app) ; normal order curried application
  (rename kappa lambda) ; normal order curried lambda
  (rename #%datum #%top) ; allow free symbols as literal data
  (rename beg #%module-begin)) ; restrict to one expr and write its value
  ; #%datum is not provided such as to disallow literal data (free symbols excepted) 
 
 (define-syntax beg ; replaces #%module-begin
  (syntax-rules () ; restricts modules to one expr and makes them write the value
   ((beg x) (#%module-begin (#%app write x) (#%app newline)))))
 
 (define-struct prom (prom)) ; promise that allows lifting of nested promises
 
 (define-syntax postpone ; replaces delay
  (syntax-rules ()
   ((postpone x) (#%app make-prom (delay x)))))
 
 (define (xforce x) ; replaces force. lifts nested proms. protection against recursive
  (cond ; promises is not required. a prom never refers to itself.
   ((prom? x) (let ((y (xforce (prom-prom x)))) (set-prom-prom! x y) y))
   ((promise? x) (xforce (force x)))
   (else x)))
         
 (define-for-syntax (force-if-ident x) (if (identifier? x) #`(#%app xforce #,x) x))
 ; is called where the value of a bound symbol is required.

 (define-syntax (kappa stx) ; replaces lambda
  (syntax-case stx () 
   ((kappa (arg) body) #`(lambda (arg) #,(force-if-ident #'body))) ; force body if ident
   ((kappa (arg0 arg1 ...) body) #'(kappa (arg0) (kappa (arg1 ...) body))))) ; curry 
 
 (define-syntax (app stx) ; curry application and force its operator if it is a symbol
  (syntax-case stx ()
   ((app x y) #`(#%app #,(force-if-ident #'x) (postpone y))) ; force operator if symbol
   ((app x y z ...) #'(app (app x (postpone y)) z ...))))) ; curry

(module example-1 kappa
 ((lambda (omega) ; omega, which is not reducible, is never evaluated.
   ((lambda (x y) y) omega yes))
   ((lambda (x) (x x)) (lambda (x) (x x))))) ; --> yes

(require example-1) ; writes yes

(module example-2 kappa
 ((lambda (omega) ; omega, which is not reducible, is never evaluated.
   ((lambda (x y) x) omega yes))
   ((lambda (x) (x x)) (lambda (x) (x x))))) ; never returns

;(require example-2) ; never returns

(module example-3 kappa (a (lambda (x) x))) ; wrong: free symbol as operator

;(require example-3) --> error:
; procedure application: expected procedure, given: a; arguments were: #<struct:prom>

(module example-4 kappa ; of course i did not write this in the present shape by hand.
((lambda (identity)     ; this is a let* form expanded in terms of lambda.
((lambda (auto-apply)   ; for the calculus implemented here see any book on lambda calculus
((lambda (omega)        ; see any book on lambda calculus or combinators.
((lambda (normal-order-y)
((lambda (true)
((lambda (false) 
((lambda (bool->symbol) 
((lambda (if)
((lambda (and) 
((lambda (or) 
((lambda (not)
((lambda (cons)
((lambda (car)
((lambda (cdr)
((lambda (zero)
((lambda (add1)
((lambda (sub1)
((lambda (zero?)
((lambda (+)
((lambda (-)
((lambda (<)
((lambda (>)
((lambda (>=)
((lambda (<=) 
((lambda (=) 
((lambda (*)
((lambda (/)
((lambda (one) 
((lambda (two)
((lambda (three)
((lambda (four)
((lambda (eight)
((lambda (ten)
((lambda (expt)
((lambda (sqrt) 
; ---------------------------------------------------------------
; compute square root of 110 rounded down to integer
; check the result to be 10; convert to 'yes' if ok, 'no' if not.
(bool->symbol (= (sqrt (+ ten (expt ten two))) ten))) ; --> yes
; om my 1 GB 1.81 GZz AMD-sempron-3100+ this takes about 10 seconds,
; provided no other havy processes are running.
; ---------------------------------------------------------------
; read the remainder from bottom to top
(lambda (x) ; sqrt ; newtons method
 ((normal-order-y
   (lambda (sqrt)
    (lambda (guess) 
     ((lambda (guess**2) 
       (if (<= guess**2 x) guess (sqrt (/ (+ x guess**2) (+ guess guess))))) 
     (* guess guess)))))
  x))))
(normal-order-y ; expt
 (lambda (expt) (lambda (x y) (if (zero? y) one (* x (expt x (sub1 y)))))))))
(+ eight two))) ; ten
(+ four four))) ; eight
(+ two two))) ; four
(add1 two))) ; three
(add1 one))) ; two
(add1 zero))) ; one
(normal-order-y ; /
 (lambda (/) (lambda (x y) (if (< x y) zero (add1 (/ (- x y) y))))))))
(normal-order-y ; *
 (lambda (*) 
  (lambda (x y) 
   (if (zero? x) zero (if (zero? y) y (sub1 (+ (* (sub1 x) (sub1 y)) (+ x y))))))))))
(normal-order-y ; =
 (lambda (=) 
  (lambda (x y) (if (zero? x) (zero? y) (and (not (zero? y)) (= (sub1 x) (sub1 y)))))))))
(lambda (x y) (not (< y x))))) ; <=
(lambda (x y) (not (< x y))))) ; >=
(lambda (x y) (< y x)))) ; >
(normal-order-y ; <
(lambda (<) (lambda (x y) (and (not (zero? y)) (or (zero? x) (< (sub1 x) (sub1 y)))))))))
(normal-order-y ; -
 (lambda (-) (lambda (x y) (if (zero? x) zero (if (zero? y) x (- (sub1 x) (sub1 y)))))))))
(normal-order-y ; +
 (lambda (+) 
  (lambda (x y) 
   (if (zero? y) x (if (zero? x) y (add1 (add1 (+ (sub1 x) (sub1 y)))))))))))
car)) ; zero?
cdr)) ; sub1
(lambda (x) (cons false x)))) ; add1
identity)) ; zero
(lambda (x) (x false)))) ; cdr
(lambda (x) (x true)))) ; car
(lambda (x y) (lambda (z) (if z x y))))) ; cons
(lambda (x) (if x false true)))) ; not
(lambda (x y) (if x true y)))) ; or
(lambda (x y) (if x y false)))) ; and
(lambda (x y z) (x y z)))) ; if (can be a proc because evaluation is lazy)
(lambda (x) (x yes no)))) ; bool->symbol. 'yes' and 'no' are free, hence literal symbols
(lambda (x y) y))) ; false
(lambda (x y) x))) ; true
(lambda (f) (auto-apply (lambda (s) (f (auto-apply s))))))) ; normal order y combinator
(auto-apply auto-apply))) ; omega (irreducible, never evaluated)
(lambda (x) (x x)))) ; auto-apply
(lambda (x) x))) ; identity

(require example-4) ; writes yes