michaelballantyne / faster-minikanren Goto Github PK

View Code? Open in Web Editor NEW

151.0 151.0 36.0 232 KB

A fast implementation of miniKanren with disequality and absento, compatible with Racket and Chez.

License: MIT License

Scheme 87.49% Racket 1.38% HTML 10.89% Shell 0.25%

faster-minikanren's People

Contributors

Stargazers

Watchers

faster-minikanren's Issues

Disequality constraint not being honored

It looks like under certain circumstances the =/= constraint is not being honored:

> (run* (q r) (matche (q) (('A)) (('B))) (matche (q r) (('A 'a)) ((,?? 'b) (=/= q 'A))))
'(('A 'a) ('B 'b) ('A 'b))

In the second matche, I ask for r to be unified with 'b but I add the constraint that q not be equal to 'A. I expect there to only be two answers; q='A, r='a and q='B, r='b. But I get back a third answer, where q='A, r='b. I think this should have been forbidden by the disequality constraint.

Is this an actual issue with faster-minikanren or is it a problem with my understanding of the language?

`vars` may produce duplicates

faster-minikanren/mk.scm

Lines 565 to 571 in dc5390a

 (define (vars term) 

 (let rec ((term term) (acc '())) 

 (cond 

 ((var? term) (cons term acc)) 

 ((pair? term) 

 (rec (cdr term) (rec (car term) acc))) 

 (else (remove-duplicates acc)))))

When term is a pair such as (,x . ,x), the result would include two instances of the var. Not sure if this would lead to bad reification later or not.

Support variable unification in matche patterns

When given an existing variable name in a pattern, matche appears to treat it as a new variable. Example:

(run 2 (q r) (matche (r) (((Foo ,q))) (((Bar ,q)))) (== q 'Qux))
'((Qux (Foo _.0)) (Qux (Bar _.0)))

I expected the output to be '((Qux (Foo Qux)) (Qux (Bar Qux))).

I glanced at the paper describing the implementation of matche, lambdae, and defmatche and the problems encountered therein, but this didn't look like one of them. Is this feature doable?

Bignums, big problem

@gregr pointed out that numbers may get big enough that eq? is no longer sufficient or correct. Such bugs would be especially pernicious, because they would only rarely manifest, and only on long-running or large programs. He suggests switching to bignum-accepting eqv? where numeric comparisons occur.

Wrong result with absento

#lang racket
(require minikanren)

(run 1 (q)
  (== q 'A)
  (absento q '(A)))

;; should be '()
;; wrongly produces '(A)

P.S.
If I rewrite it to use my own "not-membero" relation instead of absento, it produces the correct '() result.

P.P.S
webyrd/miniKenren-with-symbolic-constraints seems to have the correct behavior on this example.

Chicken scheme support?

It looks some time ago we had chicken scheme support 2fbdae6 but now it is removed?
Any chance that it could be restored easily?

The origin of the question is that I'm curious how performance of faster-miniKanren changes between scheme implementations. I want to now that Scheme itself gives good performance (because list-based data representation) or the good performance is an achievement of the Chez backend

@michaelballantyne

Add generalized absento

Thoughts copied from #2

(absento a b) is equivalent to: for all subtrees s of b, (=/= a s).

Applying (absento a b) where a and b are fresh logic variables should apply (=/= a b) and add a to the absento part of the constraint record for b. If b is instantiated to a pair (c . d), we'll consult the constraint record and apply (absento a c) and (absento a d), which will create the disequalities and add the absento constraint record to c and d just as we did with b.

Generalized absento still doesn't allow a constraint to restrict the range of values for a variable to a finite range, so it shouldn't break any of the assumptions that make the attributed variable implementation safe.

Unused argument in reifier

faster-minikanren/mk.scm

Line 573 in dc5390a

(define (extract-and-normalize st relevant-vars x)

x

dead link in readme

New link seems to be:
https://users.soe.ucsc.edu/~lkuper/papers/walk.pdf

Does not compile with Guile 2.2.3

Here is my setup:
I have a directory /home/user/development/Guile/libs, which I am adding to the GUILE_LOAD_PATH environment variable, to prepend it to the load path of Guile, as described in the docs:

# Guile Scheme Load Path
export GUILE_LOAD_PATH=/home/user/development/Guile/libs

in my .bashrc file. In that directory I have the folder faster-miniKanren, which is the git clone result for this repository.

Then I enter the Guile REPL and check the load path:

scheme@(guile-user)> %load-path 
$1 = ("/home/user/development/Guile/libs" "/usr/local/share/guile/2.2" "/usr/local/share/guile/site/2.2" "/usr/local/share/guile/site" "/usr/local/share/guile")

Then I try to use the module:

scheme@(guile-user)> (use-modules (faster-miniKanren mk-guile))
;;; note: auto-compilation is enabled, set GUILE_AUTO_COMPILE=0
;;;       or pass the --no-auto-compile argument to disable.
;;; compiling /home/user/development/Guile/libs/faster-miniKanren/mk-guile.scm
;;; WARNING: compilation of /home/user/development/Guile/libs/faster-miniKanren/mk-guile.scm failed:
;;; In procedure open-file: No such file or directory: "faster-miniKanren/mk-vicare.scm"

I am not sure why the mk-guile.scm would reference faster-miniKanren/mk-vicare.scm.

Is there any more info I need to provide for this issue?
How can I get this to run?

Room to cleanup compatibility layer

Now that racket is on top of Chez is there room to remove some of these mk-specific compatibility layer prims?

faster-minikanren/private-unstable.rkt

Lines 10 to 38 in 910fbea

 (module compatibility racket/base 

 (provide (all-defined-out)) 

 (require racket/list) 

 (define (list-sort f l) (sort l f)) 

 (define (remp f l) (filter-not f l)) 

 (define (call-with-string-output-port f) 

 (define p (open-output-string)) 

 (f p) 

 (get-output-string p)) 

 (define (exists f l) (ormap f l)) 

 (define for-all andmap) 

 (define (find f l) 

 (cond [(memf f l) => car] [else #f])) 

 (define memp memf)) 

 (require (submod "." compatibility)) 

 (define empty-intmap (hasheq)) 

 (define (intmap-count m) (hash-count m)) 

 (define (intmap-ref m k) (hash-ref m k (lambda () unbound))) 

 (define (intmap-set m k v) (hash-set m k v))

Integrate atomic type constraints with unification

It should help us avoid some occurs checks. Consider:

(define-relation (foo x y)
  (symbolo x)
  (== x y))

In the case where y is a very large list, we'll do the unification and the expensive occurs check before rechecking the symbolo constraint and discovering it is not satisfied. If we integrate atomic type constraints with unification and the substitution, the failure can be discovered immediately during unification.

Use variable-age ordering to simplify disequality

It seems like we might be able to get away with only watching one side of the disequality, now.

	(define (vars term)
	(let rec ((term term) (acc '()))
	(cond
	((var? term) (cons term acc))
	((pair? term)
	(rec (cdr term) (rec (car term) acc)))
	(else (remove-duplicates acc)))))

	(module compatibility racket/base
	(provide (all-defined-out))

	(require racket/list)

	(define (list-sort f l) (sort l f))

	(define (remp f l) (filter-not f l))

	(define (call-with-string-output-port f)
	(define p (open-output-string))
	(f p)
	(get-output-string p))

	(define (exists f l) (ormap f l))

	(define for-all andmap)

	(define (find f l)
	(cond [(memf f l) => car] [else #f]))

	(define memp memf))

	(require (submod "." compatibility))

	(define empty-intmap (hasheq))
	(define (intmap-count m) (hash-count m))
	(define (intmap-ref m k) (hash-ref m k (lambda () unbound)))
	(define (intmap-set m k v) (hash-set m k v))

michaelballantyne / faster-minikanren Goto Github PK

faster-minikanren's People

Contributors

Stargazers

Watchers

Forkers

faster-minikanren's Issues

Recommend Projects

Recommend Topics

Recommend Org