;;; -- Create truth table -----------------------------------------------
;;; receives a proposition p and a set of bindings I
;;; returns the binding set with the proposition on it
(define (add-to-binding p I)
(cond ((null? I) (cons (list p #f) I))
((eq? p (first (first I))) I)
(else (cons (first I) (add-to-binding p (rest I))))))
;;; receives a formula phi and an empty binding set I (empty list)
;;; returns a binding set with all the propositions in the formula
(define (binding-set phi I)
(cond ((null? phi) I)
((boolean? phi) I)
((symbol? phi)
(if (and (not (eq? phi 'not)) (not (eq? phi 'and)) (not (eq? phi 'or)))
(add-to-binding phi I)
I))
((list? phi) (binding-set (first phi) (binding-set (rest phi) I)))
(else (panic "Invalid formula"))))
;;; receives a proposition p and a set of bindings I
;;; returns the value of the proposition
(define (lookup p I)
(cond ((null? I) (panic "Unbound proposition"))
((eq? p (first (first I))) (second (first I)))
(else (lookup p (rest I)))))
;;; receives a formula phi and a set of bindings I returns the
;;; evaluation of the formula for the given bindings
(define (evaluate phi I)
(cond
((null? phi) (panic "Invalid fromula"))
((boolean? phi) phi)
((symbol? phi) (lookup phi I))
((list? phi)
(case (first phi)
((not) (case (length phi)
((2) (not (evaluate (second phi) I)))
(else (panic "'not' takes one argument"))))
((and) (case (length phi)
((1) #t)
((2) (evaluate (second phi) I))
(else (if (evaluate (second phi) I)
(evaluate (cons 'and (rest (rest phi))) I)
#f))))
((or) (case (length phi)
((1) #f)
((2) (evaluate (second phi) I))
(else (if (evaluate (second phi) I)
#t
(evaluate (cons 'or (rest (rest phi))) I)))))
(else (panic "Invalid formula"))))
(else (panic "Invalid formula"))))
;;; receives a set of bindings I
;;; returns whether there exists a new row
(define (exists-next-row? I)
(if (or (null? I) (null? (first I)))
#f
(not (reduce (lambda (m n) (and m n)) (map second I) I))))
;;; receives a set of bindings I
;;; returns a list of bindings with the next row (wraps around)
(define (next-row I)
(cond
((null? I) I)
((null? (first I)) I)
((eq? (second (first I)) #f)
(cons (list (first (first I)) #t) (rest I)))
((eq? (second (first I)) #t)
(cons (list (first (first I)) #f) (next-row (rest I))))
(else (panic "Malformed binding"))))
;;; receives a formula phi and a set of bindings I
;;; returns the value of evaluating phi with I
(define (evaluate-all phi I)
(if (not (exists-next-row? I))
(list (list I (evaluate phi I)))
(cons (list I (evaluate phi I)) (evaluate-all phi (next-row I)))))
;;; receives a formula phi
;;; returns the truth table of the formula
(define (truth-table phi)
(evaluate-all phi (binding-set phi (list))))
;;; -- Compare two truth tables -----------------------------------------
;;; recevies a binding and a set of bindings I
;;; whehter I includes the binding or not
(define (binding-in-bindings? binding I)
(cond
((null? I) #f)
((eq? (first binding) (first (first I)))
(eq? (second binding) (second (first I))))
(else (binding-in-bindings? binding (rest I)))))
;;; receives two sets of bindings I1 I2
;;; returns whether all the bindings in I1 are in I2
(define (equivalent-bindings? I1 I2)
(cond
((null? I1) #t)
((binding-in-bindings? (first I1) I2)
(equivalent-bindings? (rest I1) I2))
(else #f)))
;;; recieves a row and a table
;;; returns whether when the bindings match, they produce the same result
(define (congruent-row-in-table? row table)
(cond
((null? table) #t)
((equivalent-bindings? (first row) (first (first table)))
(and (eq? (second row) (second (first table)))
(congruent-row-in-table? row (rest table))))
(else (congruent-row-in-table? row (rest table)))))
;;; receives a row and a table
;;; returns whether the row is in the table or not (just bindings)
(define (row-in-table? row table)
(cond
((null? table) #f)
((equivalent-bindings? (first row) (first (first table))))
(else (row-in-table? row (rest table)))))
;;; receives two tables table1 and table2
;;; returns whether all the rows in table1 are in table2
(define (search-each-row table1 table2)
(cond
((null? table1) #t)
((row-in-table? (first table1) table2)
(and (congruent-row-in-table? (first table1) table2)
(search-each-row (rest table1) table2)))
(else #f)))
;;; receives two truth tables table1 and table2
;;; returns whether they are equavilent or not (rows can be permutated)
(define (equivalent-tables? table1 table2)
(if (<= (length table1) (length table2))
(search-each-row table1 table2)
(search-each-row table2 table1)))
;;; receives formulas phi1 and phi2
;;; returns whether the formulas produce the same truth table or not
(define (truth-tables-match? phi1 phi2)
(equivalent-tables? (truth-table phi1) (truth-table phi2)))
;;; -- Simplifies a truth table -----------------------------------------
;;; rules for boolean simplification
(define *boolean-rules*
'(((not #t) -~> #f)
((not #f) -~> #t)
((not (not phi)) -~> phi)
((and) -~> #t)
((and phi) -~> phi)
((and phi1... #t phi2...) -~> (and phi1... phi2...))
((and phi1... #f phi2...) -~> #f)
((and phi1... (not phi) phi2... phi phi3...) -~> #f)
((and phi1... phi phi2... (not phi) phi3...) -~> #f)
((and phi1...(and phi2...) phi3...) -~> (and phi1... phi2... phi3...))
((and phi1... phi phi2... phi phi3...) -~>
(and phi1... phi phi2... phi3...))
((or) -~> #f)
((or phi) -~> phi)
((or phi1... #f phi2...) -~> (or phi1... phi2...))
((or phi1... #t phi2...) -~> #t)
((or phi1... (not phi) phi2... phi phi3...) -~> #t)
((or phi1... phi phi2... (not phi) phi3...) -~> #t)
((or phi1...(or phi2...) phi3...) -~> (or phi1... phi2... phi3...))
((or phi1... phi phi2... phi phi3...) -~>
(or phi1... phi phi2... phi3...))))
;;; receives a pattern
;;; returns whether the pattern is a variable pattern or not
(define (pattern-variable? pattern)
(member pattern '(phi)))
;;; receives a pattern
;;; returns whether the pattern is a list of variables or not
(define (pattern-list-variable? pattern)
(member pattern '(phi1... phi2... phi3...)))
;;; receives a pattern variable and a set of bindings
;;; returns what the pattern is binded to
(define (lookup-pattern-variable pattern-variable bindings)
(cond
((null? bindings) (panic "Pattern variable not found"));)
((eq? pattern-variable (first (first bindings)))
(second (first bindings)))
(else (lookup-pattern-variable pattern-variable (rest bindings)))))
;;; receives a pattern variable list and a set of bindings
;;; returns what the list is binded to
(define (lookup-pattern-variable-list pattern-list bindings)
(cond
((null? bindings) '())
((eq? pattern-list (first (first bindings)))
(rest (first bindings)))
(else (lookup-pattern-variable-list pattern-list (rest bindings)))))
;;; receives a set of bindings and a list of sets of bindings
;;; returns the list with the set appended to each of the other sets
(define (append-to-all bindings bindings-list)
(if (null? bindings-list)
'()
(cons (append bindings (first bindings-list))
(append-to-all bindings (rest bindings-list)))))
;;; receives two lists of sets of bindings
;;; returns the cross product of those lists
(define (cross-product bindings-list1 bindings-list2)
(if (null? bindings-list1)
'()
(append (append-to-all (first bindings-list1) bindings-list2)
(cross-product (rest bindings-list1) bindings-list2))))
;;; receives a pattern and an expression
;;; returns a list of bindings with the first bindings set to the input
(define (correct-list pattern expression)
(if (null? expression)
(list (list))
(list (list (cons pattern expression)))))
;;; receives a pattern and two expressions
;;; returns all the possible list of sets of bindings possible
(define (possible-combinations pattern e1 e2)
(if (null? e2)
(cross-product (correct-list (first pattern) e1)
(pattern-binding (rest pattern) e2))
(append
(cross-product (correct-list (first pattern) e1)
(pattern-binding (rest pattern) e2))
(possible-combinations pattern
(append e1 (list (first e2)))
(rest e2)))))
;;; receives a pattern and an expression
;;; returns a list of sets of bindings
(define (pattern-binding pattern expression)
(cond
((pattern-variable? pattern) (list (list (list pattern expression))))
((pattern-list-variable? pattern) (panic "Malformed pattern list."))
((and (list? pattern) (not (null? pattern))
(pattern-list-variable? (first pattern)))
(possible-combinations pattern '() expression))
((and (list? pattern) (not (null? pattern)))
(if (and (list? expression) (not (null? expression)))
(cross-product
(pattern-binding (first pattern) (first expression))
(pattern-binding (rest pattern) (rest expression)))
(list (list #f))))
((equal? pattern expression) '(()))
(else (list (list #f)))))
;;; receives a pattern and as set of bindings
;;; returns the pattern, instantiating the variable with the bindings
(define (instantiate pattern bindings)
(cond
((pattern-variable? pattern) (lookup-pattern-variable pattern bindings))
((pattern-list-variable? pattern) (panic "Malformed pattern list."))
((and (list? pattern) (not (null? pattern))
(pattern-list-variable? (first pattern)))
(if (null? (lookup-pattern-variable-list (first pattern) bindings))
(instantiate (rest pattern) bindings)
(append (lookup-pattern-variable-list (first pattern) bindings)
(instantiate (rest pattern) bindings))))
((and (list? pattern) (not (null? pattern)))
(cons (instantiate (first pattern) bindings)
(instantiate (rest pattern) bindings)))
(else pattern)))
;;; receives two bindings b1 and b2
;;; returns whether the bindings are equal or not
(define (inconsistent-binding? b1 b2)
(and (eq? (first b1) (first b2)) (not (equal? (second b1) (second b2)))))
;;; receives a set of bindings
;;; returns whether all the bindings are consistent or not
(define (inconsistent-bindings? bindings)
(some (lambda (b1)
(some (lambda (b2) (inconsistent-binding? b1 b2))
bindings)) bindings))
;;; receives a list of sets of bindings
;;; returns a valid set of bindings from the set (the first)
(define (get-valid-bindings bindings-list)
(cond
((null? bindings-list) #f)
((and (not (member #f (first bindings-list)))
(not (inconsistent-bindings? (first bindings-list))))
(first bindings-list))
(else (get-valid-bindings (rest bindings-list)))))
;;; receives a rule and an expression
;;; returns whether the rule can be applied to the expression or not
(define (applicable? rule expression)
(get-valid-bindings (pattern-binding (first rule) expression)))
;;; receives a set of rules and an expression
;;; returns the first rule that can be applied to the expression, if any
(define (first-applicable-rule rules expression)
(cond
((null? rules) #f)
((not (eq? (applicable? (first rules) expression)#f)) (first rules))
(else (first-applicable-rule (rest rules) expression))))
;;; receives a rule and an expression
;;; returns the result of applying the rule on the expression
(define (apply-rule rule expression)
(let ((bindings
(get-valid-bindings (pattern-binding (first rule) expression))))
(instantiate (third rule) bindings)))
;;; receives a set of rules and an expression
;;; returns the result of applying the rules to the expression, if possible
(define (apply-rules rules expression)
(let ((rule (first-applicable-rule rules expression)))
(if rule
(rewrite rules (apply-rule rule expression))
expression)))
;;; receives a set of rules and an expression
;;; returns the result of applying the rules to any possible subexpression
(define (rewrite rules expression)
(if (list? expression)
(apply-rules
rules (map (lambda (expression) (rewrite rules expression)) expression))
expression))
;;; receives a boolean expression
;;; returns a simplified and equivalent boolean expression
(define (boolean-simplify phi)
(rewrite *boolean-rules* phi))