Redex model of "machine" semantics for micro-kanren. May not be faithful.

redex-micro-kanren.rkt

#lang racket/base

(require redex)

(define-language μ-Kanren
  ;; Syntax
  [#|Term    |# t ::= x () number (t t)]
  [#|Goal    |# g ::= (g ∨ g) (g ∧ g) (∃ (x ...) g) (↓ f t ...) (t ≡ t)]
  [#|Goal Abs|# f ::= (side-condition (name f any) (procedure? (term f)))]
  [#|Variable|# x ::= variable-not-otherwise-mentioned]
  ;; Semantics
  [#|Substitution |# σ  ::= ([x t] ...)]
  [#|Maybe Subst. |# ?σ ::= σ #f]
  [#|Search-State |# s  ::= (c ...)]
  [#|Configuration|# c  ::= (?σ g ...)]
  
  #| Being sloppy. Enabling below uglifies the printing
  #:binding-forms
  (∃ (x ...) g #:refers-to (shadow x ...))
  |#)

;; "Machine" semantics of relational programs
(define ~>
  (reduction-relation
   μ-Kanren #:domain s
   ;; "push" rules
   [--> ({σ (g_1 ∨ g_2) g ...} c ...)
        ({σ g_1 g ...} c ... {σ g_2 g ...})
        disj]
   [--> ({σ (g_1 ∧ g_2) g ...} c ...)
        ({σ g_1 g_2 g ...} c ...)
        conj]
   [--> ({σ (∃ (x ...) g_1) g ...} c ...)
        ({σ g_1* g ...} c ...)
        exists
        (where (x_* ...) ,(fresh! (term (x ...))))
        (where g_1* (substitute* g_1 (x ...) (x_* ...)))]
   [--> ({σ (↓ f t ...) g ...} c ...)
        (c ... {σ g ... g_1})
        zzz
        (where g_1 ,(apply (term f) (term (t ...))))]
   [--> ({σ (t_1 ≡ t_2) g ...} c ...)
        ({(unify t_1 t_2 σ) g ...} c ...)
        unify]
   ;; "pop" rules
   [--> ({#f g ...} c ...)
        (c ...)
        fail+continue]
   [--> ({σ} c ...)
        (c ...)
        succeed+continute
        (where _ ,(printf "~nfound: ~a~n" (term σ)))]))

(define-metafunction μ-Kanren
  unify : t t σ -> ?σ
  [(unify t_1 t_2 σ) (unify-loop (walk t_1 σ) (walk t_2 σ) σ)])

(define-metafunction μ-Kanren
  unify-loop : t t σ -> ?σ
  [(unify-loop x x σ) σ]
  [(unify-loop x t σ) (ext x t σ)]
  [(unify-loop t x σ) (ext x t σ)]
  [(unify-loop (t_1a t_1b) (t_2a t_2b) σ)
   (unify t_1b t_2b σ_1)
   (where σ_1 (unify t_1a t_2a σ))]
  [(unify-loop t t σ) σ]
  [(unify-loop _ _ _) #f])

(define-metafunction μ-Kanren
  walk : t σ -> t
  [(walk x (name σ (_ ... [x t] _ ...))) (walk t σ)]
  [(walk t _) t])

(define-metafunction μ-Kanren
  ext : x t σ -> ?σ
  [(ext x t σ) ([x t] ,@(term σ))
   (side-condition (not (term (occurs? x t σ))))]
  [(ext _ _ _) #f])

(define-relation μ-Kanren
  occurs? ⊆ x × t × σ
  [(occurs? x (t _) σ) (occurs? x t σ)]
  [(occurs? x (_ t) σ) (occurs? x t σ)]
  [(occurs? x x σ)])

(define-metafunction μ-Kanren
  substitute* : g (x ...) (x ...) -> g
  [(substitute* g () ()) g]
  [(substitute* g (x_1 x_1* ...) (x_2 x_2* ...))
   (substitute* (substitute g x_1 x_2) (x_1* ...) (x_2* ...))])

(define fresh!
  (let ([i 0])
    (λ (xs) (set! i (+ 1 i))
       (map (λ (x) (string->symbol (format "~a_~a" x i))) xs))))

;; Visualize program execution
(define (viz p) (traces ~> (term (inj ,p))))

;; Load program into initial state
(define-metafunction μ-Kanren
  inj : g -> s
  [(inj g) ({() g})])

(module+ test
  (define (appendo l r a)
    (term (((,l ≡ ()) ∧ (,r ≡ ,a))
           ∨
           (∃ (h l* a*)
              ((,l ≡ (h l*))
               ∧ ((↓ ,appendo l* r a*)
                  ∧ (,a ≡ (h a*))))))))
  (viz (appendo 'l 'r '(1 (2 (3 ()))))))