Skip to content

Home

Jump to bottom
Ambrose Bonnaire-Sergeant edited this page Jul 20, 2011 · 75 revisions

Introduction to Logic Programming with Clojure

This tutorial assumes zero experience with Logic Programming, but some experience with Clojure.

Please direct any feedback to Ambrose Bonnaire-Sergeant via http://twitter.com/#!/ambrosebs or abonnairesergeant@gmail.com

Thanks

Many thanks to these Clojurists for their invaluable feedback and encouragement!

David Nolen Twitter, Github, Blog

Jim Duey Twitter

How to use this Tutorial

This tutorial is meant to be used with a Clojure REPL handy. An example project has been set up.

You should be able to run all code examples in the logic-introduction.core namespace.

Also, don't forget your pen and paper!

Introduction

Welcome!

In the following sections, we will explore an implementation of miniKanren, a logic programming system.

At least two ports of miniKanren to Clojure have been made:

This tutorial will use core.logics implementation, which resides in the namespace clojure.core.logic.minikanren. core.logics port is rather faithful to miniKanren, which has its roots in Scheme.

Because of this, it carries some historical baggage.

Function names are rather terse compared to idiomatic Clojure, but we will try and help by providing some mnemonics. But don't worry, a little practice and they'll be like old friends.

We also follow the convention of naming relations with the suffix "o".

Enjoy building the type checker, but keep an eye on it ... I think I saw it move!

Motivation: Simple Type Checker

Let's say we want to check the resulting type for this expression:

(let [f (fn [a] a)
      g 1]
  (f g))

We propose an interface for a type checker:

(typed
  <environment>
  <expression>
  <expected-type>)
;=> <boolean>

An initial version of typed (aka. "Type Determine") takes three arguments:

  1. an environment (map of variables to values),
  2. an expression,
  3. and an expected resulting type.

typed returns true if the resulting type of executing the expression in the given environment is equal to the third argument.

In other words, return true if it type-checks successfully.

Here are some imaginary executions of typed.

(typed
  [f (fn [a] a)
   g 1]
  (f g)
  Integer)
;=> true


(typed
  [f (fn [a] a)
   g 1]
  (f g)
  Float)
;=> false

Converting a function into a relation

Logic Programming Concept: Relations

A relation is simply a function that returns a goal as its value.

Logic Programming Concept: Goals

A goal can either succeed or fail.

  • clojure.core.logic.minikanren/succeed represents the successful goal
  • clojure.core.logic.minikanren/fail represents a failed goal.

Goals are used like constants, being returned by relations as values.

Implementation note

While succeed and fail are implemented as functions, they are never called explicitly.

We will see an example of using goals in the section explaining conde.

Let's propose a new interface for typed that converts it into a relation.

(typedo
  <environment>
  <expression>
  <expected-type>)
;=> <goal>

By convention, relations end their name with "o".

Compare to typeds calling interface:

(typed
  <environment>
  <expression>
  <expected-type>)
;=> <boolean>

Note what we changed:

  1. We renamed typed to typedo
  2. typedo returns a goal instead of a Boolean value

Running the relational type checker

Logic Programming Concept: run

To execute a logic expression, we use run*.

run* is not a relation; it does not return goal.

As an example, let's roughly translate the following code,

(let [f (fn [a] a)
      g 1]
  (f g))

into our type checker, and test that it returns an integer.

