I think the core of what you might want is something like the below. If you
want a complete solver for disequality constraints, you'll to store
disequality constraints that are not inviolable in the current
substitution. In the version below, we keep ahold of *all* of the
disequality constraints in a field we've added.
== hasn't changed much. The change is that when we add a new equation, we
check if equation invalidates one of our disequations. We know
a disequation is violated if the substitution we get after trying to unify
the terms we said shouldn't be equal is the same as it was before we tried
to unify them. If those the terms unify with some extension to the
substitution, well then that extension is a way to represent the additional
criteria that would cause the disequality constraint to fail. If the terms
don't unify in the current substitution, then our disequality isn't saying
anything we don't already know from the substitution.
Every time we add a new equation or disequation, we check if we've violated
some disequality constraints by checking each of them one at a time.
There's a whole lot of dimensions in the design space to play with; this is
just one possible point you might end up at.
(define (== u v)
(lambda (s/d/c)
(let ((s (unify u v (car s/d/c))))
(if s (return (cons s (cdr s/d/c))) '()))))
(define (invalid? s d)
(ormap (lambda (pr) (equal? (unify (car pr) (cdr pr) s) s)) d))
(define (return a) (if (invalid? (car a) (cadr a)) '() (list a)))
(define (=/= u v)
(lambda (s/d/c)
(let ((s (car s/d/c)) (d (cadr s/d/c)) (c (cddr s/d/c)))
(return `(,s ((,u . ,v) . ,d) . ,c)))))
On Thu, Mar 9, 2017 at 2:16 PM, William Byrd <[email protected]> wrote:
> symbolo and numbero are run-time type constraints. (symbolo x)
> ensures that 'x' is a symbol. (numbero x) ensures 'x' is a number.
>
> (fresh (x) (symbolo x) (== x 5)) fails, while (fresh (x) (symbolo x)
> (== x 'foo)) succeeds.
>
> symbolo and numbero allow us to represent symbols and numbers without
> having to use tagged lists such as '(sym foo) or '(num 5), or `(sym
> ,x) or `(num ,x) when using uninstantiated logic variables. This is
> especially useful when writing interpreters, type inferencers, and
> parsers in miniKanren, in which we don't want to have to tag the
> terms.
>
> > How can I implement =/=?
>
> There are multiple ways to implement =/=. You might start by looking
> at this paper:
>
> https://arxiv.org/pdf/1701.00633.pdf
>
> Cheers,
>
> --Will
>
> On Thu, Mar 9, 2017 at 12:02 PM, Amirouche Boubekki
> <[email protected]> wrote:
> > I can't understand what the purpose can someone explain it to me?
> >
> > How can I implement =/=?
> >
> >
> > Tx!
> >
> > --
> > You received this message because you are subscribed to the Google Groups
> > "minikanren" group.
> > To unsubscribe from this group and stop receiving emails from it, send an
> > email to [email protected].
> > To post to this group, send email to [email protected].
> > Visit this group at https://groups.google.com/group/minikanren.
> > For more options, visit https://groups.google.com/d/optout.
>
> --
> You received this message because you are subscribed to the Google Groups
> "minikanren" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to [email protected].
> To post to this group, send email to [email protected].
> Visit this group at https://groups.google.com/group/minikanren.
> For more options, visit https://groups.google.com/d/optout.
>
--
JBH
--
You received this message because you are subscribed to the Google Groups
"minikanren" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/minikanren.
For more options, visit https://groups.google.com/d/optout.
