Tx that's exactly what I want to do! On Thu, Mar 9, 2017 at 11:05 PM Jason Hemann <[email protected]> wrote:
> 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. > -- 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.
