chalk-engine lecture 2019.04.22

# ​​Topics for today

• chalk-engine crate
• New Formulation of Tabled Resolution With Delay
• Author: Terrance Swift
• 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>)
• 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)