(run* [q]
      (typedo [['f :- [Integer :> Integer]] ;; 'f is of type Integer -> Integer
               ['g :- Integer]              ;; 'g is of type Integer
               ] 
              [:apply 'f 'g] ;; Determine the resulting type of ('f 'g) ..
              Integer)       ;;  and succeed if it is Integer
      )
;=> (_.0)

Here are some facts:

  • :- is pronounced "is of type".

  • [Integer :> Integer] represents the type of a function that take a single argument of type Integer and returns a value of type Integer.

  • ['f :- [Integer :> Integer]] is called a type association.

  • [ ['f :- [Integer :> Integer] ] ['g :- Integer]] is an environment (represented by a vector of type associations).

  • [:apply x y] represents the function call (x y).

There are still mysteries about run* that we will leave for now:

  1. What does run*s first argument, [q], mean?
  2. What exactly is run*s return value? We've already said it's not a relation, therefore it doesn't return a goal, but what is it?

Play with the type checker

Let's get a feel for our type checker.

(run* [q]
      (typedo [['f :- [Float :> Integer]]
               ['g :- Integer]
               ] 
              [:apply 'f 'g]
              Integer)
      )
;=> ()

The run returns () because typedo fails.

typedo fails because it returns the unsuccessful goal, fail.

Therefore the run expands to:

(run* [q]
      fail
      )

Why did typedo fail?

(run* [q]
      (typedo [['f :- [Float :> Integer]]
               ['g :- Float]
               ] 
              [:apply 'f 'g]
              Integer)
      )
;=> (_.0)

The run returns a non-empty list because no goals failed.

typedo succeeds because it returns the successful goal, succeed.

Therefore the run expands to:

(run* [q]
      succeed
      )

Why did typedo succeed?

(run* [q]
      (typedo [['f :- [Float :> Integer]]
               ['g :- Float]
               ['h :- [Integer :> Float]]
               ] 
              [:apply 'h [:apply 'f 'g]]
              Float)
      )
;=> (_.0)

The run returns a non-empty list because goals failed. (Why does typedo succeed?)

Familiar faces

(run* [q]
      (typedo [['max :- [Integer :> [Integer :> Integer]]]
               ['a :- Integer]
               ['b :- Integer]
               ] 
              [:apply [:apply 'max 'a] 'b]
              Integer)
      )
;=> (_.0)

The run returns a non-empty list because no goals failed. (Why does typedo succeed? What does 'max probably do?)

(run* [q]
      (typedo [['and :- [Boolean :> [Boolean :> Boolean]]]
               ['x :- Boolean]
               ['y :- Boolean]
               ] 
              [:apply [:apply 'and 'x] 'y]
              Boolean)
      )
;=> (_.0)

The run returns a non-empty list because no goals failed. (Why does typedo succeed? What does 'and probably do?)

Polymorphism

Does our type checker support polymorphism?

(run* [q]
      (typedo [['int :- [Number :> Integer]]
               ['x :- Double]
               ] 
              [:apply 'int 'x]
              Integer)
      )
;=> ()

The run returns () because typedo returns a failed goal.

Why does typedo fail? Where does typedo fail?

Hint: (= true (isa? Integer Number))

(run* [q]
      (typedo [['int :- [Double :> Integer]]
               ['x :- Double]
               ] 
              [:apply 'int 'x]
              Integer)
      (typedo [['int :- [Float :> Integer]]
               ['x :- Float]
               ] 
              [:apply 'int 'x]
              Integer)
      (typedo [['int :- [Integer :> Integer]]
               ['x :- Integer]
               ] 
              [:apply 'int 'x]
              Integer)
      )
;=> (_.0)

The run returns a non-empty list because no goals failed.

Review

In what situations does run* return an empty list?

In what situations does run* return a non-empty list?

Interlude: Logic variables

A logic variable is a lexically scoped variable that can be assigned to exactly once after it is "fresh".

A fresh variable is conceptually similar to a declared variable that has no useful value.

run*s first argument is a vector containing a name. The name is declared as a fresh logic variable.

run* returns a list of values assigned to q if no goals in the run fail.

(run* [q])
;=> (_.0)

A fresh variable is printed with a non-negative number prefixed by "_.".

Interlude: Unification

In logic programming, assignment and equality tests are performed by unification.

The == function is redefined to perform unification (pronouned "unify")

== is a relation; it returns the successful goal if unification is successful, otherwise the unsuccessful goal.

(run* [q]
     (== 1 1))
;=> (_.0)

1 is the same as 1, so unification succeeds.

The run returns a non-empty list of the values of q because no goals failed.

Because q is fresh, (_.0) is returned.

(run* [q]
     (== 0 1))
;=> ()

0 is not same as 1, so unification fails.

The run returns () because a goal failed. (Which goal failed?)

The Law of Fresh

If x is fresh, then (== v x) succeeds and associates x with v. (The Reasoned Schemer)

(run* [q]
     (== q 1))
;=> (1)

As q is fresh, it is associated with 1, and the expression succeeds.

No goals fail, and q is 1, so the expression returns (1)

(run* [q]
     (== 1 q)
     (== q 1))
;=> (1)

As q is fresh, it is associated with 1, and the first unification succeeds.

Order does not matter with unification. (== q 1) is identical to (== 1 q)

As q is 1, which is the same as 1, the second unification succeeds.

No goals fail, so the expression returns (1).

(run* [q]
     (== q 1)
     (== q 2))
;=> ()

As q is fresh, it is associated with 1, and the first unification succeeds.

q (which is now associated with 1) is not the same as 2, so the second unification fails.

A goal fails, so the expression returns ()

(run* [q]
      (typedo [['int :- [Double :> Integer]]
               ['x :- Integer]
               ] 
              [:apply 'int 'x]
              Integer)
      (== q true))
;=> ()

Why does this run return ()?

(run* [q]
      (typedo [['int :- [Double :> Integer]]
               ['x :- Double]
               ] 
              [:apply 'int 'x]
              Integer)
      (== q true))
;=> (true)

Why does this run return (true)?

Surprises

Why does this run return (java.lang.Integer)?

(run* [q]
      (typedo [['int :- [Integer :> q]]
               ['x :- Integer]
               ] 
              [:apply 'int 'x]
              Integer))
;=> (java.lang.Integer)

Because typedo would succeed if q was associated with java.lang.Integer. (Why?)

Why does this run return (java.lang.Integer)?

(run* [q]
      (typedo [['int :- [Integer :> Integer]]
               ['x :- q]
               ] 
              [:apply 'int 'x]
              Integer))
;=> (java.lang.Integer)

Because typedo would succeed if q was associated with java.lang.Integer. (Why?)

Why does this run return ([java.lang.Integer :> java.lang.Integer])?

(run* [q]
      (typedo [['int :- q]
               ['x :- Integer]
               ] 
              [:apply 'int 'x]
              Integer))
;=> ([java.lang.Integer :> java.lang.Integer])

Because typedo would succeed if q was associated with [java.lang.Integer :> java.lang.Integer]. (Why?)

Why does this run return ()?

(run* [q]
      (typedo [['int :- [Integer :> Double]]
               ['x :- q]
               ] 
              [:apply 'int 'x]
              q))
;=> ()

Because no values can be associated with q such that typedo succeeds. (Why?)

Multiple Variables

Logic Programming Concept: exist

exist takes a vector of names which are initialized to fresh logic variables.

When one variable is associated with another, we say they co-refer, or share. (The Reasoned Schemer, pg 9)

(run* [q]
      (exist [a]
             (== q a)
             (== a 1)))
;=> (1)

Both q and a are fresh when they are associated with eachother. q gets whatever associations a gets.

a is associated with 1, which is q.

No goals fail, so the expression returns (1).

Why does this expression return ( [java.lang.Double java.lang.Integer] )?

(run* [q]
      (exist [a b]
             (typedo [['int :- [Integer :> Double]]
                      ['x :- b]
                      ] 
                     [:apply 'int 'x]
                     a)
             (== q [a b])))
;=> ([java.lang.Double java.lang.Integer])

Because typedo would succeed if both a was associated with java.lang.Double and b was associated with java.lang.Integer. (Why?)

Why does this expression return ([ [_.0 :> java.lang.Integer] _.0])?

(run* [q]
      (exist [a b]
             (typedo [['int :- a]
                      ['x :- b]
                      ] 
                     [:apply 'int 'x]
                     Integer)
             (== q [a b])))
;=> ([[_.0 :> java.lang.Integer] _.0])

Because typedo would succeed if a was associated with [_.0 :> java.lang.Integer] and b was associated with _.0.

_.0 represents a fresh variable. The typedo would succeed if all instances of _.0 are substituted with the same (arbitrary) type.

Verify this by substituting all _.0s with a type.

Why does this expression return ( [ [_.0 :> _.1] _.0 _.1] )?

(run* [q]
      (exist [a b c]
             (typedo [['int :- a]
                      ['x :- b]
                      ] 
                     [:apply 'int 'x]
                     c)
             (== q [a b c])))
;=> ([[_.0 :> _.1] _.0 _.1])

Because typedo would succeed if

  • a was associated with [_.0 :> _.1] and
  • b was associated with _.0 and
  • c was associated with _.1.

The typedo would succeed

  • if all instances of _.0 are substituted with the same (arbitrary) type and
  • if all instances of _.1 are substituted with the same (arbitrary) type.

Verify this by substituting all _.0s with a type and substituting all _.1s with a type.

Infinite results

Why does the following expression not yield a value?

(run* [q]
     (exist [a x]
            (typedo [['f :- [Integer :> a]]
                     ['g :- Integer]]
                    x
                    Float)
            (== [x a] q)))
;

Because there are infinite values of q that satisfy typedo.

Why does the following expression yield a value?

(run 2 [q]
     (exist [a x]
            (typedo [['f :- [Integer :> a]]
                     ['g :- Integer]]
                    x
                    Float)
            (== [x a] q)))
;=> ([[:apply f g] java.lang.Float] 
;    [[:apply [:apply f g] g] [java.lang.Integer :> java.lang.Float]])

Because we requested for 2 values of q that satisfy typedo.

Verify each combination satisfies typedo.

Why does the following expression yield a value?

(run 4 [q]
     (exist [a x]
            (typedo [['f :- [Integer :> a]]
                     ['g :- Integer]]
                    x
                    Float)
            (== [x a] q)))
;=> ([[:apply f g] java.lang.Float] 
;    [[:apply [:apply f g] g] [java.lang.Integer :> java.lang.Float]] 
;    [[:apply [:apply [:apply f g] g] g] [java.lang.Integer :> [java.lang.Integer :> java.lang.Float]]] 
;    [[:apply [:apply [:apply [:apply f g] g] g] g] [java.lang.Integer :> [java.lang.Integer :> [java.lang.Integer :> java.lang.Float]]]])

Because we requested for 4 values of q that satisfy typedo.

Logic Programming Concept: conde

Why does this expression return nil?

(cond
  false true)
;=> nil

Because the question is falsy, cond falls though and returns nil.

Why does this expression fail?

(run* [q]
      (conde
        (fail succeed)))
;=> ()

Because the question fails, conde falls through and fails.

Why does this expression return true?

(cond
  true true)
;=> true

Because the question is truthy, and the answer is true.

Why does this expression succeed?

(run* [q]
      (conde
        (succeed succeed)))
;=> (_.0)

Because the question succeeds, and the answer is successful.

conde clauses have 1 question and 0 or more answers.

Why does this expression succeed?

(run* [q]
      (conde
        (succeed succeed succeed)
        (succeed fail)
        (succeed succeed)))
;=> (_.0 _.0)

The first clause succeeds because the question and the answers succeed. q is still fresh.

q is refreshed to a new fresh value. The second clause fails because the answer fails.

q is refreshed to a new fresh value. The third clause succeeds because the question and the answers succeed. q is still fresh.

At least one clause succeeds, so conde succeeds.

Two fresh values are returned, one from each successful clause.

Why does this expression succeed?

(run* [q]
      (conde
        ((== 'olive q) succeed)
        ((== 'oil q) succeed)))
;=> (olive oil)

Because (== 'olive q) succeeds, and therefore the answer is succeed. The succeed preserves the association of q to 'olive.

To get the second value we "pretend" that (== 'olive q) fails; this imagined failure "refreshes" q.

Then (== 'oil q) succeeds. The succeed preserves the association of q to 'oil.

We then pretend that (== 'oil q) fails, which once again refreshes q.

Since no more goals succeed, we are done.

(The Reasoned Schemer, Pg 11)

Since at least one conde clause succeeded, the conde expression succeeds.

Since no goals fail, the expression succeeds.

The Law of conde

To get more values from conde, pretend that the successful conde line has failed, refreshing all variables that got an association from that line.

(The Reasoned Schemer)

The "e" in conde stands for "every line", since every line can succeed.

(The Reasoned Schemer, Pg 12)

Logic Programming Concept: run n

Why isn't the value of this expression (olive oil)?

(run 1 [q]
      (conde
        ((== 'olive q) succeed)
        ((== 'oil q) succeed)))
;=> (olive)

Because (== 'olive q) succeeds and because run 1 produces at most one value of q. (The Reasoned Schemer, pg 12)

Experiment with the number of clauses and with varying the number of output values.

Why is the value of this expression (extra virgin)?

(run 2 [q]
      (conde
        ((== 'extra q) succeed)
        ((== 'virgin q) succeed)
        ((== 'olive q) succeed)
        ((== 'oil q) succeed)))
;=> (extra virgin)

Because run 2 produces at most two values.

Why is the value of this expression (extra virgin olive oil)?

(run* [q]
      (conde
        ((== 'extra q) succeed)
        ((== 'virgin q) succeed)
        ((== 'olive q) succeed)
        ((== 'oil q) succeed)))
;=> (extra virgin olive oil)

Because all clauses succeed and because run* keeps producing values until they are exhausted.

matche

matche is a syntactic variation on conde that introduces pattern matching.

The following expressions are equivilant.

(run* [q]
      (conde
        ((== 'extra q) succeed)
        ((== 'virgin q) succeed)
        ((== 'olive q) succeed)
        ((== 'oil q) succeed)))
;=> (extra virgin olive oil)
(run* [q]
      (matche [q]
              (['extra]  succeed)
              (['virgin] succeed)
              (['olive]  succeed)
              (['oil]    succeed)))
;=> (extra virgin olive oil)

matche sugar: Wildcards

matche supports wildcards with _.

(run* [q]
  (exist [a o]
    (== a [1 2 3 4 5])
    (matche [a]
            ([_]
             (== q "first"))
            ([[1 2 3 4 5]]
             (== q "second"))
            (["a"]
             (== q "third")))))
;=> ("first" "second")

The first clause matches because the wildcard matches [1 2 3 4 5]. The second clause matches because (== [1 2 3 4 5] [1 2 3 4 5] ) succeeds. The third clause fails because (== [1 2 3 4 5] "a") fails.

matche sugar: List destructuring

matche supports destructuring with ..

(run* [q]
  (exist [a o]
    (== a [1 2 3 4 5])
    (matche [a]
            ([[1 2 . [3 4 5]]]
             (== q "first"))
            ([[1 2 3 . [4 5]]]
             (== q "second")))))
;=> ("first" 
;    "second")

The first clause matches because [1 2 . [3 4 5] ] matches [1 2 3 4 5] The second clause matches because [1 2 3 . [4 5] ] matches [1 2 3 4 5] The third clause matches because [1 . _] matches [1 2 3 4 5] when the wildcard is replaced with [2 3 4 5]

matche sugar: Combining wildcards and destructuring

Wildcards match the minimum possible amount to satisfy matching.

(run* [q]
  (exist [a o]
    (== a [1 2 3 4 5])
    (matche [a]
            ([[1 . _]]
             (== q "first"))
            ([[_ . o]]
             (== q ["second" o])))))
;=> ("first" 
;    ["second" (2 3 4 5)])

The _ in the second clause is guaranteed just to match 1, as that is the absolute minimum required to satisfy matching.

matche sugar: Implicit variables

matche implicitely declares variables prefixed by "?".

(run* [q]
  (exist [a o]
    (== a [1 2 3 4 5])
    (matche [a]
            ([[1 . o]]
             (== q ["one" o]))
            ([[1 2 . ?o]]
             (== q ["two" ?o]))
            ([[o . ?o]]
             (== q ["third" o ?o])))))
;=> (["one" (2 3 4 5)] 
;    ["two" (3 4 5)] 
;    ["third" 1 (2 3 4 5)]

matche declares ?o for us, and ?o acts like any other variable.

Logic Programming Concept: Disequality

Disequality constraints guarantee that two terms can never become equal. It is comparable to the inverse of unification.

!= is used to describe this relationship.

This expression succeeds

(run* [q]
      (!= q 2)
      (== q 1))
;=> (1)

because (!= q 2) guarantees q not to be associated with 2.

(== q 1) assigns q to 1 successfully.

This expression fails

(run* [q]
      (!= q 2)
      (== q 2))
;=> ()

because (!= q 2) guarantees q not to be associated with 2.

The disequality constraint causes (== q 2) to fail.

Therefore the run yields ().

typedo Implementation

We have covered enough material to present typedos full implementation:

(ns logic-introduction.core
    (:refer-clojure :exclude [inc reify ==])
    (:use [clojure.core.logic minikanren prelude nonrel match disequality]))

(defn geto [k m v]
  (matche [m]
          ([[[k :- v] . _]])
          ([[_ . ?r]] (geto k ?r v))))

(defn typedo [c x t]
  (conde
    ((geto x c t))
    ((matche [c x t]
             ([_ [:apply ?a ?b] _]
              (exist [s]
                     (!= ?a ?b)
                     (typedo c ?b s)
                     (typedo c ?a [s :> t])))))))

Walking through the plumbing

We will walk through the execution of this example:

(run* [q]
      (typedo [['f :- [Float :> Integer]]
               ['g :- Float]
               ] 
              [:apply 'f 'g]
              Integer)
      )
;=> (_.0)

Our toplevel call to typedo yields these logic variable associations:

c <- [['f :- [Float :> Integer]]
      ['g :- Float]]

x <- [:apply 'f 'g]

t <- Integer

Toplevel typedo: first clause

We execute the first conde clause:

(conde
  ((geto x c t)))

We execute the function call (geto x c t), and these logic variables are associated in getos scope:

k <- [:apply 'f 'g]

m <- [['f :- [Float :> Integer]]
      ['g :- Float]]

v <- Integer

matches first clause is executed:

(matche [m]
        ([[[k :- v] . _]]))

[ [k :- v] . _] does not match with [ ['f :- [Float :> Integer] ] ['g :- Float] ] so the clause fails.

matches second clause is executed:

(matche [m]
        ([[_ . ?r]] (geto k ?r v)))

[_ . ?r] matches with [ ['f :- [Float :> Integer] ] ['g :- Float] ] when ?r is associated with [ ['g :- Float] ]

So we have a new association:

?r <- [['g :- Float]]

Review matche sugar explanation if confused about the relationship between wildcards and list destructuring.

We execute the clauses answer.

We execute the function call (geto k ?r v), and these logic variables are associated in getos scope:

k <- [:apply 'f 'g]

m <- [['g :- Float]]

v <- Integer

[ [k :- v] . _] does not match with [ ['g :- Float] ] so the clause fails.

matches second clause is executed:

[_ . ?r] matches with [ ['g :- Float] ] when ?r is associated with []

So we have a new association:

?r <- []

We execute the clauses answer.

We execute the function call (geto k ?r v), and these logic variables are associated in getos scope:

k <- [:apply 'f 'g]

m <- []

v <- Integer

matches first clause is executed:

[ [k :- v] . _] does not match with [ ['g :- Float] ] so the clause fails.

matches second clause is executed:

[_ . ?r] does not match with [] so the clause fails.

Because of these two failures, all the recursive calls of geto up to the calling code in typedo fail.

Toplevel typedo: second clause

We are reminded of the associations in the current scope:

c <- [['f :- [Float :> Integer]]
      ['g :- Float]]

x <- [:apply 'f 'g]

t <- Integer

(conde
  ((matche [c x t]
           ([_ [:apply ?a ?b] _]
            (exist [s nc]
                   (!= ?a ?b)
                   (typedo c ?b s)
                   (typedo c ?a [s :> t]))))))

The matche pattern match matches successfully because [:apply ?a ?b] is the same as [:apply 'f 'g] when ?a <- 'f and ?b <- 'g.

Entering into the clause's answer, we have these associations.

?a <- 'f   
?b <- 'g

c <- [['f :- [Float :> Integer]]
      ['g :- Float]]

x <- [:apply 'f 'g]

t <- Integer

s (fresh)

(!= ?a ?b) succeeds because ?a and ?b are not the same.

First typedo recursive call

We execute the function (typedo c ?b s)

We have these associations in scope:

c <- [['f :- [Float :> Integer]]
      ['g :- Float]]

x <- 'g

t <- Integer

We execute the first conde clause:

(conde
  ((geto x c t)))

typedo's First conde clause

Here are the associations in our scope:

k <- 'g 

m <- [['f :- [Float :> Integer]]
      ['g :- Float]]

v (fresh)

matches first clause is executed:

[ [k :- v] . _] does not match with [ ['f :- [Float :> Integer] ] ['g :- Float] ] so the clause fails.

matches second clause is executed:

[_ . ?r] matches with [ ['f :- [Float :> Integer]] ['g :- Float] ] when ?r is associated with [ ['g :- Float] ]

So we have a new association:

?r <- [['g :- Float]]

We execute the clauses answer.

We execute the function call (geto k ?r v), and these logic variables are associated in getos scope:

k <- 'g

m <- [['g :- Float]]

v (fresh)

[ [k :- v] . _] does match with [ ['g :- Float] ] when v <- Float

So the first clause is successful.

This v is the same as the toplevel s, as s is fresh. Therefore the toplevel scope has the association s <- Float.

While the other clause will match successfull once more, we already determined that if m is empty then both clauses will fail, so we don't retrace our steps, even though execution continues.

Since one clause completed successfully in geto, our first typedo clause succeeds.

typedo's Second conde clause

We are reminded of the association of x

x <- 'g

((matche [c x t]
         ([_ [:apply ?a ?b] _]
          ...)))

'g does not match with [:apply ?a ?b], so the clause fails.

We then bubble up to the toplevel typedo call, having completed successfully the first recursive call to typedo

Second recursive typedo call

We execute the function (typedo c ?a [s :> t] )

We have these associations in scope:

c <- [['f :- [Float :> Integer]]
      ['g :- Float]]

x <- 'f

t <- [Float :> (!fresh!)]

We execute the first conde clause:

(conde
  ((geto x c t)))

typedo's First conde clause

Here are the associations in our scope of geto:

k <- 'f

m <- [['f :- [Float :> Integer]]
      ['g :- Float]]

v <- [Float :> (fresh)]

matches first clause is executed:

[ [k :- v] . _] does match with [ ['f :- [Float :> Integer] ] ['g :- Float] ] when v <- [Float :> Integer]

As we have seen previously, geto will continue to recursively scan the environment list, even though we have found a match. It will eventually fail.

vs new association replaces its fresh variable with Integer.

This fresh variable is the same as t from the toplevel typedo.

Since a clause is successful, the call to geto is successful.

typedo's Second conde clause

We are reminded of the association of x

x <- 'f

((matche [c x t]
         ([_ [:apply ?a ?b] _]
          ...)))

'g does not match with [:apply ?a ?b], so the clause fails.

We then bubble up to the toplevel typedo call, having completed successfully the first recursive call to typedo

typedo Toplevel finish

We are reminded of our current scope:

?a <- 'f   
?b <- 'g

c <- [['f :- [Float :> Integer]]
      ['g :- Float]]

x <- [:apply 'f 'g]

t <- Integer

s <- Float

The second clause of our toplevel typedo conde finishes successfully. There is no more work to be done, so typedo returns the successful goal.

Toplevel run

We are reminded of our toplevel run:

(run* [q]
      (typedo [['f :- [Float :> Integer]]
               ['g :- Float]
               ] 
              [:apply 'f 'g]
              Integer)
      )

The typedo call expands to succeed

(run* [q]
      succeed
      )

The run is successful, and q is still fresh, so it is printed as a fresh variable.

(_.0)

Advanced uses

Clone this wiki locally