sk.scm

; Regular SKI evaluator
(define eval-sk
  (lambda (es)
    (cond
      ; drop parenthesis (left-associativity)
      [(and (list? es) (positive? (length es)) (list? (car es)))
       (eval-sk (append (car es) (cdr es)))]
      ; K
      [(and (list? es) (>= (length es) 3) (eq? (car es) 'K))
       (eval-sk (cons (cadr es) (cdddr es)))]
      ; S
      [(and (list? es) (>= (length es) 4) (eq? (car es) 'S))
       (let ((x (cadr es))
             (y (caddr es))
             (z (cadddr es))
             (tl (cddddr es)))
         (eval-sk `(,x ,z (,y ,z) . ,tl)))]
      [(list? es) (map eval-sk es)]
      [else es])))

; Examples
(eval-sk '(a b c d))                                      ;; a b c d
(eval-sk '(K a))                                          ;; K a
(eval-sk '(K a b c))                                      ;; a c
(eval-sk '(S a b))                                        ;; S a b
(eval-sk '(S a b c))                                      ;; a c (b c)
(eval-sk '(S a b c d f))                                  ;; a c (b c) d f
(eval-sk '((K a) b c))                                    ;; a c
(eval-sk '(S K K a))                                      ;; a
(eval-sk '((K(S K K)) a b))                               ;; b
(eval-sk '(((S((S(K((S(K S))K)))S))(K K)) a b c))         ;; a c b
(eval-sk '(((S((S K)K))((S K)K)) a))                      ;; a a
(eval-sk '(((S((S(K S))K))(K((S((S K)K))((S K)K)))) a b)) ;; a (b b)

; I'm using the miniKanren from:
; https://github.com/webyrd/miniKanren-with-symbolic-constraints

; Some preliminaries borrowed from The Reasoned Schemer

(define nullo
  (lambda (x)
    (== '() x)))

(define conso
  (lambda (hd tl q)
    (== (cons hd tl) q)))

(define pairo
  (lambda (p)
    (fresh (x y) (conso x y p))))

(define caro
  (lambda (p d)
    (fresh (b) (== (cons d b) p))))

(define cdro
  (lambda (p d)
    (fresh (a) (== (cons a d) p))))

(define listo
  (lambda (l)
    (conde
      ((nullo l) succeed)
      ((pairo l)
       (fresh (d)
              (cdro l d)
              (listo d)))
      )))

(define proper-listo
  (lambda (l)
    (conde
      ((pairo l)
       (fresh (d)
              (cdro l d)
              (listo d)))
      )))

(define appendo
  (lambda (l s out)
    (conde
      [(== '() l) (== s out)]
      [(fresh (a d res)
         (== `(,a . ,d) l)
         (== `(,a . ,res) out)
         (appendo d s res))])))


; Some additional helpers for handling lists

(define mapo
  (lambda (f l out)
    (conde
      [(== '() l) (== '() out)]
      [(fresh (hd hdo tl tlo)
              (== `(,hd . ,tl) l)
              (f hd hdo)
              (mapo f tl tlo)
              (== (cons hdo tlo) out))]
              )))

(define mape
  (lambda (f l out)
    (conde
      [(== '() l) (== '() out)]
      [(fresh (hd hdo tl tlo)
              (conso hd tl l)
              (conde
                [(== hd hdo)]
                [(f hd hdo)])
              (mapo f tl tlo)
              (== (cons hdo tlo) out))]
              )))

(define for-allo
  (lambda (f l)
    (conde
      [(== '() l)]
      [(fresh (hd tl)
              (== `(,hd . ,tl) l)
              (f hd)
              (for-allo f tl))])))

; Goal for checking that a list is an SKI-combinator (ie does not contain variables)
(define combinatoro
  (lambda (q)
    (conde
      [(== 'K q)]
      [(== 'S q)]
      [(proper-listo q) (for-allo combinatoro q)]
      )))


; Here comes the attempted SKI-evaluator:

; Take an evaluation step
(define step-sko
  (lambda (e f)
    (conde
      [(fresh (a b tl)
              (== `(K ,a ,b . ,tl) e)
              (== `(,a . ,tl) f))]
      [(fresh (a b c tl)
              (== `(S ,a ,b ,c . ,tl) e)
              (== `(,a ,c (,b ,c) . ,tl) f))]
      [(fresh (a tl l)
              (== `(,a . ,tl) e)
              (proper-listo a)
              (appendo a tl l)
              (== l f))]
      )))

; Try taking a step on all expressions in a list
(define spread-sko
  (lambda (e f)
    (fresh ()
           (mape step-sko e f)
           (=/= e f))))

; The evaluator
(define eval-sko
  (lambda (e f)
    (conde
      [(spread-sko e f)]
      [(step-sko e f)]
      [(fresh (g) (spread-sko e g) (eval-sko g f))]
      [(fresh (g) (step-sko e g) (eval-sko g f))]
      )))

; Works fine forwards
(run* (q) (eval-sko '(K a b) q)) ; ((a))
(run* (q) (eval-sko '(S a b c) q)) ; ((a c (b c)))
(run* (q) (eval-sko '(S K K a) q)) ; ((K a (K a)) (a)) NB. not evaluated fully
(run* (q) (eval-sko '(S K K a) q) (absento 'S q) (absento 'K q)) ; ((a)) use absento to force evaluation
(run* (q) (eval-sko '(S (S K K) (S K K) a) q) (absento 'S q) (absento 'K q)) ; ((a (a))) the mocking bird: λa.a a

(run 10 (q) (eval-sko `(,q a) '(a)) (combinatoro q)) ; can find some identity combinators
(run 1 (q) (eval-sko `(,q a b) '(a))) ; and K
(run 1 (q) (eval-sko `(,q a b c) '(a c (b c)))) ; and S

(run 5 (q) (eval-sko `(,q a b) '(b)) (combinatoro q))
; after quite a while: ((S K) ((S K)) (S (K)) (K S K K) (K S S K))

(run 1 (q) (eval-sko `(,q a) '(a (a))) (combinatoro q))
; doesn't seem to terminate any time soon...