;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Today: Logic programming
;;
;; Viewpoint #3: (best)
;; We are building a 'model' of truth. We start by
;; asserting some basic facts (axioms) -- these
;; facts are assumed to be true.
;;
;; We also specify some rules of inference which tell
;; us how to use some facts to prove other facts. The
;; process of tracing from axioms to final facts
;; (or backwards) is called deduction.
(load "query.scm")
(query-driver-loop)
;;
;; Rules
;;
;; o We can use rules to describe the relations
;; between alogirthms, their inputs, and their
;; return values.
;;
;; o Consider APPEND:
;;
;; o What can we say about the relations of Append
;;
;; 1. (append ?x ?y ?z) ; (append x y) ==> z
;;
;; 2. (append () ?x ?x) ; (append '() x) ==> x
;;
;; 3. (append (cons a x) y) == (cons a (append x y))
;;
;; -- in the logic language --
;;
;; 3. (append ?x ?y ?z) -> (append (?a . ?x) ?y (?a . ?z))
;;
;;
;;
;; o Rules for Append
(assert! (rule (append () ?x ?x)))
(assert! (rule (append (?a . ?x) ?y (?a . ?z))
(append ?x ?y ?z)))
;; o What do we have?
;;
;; o Zero how-to knowledge.
;; o We'd only be half-way there to writing this in scheme.
;;
;; o A complete description of the rules for append.
;; o Sufficient for the logic language
(append (1 2 3) (4 5 6) ?z)
;; o But, remember that logic is just syntactic!!
;; o We haven't said which are inputs and/or outputs
(append (1 2 3) ?y (1 2 3 4 5 6))
;; o In fact, we can use multiple placeholders:
(append ?x ?y (1 2 3 4 5 6))
;; o This is super cool!
;; o But it is just syntactic pattern matching:
;;
;; "Find all patterns that start with "append"
;; and end with (1 2 3 4 5 6)
;; that are deducible from the rules and axia."
;; o There are limits:
(append ?x ?y ?z)
;; o We'll explore these a bit more later:
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Arithmetic
;;
;;
;; o We can use the logic system to model arithmetic.
;;
;; o We'll cheat and use a unary representation!
;; o Can be done other bases.
;; Addition:
;; (1 1 1) + (1 1) = (1 1 1 1 1)
;; o How to do this in logic?
;; o (plus ?x ?y ?z) <===> (+ x y) = z
;; o 0 plus anything is anything.:
(assert! (rule (plus () ?x ?x)))
;; o x plus anything is 1+ (plus x-1 anything)
;; o How do we do plus-one?
;; o How do we do minus-one?
;; (plus ?x ?y ?z) ==> (plus (1 . ?x) ?y (1 . ?z))
(assert! (rule (plus (1 . ?x) ?y (1 . ?z))
(plus ?x ?y ?z)))
(plus (1 1 1) (1 1) ?x)
(plus ?x (1 1) (1 1 1))
(plus ?x ?y (1 1 1))
;; o Harder: multiplication
;;
;; o 0 times anything is 0:
(assert! (rule (times () ?x ())))
;; o (x+1) * y = x*y + y
;;
;; o So, we need a way to do x+1
(1 . ?x)
;; o and a way to do + generally:
(plus ?z ?b ?c) ;; !!
;; o Now we have to translate to
;; logic:
;;
;; 1. If x * y = z, and
;;
;; 2. y + z = temp, then
;;
;; 3. (x+1) * y = z + temp
;;
;; o In pseudologic:
(and (times (?x ?y ?z))
(plus (?y ?z temp)))
;; -->
(times (1 . ?x) ?y ?temp)
;; o In real logic:
(assert! (rule (times (1 . ?x) ?y ?temp)
(and (times ?x ?y ?z)
(plus ?y ?z ?temp))))
(times (1 1) (1 1 1) ?x)
;; Can you do exponentiation??
(assert! (rule (expr ?x () (1))))
(assert! (rule (expr ?x (1 . ?y) ?temp)
(and (expr ?x ?y ?z)
(times ?x ?z ?temp))))
(expr (1 1 1) (1 1) ?what)
;;
;; Something with words:
;;
;; o Say we wanted to censor a word out of a list:
;;
;; >(censor 'nasty '(what a nasty day))
;; (what a xxx day)
;;
;; o What are the properties of this relation?
;;
;; o The empty list is already censored:
(assert! (rule (censor ?bad () ())))
;; o If the input list begins with a bad word,
;; the output list should begin with xxx:
;;
;; o (censor ?bad ?in ?out) ==>
;; (censor ?bad (?bad . ?in) (xxx .out))
(assert! (rule (censor ?bad (?bad . ?in) (xxx . ?out))
(censor ?bad ?in ?out)))
;;
;; o Otherwise, if the first word is not bad, then
;; the output list begins with the same word as
;; the input list:
;;
;; (and (censor ?bad ?in ?out)
;; (not (same ?bad ?first))
;; -->
;; (censor ?bad (?first . ?in) (?first . ?out))
;;
;; o In logic:
(assert! (rule (censor ?bad (?first . ?in) (?first . ?out))
(and (censor ?bad ?in ?out)
(not (same ?bad ?first)))))
;; o So what does same mean?
(assert! (rule (same ?x ?x)))
;; o Try it out:
(censor nasty (what a nasty day) ?what)