CLP(Rosette)-miniKanren - A miniKanren variant integrated with Rosette

Show & Tell
1

Hi,

I wrote a miniKanren variant integrated with Rosette. It uses Rosette (SMT) as a backend for constraints solving. Now you can use SMT assertions as constraints. It significantly improves the expressiveness of miniKanren. See GitHub - chansey97/clprosette-miniKanren: CLP(Rosette) on top of miniKanren.

For example, you can define a factorial relation in miniKanren and run it forward or backward.

#lang racket
(require "../mk.rkt")
(require "../rosette-bridge.rkt")

(define (faco n out)
  (conde
    ((== n 0) (== out 1))
    ((rosette-typeo n r/@integer?)
     (rosette-asserto `(,r/@! (,r/@= ,n 0)))
     (fresh (n-1 r)
       (rosette-typeo n-1 r/@integer?)
       (rosette-typeo r r/@integer?)
       (rosette-typeo out r/@integer?)
       (rosette-asserto `(,r/@= (,r/@- ,n 1) ,n-1))
       (rosette-asserto `(,r/@= (,r/@* ,n ,r) ,out))
       (faco n-1 r)))))

;; run factorial forward
(run* (q)
  (fresh (out)
    (faco 5 out)
    (== q out)))
;; '(120)

;; run factorial backward
(run* (q)
  (fresh (n)
    (faco n 120)
    (== q n)))
;; '(5)

;; No solution such that fac n = 500
(run* (q)
  (fresh (n)
    (faco n 500)
    (== q n)))
;; '()

;; Get all factorials
(run 7 (q)
  (fresh (n out)
    (faco n out)
    (== q `(,n ,out))))
;; '((0 1) (1 1) (2 2) (3 6) (4 24) (5 120) (6 720))

Here,

  • (rosette-typeo <var> <type) is a Rosette type constraint.

    It constraints a miniKanren variable's domain as a Rosette type. You can put all Rosette solvable types in <type> , but prefix it with r/.

  • (rosette-asserto <formula>) checks a SMT formula satisfiable.

    The <formula> can include any miniKanren variables, as long as they have been constrained by rosette-typeo. Again, you can put all Rosette operators in <formula> , but prefix it with r/.

Note that the factorial example is not easy to be implemented in "vanilla miniKanren" (e.g. miniKanren-symbolic-constraints), because "vanilla miniKanren" does not support relational arithmetic operations.

P.s. The Reasoned Schemer introduced Kiselyov Arithmetic, which encodes natural numbers as lists of binary digits, but it is difficult to use and not flexible (e.g. it doesn't support negative numbers, rational, real, etc). CLP(Rosette)-miniKanren supports all Rosette solvable types out of the box (e.g. booleans, integers, reals, bitvectors, and uninterpreted functions). Also, I believe extending other SMT theories is not difficult.

This project is still working in progress, any advice would be appreciated.

Enjoy .

9 Likes