Loading...

​​chalk-engine lecture 2019.04.22

​​Topics for today

• ​​chalk-engine crate

• ​​New Formulation of Tabled Resolution With Delay

• ​​Author: Terrance Swift

• ​​Published: EPIA ’99

• ​​today:

• ​​finding answers and ‘positive reasoning’

• ​​next time:

• ​​negative reasoning — p :- not q​

​​Terminology

• ​​Proposition — Option<u32>: Sized​

• ​​Sized(Option<u32>)​

• ​​Name(type)​

• ​​thing that can be proven and unified together

• ​​Query ?- Sized(Option<u32>)​

• ​​ask for answers

• ​​answers have the form “yes — with a substitution for any variables”

• ​​?- Sized(Option<X>)​

• ​​Yes, if X = u32​

• ​​Yes, if X = f32​

• ​​Yes, if X = Option<u32>​

• ​​Goal — proposition that you are trying to prove

• ​​Clause — proposition that you assume to be true

​​Example Program 

​​

​​Copy(u32) :- (empty list). // impl Copy for u32 { }

​​Copy(f32).

​​Copy(Option<T>) :- Copy(T). // impl<T> Copy for Option<T> where T: Copy

​​

​​Solver concept

​​

​​"X-clause" (ExClause)

​​


​​Goal :- DelaySet | Subgoals

​​


​​forest of trees of ex-clauses

​​Initial state

​​

​​?- Copy(u32)​

​​

• ​​Copy(u32) :- <empty-set> | Copy(u32)​

• ​​Copy(u32) :- <empty-set> | <empty-set>​ // “answer"

• ​​Copy(f32)​ — fails to unify

​​Example 2

​​

​​?- Copy(Option<u32>)​

​​

• ​​Copy(Option<u32>) :- | Copy(Option<u32>)​

• ​​Copy(Option<u32>) :- | Copy(u32)​