Synthesizing functions as folds from test cases

README.md

Intro

The fold function captures a common recursion pattern

(define (fold kons knil list) ;; Uncurried version
  (if (null? list)
      knil
      (kons (car list) (fold kons knil (cdr list)))))

so it can define a lot of common list functions easily:

(define (append x y) (fold cons y x))

(define (map f l) (fold (lambda (x xs) (cons (f x) xs)) '() l))

(define (reverse x) ((fold (lambda (x y) (lambda (z) (y (cons x z))))
                           (lambda (i) i)
                           x) '()))

Summary

Add a fold function to the relational interpreter:

  ....
        ((fresh (kons knil ls v3 r)
           (== `(fold ,kons ,knil ,ls) expr)
           (unboundo 'fold env)
           (eval-expo ls env v3)
           (make-foldo kons knil v3 r)
           (eval-expo r env out)))
  ....

along with a helper relation to build a fold expression up:

(define (make-foldo kons knil ls res)
  (conde
   ((== ls '()) (== res knil))
   ((fresh (u v m)
      (== ls `(,u . ,v))
      (== res `((,kons ',u) ,m))
      (make-foldo kons knil v m)))))

Make relations to help run test queries:

(define (testo rec base input output)
 (eval-expo `(fold ,rec ,base ',input) '() output))

(define (testo-app-nil rec base input output)
  (fresh (t1 t2)
   ;; eta expanded template to help things along a little
   (== base `(lambda (x) ,t1))
   (== rec `(lambda (x) (lambda (y) (lambda (z) ,t2))))
   (eval-expo `((fold ,rec ,base ',input) '()) '() output)))

and then we can derive some simple recursive functions as folds using tests!

Results

(define (synth-appendo f)
  (fresh (rec base)
    (== f `(lambda (input) (fold ,rec ,base input)))
    (testo rec base '(a b c) '(a b c u v))
    (testo rec base '(x y) '(x y u v))
    (testo rec base '() '(u v))))
;; => Yes. (361.12ms)
;; f: (lambda (input)
;;      (fold (lambda (_.0)
;;              (lambda (_.1)
;;                (cons _.0 _.1)))
;;            (quote (u v))
;;            input))

(define (synth-map f)
  (fresh (rec base)
    (== f `(lambda (input) (fold ,rec ,base input)))
    (testo rec base '() '())
    (testo rec base '(x) '((f . x)))
    (testo rec base '(y) '((f . y)))
    (testo rec base '(u v w) '((f . u) (f . v) (f . w)))))
;; => Yes. (2284.32ms)
;; f: (lambda (input)
;;      (fold (lambda (_.0)
;;              (lambda (_.1)
;;                (cons (cons (quote f) _.0) _.1)))
;;            (quote ())
;;            input))

(define (synth-reverse f)
  (fresh (rec base)
    (== f `(lambda (input) ((fold ,rec ,base input) '())))
    (testo-app-nil rec base '() '())
    (testo-app-nil rec base '(a) '(a))
    (testo-app-nil rec base '(b) '(b))
    (testo-app-nil rec base '(x y) '(y x))
    (testo-app-nil rec base '(d e l i v e r) '(r e v i l e d))))
;; => Yes. (1277.19ms)
;; f: (lambda (input)
;;      ((fold (lambda (x)
;;               (lambda (y)
;;                 (lambda (z) (y (cons x z)))))
;;             (lambda (x) x)
;;             input)
;;       (quote ())))

Alternative

To derive the real append (rather than a specialized version):

(define (synth-appendo f)
  (fresh (rec base)
    (== f `(lambda (a)
             (lambda (b)
               (fold ,rec ,base a))))
    
    (eval-expo `((,f '(a b c)) '(u v)) '() '(a b c u v))
    (eval-expo `((,f '(x y)) '(z)) '() '(x y z))
    (eval-expo `((,f '()) '(o k !)) '() '(o k !))))
;; => Yes. (461.12ms)
;; f: (lambda (a) (lambda (b) (fold (lambda (_.0) (lambda (_.1) (cons _.0 _.1))) b a)))

synth.scm

;; relational scheme interpreter

(define lookupo
  (lambda (x env out)
    (fresh (y val env^)
      (== `((,y . ,val) . ,env^) env)
      (symbolo x)
      (symbolo y)
      (conde
        ((== x y) (== val out))
        ((=/= x y) (lookupo x env^ out))))))


(define unboundo
  (lambda (x env)
    (fresh ()
      (symbolo x)
      (conde
        ((== '() env))
        ((fresh (y v env^)
           (== `((,y . ,v) . ,env^) env)
           (=/= x y)
           (unboundo x env^)))))))

(define (make-foldo kons knil ls res)
  (conde
   ((== ls '()) (== res knil))
   ((fresh (u v m)
      (== ls `(,u . ,v))
      (== res `((,kons ',u) ,m))
      (make-foldo kons knil v m)))))

(define eval-expo
  (lambda (expr env out)
    (fresh ()
      (conde
        ((symbolo expr) ;; variable
         (lookupo expr env out))
        ((== `(quote ,out) expr)
         (absento 'closure out)
         (unboundo 'quote env))
        ((fresh (x body) ;; abstraction
           (== `(lambda (,x) ,body) expr)
           (== `(closure ,x ,body ,env) out)
           (symbolo x)
           (unboundo 'lambda env)))
        ((fresh (expr*)
           (== `(list . ,expr*) expr)
           (unboundo 'list env)
           (eval-exp*o expr* env out)))
        ((fresh (e1 e2 val x body env^) ;; application
           (== `(,e1 ,e2) expr)
           (eval-expo e1 env `(closure ,x ,body ,env^))
           (eval-expo e2 env val)
           (eval-expo body `((,x . ,val) . ,env^) out)))
        ((fresh (e1 e2 v1 v2)
           (== `(cons ,e1 ,e2) expr)
           (== `(,v1 . ,v2) out)
           (unboundo 'cons env)
           (eval-expo e1 env v1)
           (eval-expo e2 env v2)))
        ((fresh (kons knil ls v3 r)
           (== `(fold ,kons ,knil ,ls) expr)
           (unboundo 'fold env)
           (eval-expo ls env v3)
           (make-foldo kons knil v3 r)
           (eval-expo r env out)))
        ((fresh (e v2)
           (== `(car ,e) expr)
           (unboundo 'car env)
           (eval-expo e env `(,out . ,v2))))
        ((fresh (e v1)
           (== `(cdr ,e) expr)
           (unboundo 'cdr env)
           (eval-expo e env `(,v1 . ,out))))
        ((fresh (e v)
           (== `(null? ,e) expr)
           (conde
             ((== '() v) (== #t out))
             ((=/= '() v) (== #f out)))
           (unboundo 'null? env)
           (eval-expo e env v)))
        ((fresh (t c a b)
           (== `(if ,t ,c ,a) expr)
           (unboundo 'if env)
           (eval-expo t env b)
           (conde
             ((== #f b) (eval-expo a env out))
             ((=/= #f b) (eval-expo c env out)))))))))

(define eval-exp*o
  (lambda (expr* env out)
    (conde
      ((== '() expr*) (== '() out))
      ((fresh (a d res-a res-d)
         (== (cons a d) expr*)
         (== (cons res-a res-d) out)
         (eval-expo a env res-a)
         (eval-exp*o d env res-d))))))


;;;

(define (testo rec base input output)
 (eval-expo `(fold ,rec ,base ',input) '() output))

(define (testo-app-nil rec base input output)
  (fresh (t1 t2)
   ;; eta expanded template to help things along a little
   (== base `(lambda (x) ,t1))
   (== rec `(lambda (x) (lambda (y) (lambda (z) ,t2))))
   (eval-expo `((fold ,rec ,base ',input) '()) '() output)))

(define (synth-appendo f)
  (fresh (rec base)
    (== f `(lambda (input) (fold ,rec ,base input)))
    (testo rec base '(a b c) '(a b c u v))
    (testo rec base '(x y) '(x y u v))
    (testo rec base '() '(u v))))

(define (synth-map f)
  (fresh (rec base)
    (== f `(lambda (input) (fold ,rec ,base input)))
    (testo rec base '() '())
    (testo rec base '(x) '((f . x)))
    (testo rec base '(y) '((f . y)))
    (testo rec base '(u v w) '((f . u) (f . v) (f . w)))))

(define (synth-reverse f)
  (fresh (rec base)
    (== f `(lambda (input) ((fold ,rec ,base input) '())))
    (testo-app-nil rec base '() '())
    (testo-app-nil rec base '(a) '(a))
    (testo-app-nil rec base '(b) '(b))
    (testo-app-nil rec base '(x y) '(y x))
    (testo-app-nil rec base '(d e l i v e r) '(r e v i l e d))))