Symbolic Reasoning
CSCI-534, Colorado School of Mines
Spring 2022
Li (Mines CSCI-534) Symbolic Reasoning Spring 2022 1 / 93
Copyright By PowCoder代写 加微信 powcoder
Introduction
What is Symbolic Reasoning?
Definition (Symbolic Reasoning)
Inference using symbols—abstract items which stand for something else—coupled with rules to rewrite or transform symbolic expressions.
Computer Algebra
Algebra, Calculus
Li (Mines CSCI-534) Symbolic Reasoning Spring 2 2 / 93
Symbolic Planning
Introduction
Overview and Outcomes
Symbolic Reasoning: rewriting symbolic expressions
Calculus Algorithmic:
computer algebra symbolic planning
Relate infix notations and symbolic data structures.
Understand the s-expression notation.
Apply recursion to s-expressions.
Implement algorithms for symbolic reasoning.
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
Rewrite Systems
Symbolic Expressions Reductions
List and S-Expression Manipulation
List Manipulation
Application: Computer Algebra
Partial Evaluation Differentiation
Notation and Programming
Rewrite Systems
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
Rewrite Systems
Rewrite Systems
Definition (Rewrite System)
A well defined method for mathematical reasoning employing axioms and rules of inference or transformation. A formal system or calculus.
Example (Expressions) Example (Reductions)
Arithmetic: Distributive Properties: 23
a0x+a1x +a3x x∗(y+z)xy+xz 3x+1=10 PropositionalLogic: α∨(β∧γ)(α∨β)∧(α∨γ)
(p1 ∨ p2) ∧ p3 De Morgan’s Laws:
(p1 ∧p2) =⇒ p3 ¬(α∧β)(¬α∨¬β)
¬(α∨β)(¬α∧¬β)
Progressively apply reductions until reaching desired expression.
Li (Mines CSCI-534) Symbolic Reasoning Spring 2022 5 / 93
Example: Algebra
Given: 3x +1 = 10 Find: x
Initial 3x+1 = 10
−1 3x+1−1 = 10−1
Simplify 3x = 9
Rewrite Systems
3x /3 = 9/3
How would you write a program to solve for x?
Simplify x = 3
Li (Mines CSCI-534) Symbolic Reasoning Spring 2022 6 / 93
The Cons Cell Declaration
struct cons { void ∗first;
struct cons
Rewrite Systems Symbolic Expressions
S-Expression
}; Diagram
Cons Cell Diagram
CAR / CDR / first rest
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
Abstract Syntax Infix
Function / Operator
Arguments / Operands
f(x0,…,xn)
Abstract Syntax Tree
Function / Operator
Children:
Arguments / Operands
S-Expression
First: Root, Function / Operator
Rest: Children, Arguments / Operands
(f x0 … xn)
Rewrite Systems Symbolic Expressions
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
Example: S-Expression
Rewrite Systems Symbolic Expressions
Infix Expression
3x + 1 = 10
Abstract Syntax Tree
S-expression
(= (+ (* 3 x) 1) 10)
(= (+ (*3x) 1)
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
Example: Cell Diagram S-Expression
Rewrite Systems Symbolic Expressions
(= (+ (*3x) 1)
Cell Diagram
(Mines CSCI-534)
Symbolic Reasoning
Spring 2022
List vs. Tree List
struct cons { void ∗first ;
struct treenode { void ∗first ;
Rewrite Systems
Symbolic Expressions
struct cons
struct cons
∗children ;
struct cons { void ∗first;
struct cons ∗rest ; };
Same structure
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
Data Structure, Redux
3x + 1 = 10
Cons Cells
Rewrite Systems
Symbolic Expressions
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
Exercise 1: S-Expression
2(x-1) = 4
2(x − 1) = 4 =
Rewrite Systems
Symbolic Expressions
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
Exercise 2: S-Expression
a + bx + cx2
Rewrite Systems Symbolic Expressions
a + bx + cx2 +
x c expt x2
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
Exercise 2: S-Expression
a+bx+cx2 –continued
(* c (expt x 2)))
Rewrite Systems
Symbolic Expressions
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
Rewrite Systems Reductions
3x + 1 = 10
3x + 1 – 1 = 10 – 1
3x / 3 = 9 / 3
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022 16 / 93
Evaluation Function
Rewrite Systems Reductions
eval : s-exp → R
Li (Mines CSCI-534) Symbolic Reasoning Spring 2022 17 / 93
Recursive Evaluation Algorithm
Base Case: If argument is a value: return the value Recursive Case: Else (argument is an expression):
1. Recurse on arguments
2. Apply operator to results
Rewrite Systems Reductions
Li (Mines CSCI-534) Symbolic Reasoning Spring 2022 18 / 93
Example: Evaluation
+
2 3 4 2
Rewrite Systems Reductions
eval * /
* /
, add eval eval
2 3 4 2
Li (Mines CSCI-534) Symbolic Reasoning Spring 2022 19 / 93
Example: Evaluation
2*3 + 4/2 – continued
Rewrite Systems Reductions
* /
, add eval eval
2 3 4 2
,,,
add mul eval 2 eval 3 div eval 4 eval 2
Li (Mines CSCI-534) Symbolic Reasoning Spring 2022 20 / 93
Rewrite Systems Reductions
Example: Evaluation
2*3 + 4/2 – continued
,,,
add mul eval 2 eval 3 div eval 4 eval 2
,,, add mul 2 3 div 4 2
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
Example: Evaluation
2*3 + 4/2 – continued
Rewrite Systems Reductions
, add 6 2
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
Evaluation via S-Expressions
(+ (*23) (/ 4 2)))
Rewrite Systems
Reductions
eval : s-exp → R
Li (Mines CSCI-534) Symbolic Reasoning Spring 2022 23 / 93
Rewrite Systems
Symbolic Expressions Reductions
List and S-Expression Manipulation
List Manipulation
Application: Computer Algebra
Partial Evaluation Differentiation
Notation and Programming
List and S-Expression Manipulation
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
Evaluation and Quoting Evaluation
Evaluating (executing) an expression and yielding its return value:
(fun a b c)
return value of fun
applied to a, b, and c
Returns the quoted s-expression: ’(fun a b c)
List and S-Expression Manipulation
The s-expression: (fun a b c)
’(+12)(+12) ’1 1
(quote x) x
(+ 1 2) 3 11
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
List and S-Expression Manipulation List Manipulation
Dotted List Notation
’(x y) NIL
’(x . (y z)) NIL
’(x (y z))
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
List and S-Expression Manipulation
List Manipulation
Creating Lists
Contruct a new cons cell:
(cons x y)
a fresh cons cell with x in the car (first) and y in the cdr (rest)
(cons α β) (cons 1 NIL) (cons 2 ((cons 1 NIL))
Li (Mines CSCI-534)
(α . β) (1 . nil)
(2 . (1 . nil)) Symbolic Reasoning
(1) NIL (2 1)
Spring 2022
List Function
List and S-Expression Manipulation List Manipulation
Return a list containing the supplied objects: (lista0 …an)
(list α β)
(list α β γ)
Li (Mines CSCI-534)
a list containing objects a0, . . . , an NIL
(cons α NIL)
(cons α (list β))
(cons α (list β γ))
Symbolic Reasoning
Spring 2022
Exercise: List Construction
(cons ’x ’y) (x . y)
(cons ’x ’(y z)) (x y z)
(cons ’x (list ’y ’z)) (x y z) (list (+123)) (6)
List and S-Expression Manipulation
List Manipulation
(list’(+123))
(list’∗(+22)’(−22)) (list’∗4’(−22))
Li (Mines CSCI-534) Symbolic Reasoning
Spring 2022
List Access
Return the car of a cons cell: (car cell)
the car (first) of cell (car ’(α . β)) α
Return the cdr of a cons cell: (cdr cell)
List and S-Expression Manipulation List Manipulation
the cdr (rest) of cell (cdr ’(α . β)) β
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
Example: CAR / CDR
(car ’(x . y))
(cdr ’(x . y))
(car ’(x y z))
(cdr ’(x y z))
List and S-Expression Manipulation
List Manipulation
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
List and S-Expression Manipulation List Manipulation
List Template Syntax
Backquote (‘): Create a template
‘(x0 … xn) (list ’x0 … ’xn)
‘(+a(*bc)) (list’+’a (list’∗’b’c)) (+a(∗bc))
Comma (,) Evaluate and insert:
‘(α… ,y β…)
evaluated
Comma-At Evaluate and splice:
‘(α… β…)
(append α… y
list α…
‘(+a,(∗23))
(list’+’a (*23)) (+ a 6)
(append’(+a) (list (*23) (*45))) (+a620)
Li (Mines CSCI-534)
Symbolic Reasoning Spring 2022 32 / 93
Comma (,) vs. Comma-At Comma ,: Insert
List and S-Expression Manipulation
List Manipulation
‘(1 , (list 2 3) 4)
Comma-At Splice 4)
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
Exercise: List Template Syntax
‘(1 2 ,(+ 3 4)) (1 2 7)
‘(,1 ,2 (+ 3 4))
(1 2 (+ 3 4))
‘(+ 1 ,2 ,(+ 3 4))
‘(1 2 ’+ ’3 ’4))
(1 2 + 3 4)
List and S-Expression Manipulation List Manipulation
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
Rewrite Systems
Symbolic Expressions Reductions
List and S-Expression Manipulation
List Manipulation
Application: Computer Algebra
Partial Evaluation Differentiation
Notation and Programming
Application: Computer Algebra
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
Example: Evaluation via S-Expressions
Application: Computer Algebra
(eval ’(+ (*23) (/ 4 2)))
(+ (* 2 3)
(eval ’(* 2 3)) (eval ’(/ 4 2))))
(eval ’2) (eval ’3)) (eval ’4) (eval 2))))
Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
Evaluation Algorithm
Application: Computer Algebra
1 2 3 4 5 6 7 8 9
Procedure eval(e)
if value?(e) then /* Argument is a value */ return e;
else /* Argument is an expression */ operator ← first(e) ;
arg-sexp ← rest(e) ;
arg-vals ← map (eval, arg-sexp);
switch operator do case ’+ do f ← +; case ’-do f ←−; case ’/ do f ← /; case ’* do f ← ∗;
return apply(f , arg-vals); Li (Mines CSCI-534)
Symbolic Reasoning
Spring 2022
Application: Computer Algebra
Map function Definition (map)
Apply a function to every member of an input sequence, and collect the results into the output sequence.
map : (X→Y) × Xn → Yn
input sequence
output sequence
Illustration
input sequence
output sequence
f(x0), f(x1), …, f(xn−1)
x0, x1, …, xn−1
(Mines CSCI-534)
Symbolic Reasoning
Spring 2022
Example: Map +1
λx . x + 1
(1+1, 2+1, 3+1) (2, 3, 4)
Application: Computer Algebra
(⊤, ⊥, ⊤) Li (Mines CSCI-534)
(¬⊤, ¬⊥, ¬⊤)
Symbolic Reasoning
Spring 2022
Algorithm: Map function Functional Map
Procedure map(f,s)
1 if empty(s) then /* s is empty
Imperative Map
Procedure map(f,s) 1 n ← length(s);
2 Y ← make-sequence(n); 3 i←0;
4 while i