chalk-engine lecture 2019.05.06
Follow-up notes and clarifications are in the Zulip topic for this lecture

The high-level idea

  • “Table”
  • current state of solving for some query
  • Query = Env |- Goal
  • Goal :=
  • “domain goal” Implemented(T: Trait)
  • Goal && Goal
  • Clause => Goal
  • callback for domain goals:
  • “to solve this goal G in that environment E, here are the options”
  • chalk#216 implemented this callback in chalk-solve
  • Tabling

What we don’t do — traditional prolog solver

foo(X) :- bar(X), baz(X).

bar(11).
bar(22).

baz(22).
Traditional prolog solvers used DFS:
  • ?- foo(X)
  • bar(X)
  • X = 11
  • baz(11) → fail
  • X = 22
  • baz(22) → succeeds

One particular problem that is very hard to solve without tables: infinite loops

foo(X) :- foo(X).
foo(X) :- bar(X).
bar(22).

?- foo(X)
  • one possible answer: X = 22

chalk-engine tables


  • Table:
  • Query: Env, Goal
  • in canonical form
  • Answers
  • Strands (“a possible way to find an answer”)
  • Substitution — current value for all the variables in the env/goal
  • to start, this is an identity mapping
  • more precisely, there is a 1-to-1 mapping between our canonicalized goal type variables and a type variable in our inference context
  • ?A := ?A