►
From YouTube: How the chalk-engine crate works
Description
A discussion of how the chalk-engine crate works.
A
A
A
Probably
won't,
hopefully,
we'll
get
through
everything
today
because
they
didn't
finish
preparing
everything
so,
but
what
I
will
try
to
talk
about?
Our
main
focus
was
to
talk
about
this,
the
chalk
engine
great
first
and
foremost,
and
some
of
the
sort
of
foundational
concepts
that
it's
based
on
in
particular,
there's
a
paper
hold
on
a
second
here.
A
There
we
go
so
there's
a
paper
if
I
can
change
windows
successfully.
Yes
called
a
new
formulation
of
tabled
resolution
with
delay
very
catchy
title
that
kind
of
covers
the
concepts
in
a
sort
of
conceptually
elegant
way,
although
it
doesn't
give
you
much
information
about
how
to
put
it
into
practice,
and
so
one
of
my
goals
here
is
to.
A
This
is
the
paper.
One
of
my
goals
is
to
kind
of
make
some
connections
between
the
terminology
in
this
paper
and
the
pardon
what
the
code
itself
actually
does
and
I
think
today,
if
all
goes
to
plan,
will
cover
the
kind
of
easy
part
of
how
this
works,
which
is
to
say
this
sort
of
positive
part
of
find
any
answers
and
we'll
see
a
little
bit.
What
happens
when
there
could
be
an
infinite
set
of
answers
and
so
on.
A
A
I'm
gonna
bring
my
secret
paper
just
a
little
bit
of
a
plan,
all
right,
so
first
I
want
to
do
a
little
terminology
for
anything
else.
Probably
many
of
you
have
heard
these
turn
out
just
terms,
but
it's
always
good
to
be
sure.
We're
saying
you
mean
the
same
things.
The
first
thing
is
I.
Think
people
usually
call
this
a
proposition.
A
It's
basically
something
that
can
be
proven.
True,
so
like
in
rust
terms.
This
might
be
something
like
option
of
a
few
thirty-two
is
sized,
but
the
notation
that
I'll
be
using
today
would
be
more
like
this
and
in
general
you
would
have
something
like
I,
don't
know,
I
don't
have
to
call
this
the
name
of
the
proposition
and
then
some
some
term,
some
type
in
here
in
the
full
it
in
the
full
choc
D
sugaring.
There's
like
a
bunch
of
more
complex
things
here,
but
we
don't
actually
care
for
the
purposes
of
choc
engine.
A
And
it
means
something
you
it's
basically
the
outside
when
you
request
answers,
this
is
the
the
thing
you're
looking
for
answers
to,
and
answers
would
be
like
both
a
result
of
yes,
meaning
it
is
true
and
then
with
a
substitution
for
any
variables.
So
in
this
case
there
are
no
variables,
this
particular
example,
so
there
would
be
no
substitution.
This
is
just
true
or
false.
A
In
which
case
an
answer
might
be
yes,
if
X
is
youth,
are
you
doing
and
there
might
be
other
answers
like?
Yes,
if
X
is
32
and
in
fact,
there's
kind
of
an
infinite
series
of
answers
here,
because
you
could
have
option
of
you
32
like
an
option
option
and
so
on.
So
we'll
come
to
that
problem
a
little
bit
and
how
we
think
about
that.
But
that's
the
basic
idea
of
a
query,
and
so
from
the
point
of
view
of
chalk
engine.
A
This
part
of
the
code
that
I'm
going
to
cover
today
at
least
depends
how
far
I
get
we're.
Basically
just
giving
a
series
of
answers.
It's
somebody
else's
problem
to
decide
if
they
want
more,
how
many
they
want
and
so
on,
and
the
code
kind
of
has
like
an
iterator
like
ylan.
So
you
can
stop
at
any
temple
and
the
last
two
thing
not
too
relevant
today
that
usually
helpful
term
a
goal.
The
goal
is
just
a
proposition
a
little
bit
more
general
than
this,
but
basically
it's
a
proposition
that
you
are
trying
to
prove.
A
So
what
you're,
trying
to
figure
out
and
the
clause
with
the
proposition
that
you
assume
to
injure
any
questions
on
that
basic
terminology?
Okay,
so
so,
let's
see,
let's
give
an
example,
so
here's
a
little
probiem
in
prologue
e
/
rusty
quasi
syntax-
this
might
have
come
from
so
in
the
level
of
we're
operating
out
here,
we're
really
quite
just
separated
from
rusts.
You
know
notions
of
traits
and
impulse,
but
of
course
this
might
have
come
from.
A
So
it
says
copy
is
true
for
option
of
T
if,
if
copy
is
true
for
T
and
there's
kind
of
an
implicit
like
for
all
T
here
that
I'm
not
gonna
write
because
it's
tedious.
So
this
is
our
example
program
that
we'll
be
working
with
to
the
most
part
and
the
actually
I,
don't
think
we'll
actually
get
to
clone.
So
maybe
we
don't
even
need
that
just
look
at
copy
it's
enough.
So
now
we
want
to
be
able
to
take
queries
like
well
like
a
very
simple
query,
might
be
something
like.
A
And
we
want
to
be
able
to
get
an
answer
out
from
this
yeah,
that's
kind
of
the
topic
of
today.
How
do
we
evaluate
these
queries?
How
do
we
come
up
with
answers?
However?
Many
there
are
and
so
on,
and
that's
exactly
what
this
paper
is
kind
of
about,
and
it's
based
on
this
idea,
where
the
idea
is
that
you
have
a
solver
or
the
solver
is
kind
of
represented
as
a
tree.
Sorry,
a
forest
of
trees.
A
The
state
of
the
solver
is
represented
as
a
forest
of
trees,
and
each
of
these
trees
is
like
some
thing,
you're
trying
to
prove
in
different
ways.
You
can
prove
it,
and
so
the
the
nodes
in
these
trees
have
a
particular
form.
That's
called
well
I'm,
calling
it
an
X
in
some
of
the
papers
is
called
an
x
clause
for
some
reason
and
I'm
keeping
up
with
that
terminology.
A
It's
actually
not
called
Ben's
particular
paper,
but
the
the
structure
of
this
clause
looks
like
well,
it's
kind
of
the
goal
that
you're
trying
to
prove
and
something
called
a
delay
set,
and
then
something
called
the
sub
goals
so
well
we're
not
gonna
get
to
the
delay
set
today.
This
has
to
do
with
negative
reasoning,
but
all
of
these
things
are
propositions,
so
something
might
be
like
you
might
imagine
if
we
were
trying
to
copy
not
not
for
this
particular
example.
A
But
let's
come
back
to
this
over
concept,
you
might
imagine
if
we
were
trying
to
figure
out
if
option
of
u
32
were
copy
and
somewhere
along
the
line.
We're
gonna
wind
up
in
a
state
kind
of
like
this,
which
is
saying
I,
can
prove
that
option
of
u-32
is
copy
if
I
can
prove
that
copy
of
u32
is
true.
Okay,
we'll
come
back
to
so
so
these
X
causes
there's
like
a
forest
of
trees
of
expose
as
possible,
and
the
idea
is
that
we
have
this
initial
State.
A
The
initial
state
is
going
to
take
the
query.
So
let's
say:
let's
use
our
simple
or
really
simple:
query
copy
of
you
32.
The
initial
state
is
we're
gonna
make
a
tree
that
looks
like
this
and
now
what's
going
on
here.
So
first
of
all,
there's
an
empty
set
of
delay
clauses
here,
that's
what
that
pipe
is
and
right
now,
we'll
always
just
see
the
pipe
as
an
empty
set,
and
then
this
is
like
the
stuff
we
have
yet
to
prove.
A
So
this
root
node
is
a
little
bit
weird,
because
we're
basically
saying
it's
always
the
same
thing
in
the
root
node,
we're
they
here's
the
thing
we're
trying
to
prove-
and
we
haven't
proven
anything
yet
so
we'll
put
this
here.
Okay-
and
this
is
gonna-
be
a
tree,
so
I'm
actually
can
I
represent
it
as
a
list
either
way
feel
free
to
interrupt
me
and
ask
questions.
A
A
So
if
we
go
to
our
program,
we
have
three
ways.
We
can
prove
that
we
know
that
copy
is
true
for
you
32.
We
know
that
it's
true
for
F
32,
and
we
know
that
it's
true
for
option
of
T
as
long
as
it's
also
true
for
T
for
any
T,
so
we
can
try
to
apply
those
and
the
way
we
apply
them
is
we
take
the
thing
we're
trying
to
prove
here
in
this
proposition
and
we
unify
it
with
with
the
sort
of
head
of
this
clause
here
right
and
so
sometimes
that
succeeds.
A
That's
great.
In
this
case,
it's
only
gonna
succeed
once
which
is
with
the
copy
of
you
32
at
the
top,
so
we're
gonna
add
a
node.
Then
it
says:
okay,
it's
gonna
look
kind
of
similar
as
the
same
it
has
the
same
goal,
but
what
comes
here
would
be
all
the
conditions
we
have
yet
to
prove
based
on
this
particular
rule.
Now,
in
this
case,
there
are
none,
because
this
format
basically
means
we
can
prove
copy
of
you
32.
If
we
prove
these
sub-goals,
when
there
are
none
to
prove
we
just
end
up
with
this.
A
Okay-
and
this
is
a
this-
is
a
child.
So
now
we
have
a
tree.
This
is
the
root
node
in
the
tree.
This
is
its
child.
We
don't
add
any
rules
for
like
the
copy
of
f/32
rule.
For
example,
we
can't
unify
copy
of
you
32
and
copy
of
F
32,
because
you
32
an
F
32
are
different
types
and
same
for
this
rule,
so
we
get
exactly
one
child
and
this
child
is
kind
of
special
because
it
has
no
goals
left
to
prove.
So
we
call
that
an
answer.
A
Basically,
we
just
now
proved
that
rule
you
32
is
copy
and
we
proved
it
by
saying.
Oh
well,
there's
a
rule
that
says
you
32
is
comfy,
so
that's
like
a
example.
That's
so
trivial,
it's
almost
kind
of
confusing,
because
it's
so
trivial,
but
this
is
the
general
shape
of
what
we're
going
to
do.
Is
we're
going
to
start
with
these
trees?
A
B
A
Will
I?
Oh
yes,
I
will
so
the
answer
is
that
each
each
tree
corresponds
to
sort
of
some
query
that
we're
trying
to
prove
right,
and
in
this
case
the
queries.
Let
me
just
me
just
work
it
out
and
I'll
show
you,
but
basically,
as
we
encounter
different
kinds
of
predicates
with
different
sets
of
variables,
we're
gonna
create
new
trees
to
represent
them.
But
let's,
let's
make
an
example,
suppose
that
we're
trying
to
prove
so
example,
number
two.
A
Suppose
I
were
trying
to
prove
copy
of
option
user.
This
is
a
little
more
complex.
So
again,
we're
gonna
follow
the
same
procedure,
we're
going
to
start
with
a
root
node
that
is
just
or
equal
to
itself.
That's
the
thing
we're
trying
to
prove
and
we're
gonna
elaborate
it
by
adding
by
using
the
program
clauses
and
we
go
up
here.
We
can't
use
this
one
because
option
and
u-32
are
different
types.
We
can't
use
this
one
because
I
left
32
an
option
or
different
types,
but
we
can
use
this
one.
So
when
we
unify.
A
So
we're
going
to
apply
the
rule
okay,
and
when
we
try
to
unify
option
of
you
32
an
option
of
T,
we
see
we
need
a
substitution
that
says.
Okay,
we
can
do
that
if
T
is
U
32
right,
so
we
have
some
substitution
that
goes
from
this
from
this
rule,
to
the
one
we're
trying
to
prove,
and
so,
when
we
do
that,
we
we
apply
that
substitution
and
we
wind
up
with
a
child
that
says
copy
adoption
32.
A
A
A
So
right,
so
this
is
the
tree
we
had
now
we
started
with
the
root
node,
we
added
a
child,
and
this
is
not
unlike
before
this.
Child
still
has
a
list
of
goals.
So
it's
not
an
answer
yet
right
now
we
need
to
figure
out
what
do
we
do?
How
do
we
prove
that
sub
goal
copy
of?
U
32
and
the
answer
is
this
is
where
the
forest
comes
in,
because
now
we
go
looking
for
some
other
for
some
tree
where
this
is
the
label.
A
This
is
the
goal
of
that
tree
that
it
was
trying
to
prove-
and
we
don't
have
a
tree
like
that.
Yet
because
this
this
tree
is
trying
to
prove
four
options,
and
this
one
is
asking
for
integers.
That's
a
different
question.
You
would
add
another
tree
and
just
like
before
the
root
node
of
the
tree
is
always
kind
of
the
same
thing
twice
and
now
we're
actually,
interestingly,
this
is
the
same
tree.
We
just
did
here
right,
so
we
can
do
the
same
step
of
will
apply
the
program.
Clause
rule
we'll
end
up
with
this.
A
A
Why
not
just
keep
writing
down
every
everything
in
the
sub
tree
has
to
be
working
towards
this
thing
for
some
instantiation
of
this
course,
so
good
lettuces.
This
is
working
towards
a
different
goal
like
when
we
produce
the
answers
we
get
here
are
going
to
be
our
answers.
That
proves
that
you
32
is
copy.
A
A
Okay,
so
the
unification,
it's
basically
the
rustic
type,
the
quality
rules
in
this
case,
but
in
in
Prolog
rules.
Normally
it
would
just
be
basically
the
same
string.
You
means
like
they're,
the
they're
the
same
alright,
so
the
same
string
u-32
it
after
two
are
not
the
same
string
and
there's
no
variables
in
it.
So
they're
not
equal.
A
So
let
me
present
so
soon
j2
coming
back
to
this
question
of
like
why
are
these
different
trees?
Maybe
it's
helpful
to
say
that?
Well,
when
we
get
to
the
actual
code,
there's
actually
a
slightly
different
name
for
these
trees.
That
I
was
using.
That
comes
from
some
other
text
called
tables,
but
the
idea
is
basically
each
one
corresponds
to
yeah
some
goal
that
we
were
trying
to
prove
right
and
they
are
they're
interdependent
with
one
another,
because
proving
one
goal
requires
proving
another.
A
But
when
you
create
them
this
way,
often
these
things
can
be
really
complicated
and
there
might
be
cycles
back
and
forth,
and
this
allows
you
to
kind
of
cache
answers,
also
between
queries
and
so
forth.
So
if
you
put
everything
like
these
trees,
they
sell
seems
very
abstract,
I
guess,
but
it
does
correspond
pretty
closely
to
the
code
and
the
essentially
it's
just
how
you
organize
the
answers.
A
C
A
Like
this
is,
if
you
another
way
to
look
at
it,
it
also
it
comes
up
when
you
have
recursion
to
prevent
infinite
recursion.
So
when
I
mentioned
that,
like
there's
an
infinite
set
of
answers
and
we'll
see
later,
that
part
of
the
having
these
trees
allows
us
to
produce
that
infinite
set
of
answers
correctly.
So
in
contrast,
I
would
have
to,
in
contrast,
like
a
traditional
four
locks
over,
doesn't
have
any
trees
in
its
state.
A
It
only
has
a
stack,
the
things
that
it's
trying
to
prove
and
it
can
easily
go
into
an
infinite
loop
and
never
produce
any
answers.
So
well,
I'll
come
back
to
that,
and
maybe
that
will
help
clarify
it.
But
let
me
give
one:
let
me
keep
going
the
disks
I
want
to
show
one
more
example
and
then
we'll
try
it
so
we're
now
just
taking
on
faith
that
there's
a
useful
to
have
these
trees
and
that
they
represent
different
questions
like
you
32
or
optionally
32.
A
So
at
this
point
we
have
now
two
trees,
one
of
them
references
the
other
here
and
in
the
second
tree
we
actually
have
an
answer:
node,
which
has
no
nothing.
No
work
left
to
do
so,
there's
another
kind
of
stuff
we
can
do
now
where
we
say.
Okay,
we
resolve
this
sub
goal.
We
resolve
this
sub
goal,
sorry
by
using
the
answer
here.
So
in
this
case
this
case
there's
no
variables,
so
it's
a
little
maybe
unclear,
but
we
know
that
you
thirty.
A
Basically,
we
know
that
this
is
true,
because
we
have
this
answer
that
says
it's
true
and
that's
what
we
were
trying
to
prove.
So
we
can
remove
that
from
the
list
of
work
to
do
and
we
can
have
caption
of
option.
U
32,
if
nothing
right,
because
you
use
that
answer
to
remove
this
and
now
this
is
another
interval,
and
so
now
indeed
we
know
that
option
of
u.
32
is
also
comfortable
at
this
point.
There's
nothing
left
we
can
do
in
this
tree
because
all
of
the
nodes
in
the
tree
have
answers
as
children.
B
A
The
actual
code
like
some
of
these,
this
is
sort
of
a
mathematical
formulation
and
nothing
ever
gets
removed.
It
just
gets
added,
but
the
reason
for
that
is
you'll
see
later
that
it
could
be
as
possible.
Well,
let
me
just
give
you
the
next
example:
it's
possible
to
have
many
children.
So
far,
we've
only
had
one
children
of
any
given
node,
but
it's
possible.
So
let's
do
the
next
example.
A
A
A
So
so
how
would
we
do
this
one?
So,
let's
walk
it
through,
so
we'll
make
a
treat
we'll
say:
okay,
copy
option,
you
32,
if
copy
of
sorry,
how
do
you
think
you
cut
the
adoption
of
X
you
copy
of
option
X,
and
this
is
the
first
time
that
we've
actually
had
a
variable
in
our
in
our
tree
nodes
and
I'm
being
a
little
hand
wavy
here
about
how
we
know
it's
a
variable
like.
A
So
basically,
one
of
the
steps
in
chalk
when
you
try
to
create
a
table
or
you
create
a
tree
in
the
forest.
Is
you
canonicalize
the
names
of
all
the
variables
so
that
they
start
in
this
case
I'm,
starting
from
a
and
going
BCD
like,
in
the
order
of
which
they
appear?
And
that
way,
if
you
had
multiple
queries,
that
are
all
kind
of
variations
of
this
you'll
end
up
at
the
same
tree?
A
But
one
easy
way
to
do
that
is
just
to
Nate
will
always
have
the
consistent
naming
so
copy
about
tonight
here.
So
this
is
our
estate,
and
if
we
go
back
to
our
rules,
you
know
we
can't
apply
you
32
we're
gonna,
do
the
same
thing
as
we
did
before,
and
there's
only
going
to
be
one
program
cause
we
can
apply
to
make
the
child,
which
is
we
can
apply
this
one,
the
one
we
have
the
same
as
here,
but
this
time
the
variable
t
winds
up
getting
maps
basically
to
a
right,
because.
A
A
A
So
if
we
look
at
this
like
when
we
go
down
this
path
to
proving
that
route
annuities,
we
actually
have
a
value
for
a
now
I'm
gonna
call:
okay,
I'm
gonna
call
this
B,
and
here
we
have
a
value
for
a
which
is
F
32,
and
here
we
have
a
partial
value.
We
know
that
it's
an
option,
but
we
don't
know
what
it's
not
enough
yet.
So
as
we
go
this
as
we
as
we
go
down
a
tree,
we
always
stay
with
something
that
can
be
unified.
E
D
A
I'm
gonna
come
to
map
to
the
code,
but
what
we
actually
do
here,
it's
a
good
question.
So
in
the
actual
code,
if
I
recall,
I
think
we
only
store
the
values
for
these.
We
store
two
things
in
the
table
for
tree.
We
keep
this
this
root
goal
that
we
originally
had
and
then
for
each
child
within
the
tree,
each
node
within
the
tree.
We
store
the
values
for
these
variables,
so
we
wouldn't
actually
kind
of
repeat
all
the
information
we
would
just
kind
of
keep
like
hey.
Is
your
3200
here
in
this
path?
A
That's
what
it
is
in
this
formulation
that
comes
from
the
paper.
You
can
sort
of
reproduce
that
by
unifying
the
two
of
them
and
figuring
out
what
the
substitution
is,
that
makes
them
unify
yeah
thanks
sense,
so
right
so
now
we
have
three
children
here
and
interestingly,
two
of
them
are
answers,
and
this
one
is
not
an
answer.
Node.
However,
it
is
an
instance
of
something
which
we
hadn't
seen
before,
which
is
a
cycle
which
kind
of
gets
back
to
some
of
the
questions.
2J
was
asking
I
think
but
yeah.
A
A
A
Which
comes
from
here
right,
and
so
you
can
see
that
will
never.
Actually,
if
we
keep
repeating
this
process,
we'll
never
really
reach
a
fixed
point,
we'll
just
keep
growing
the
tree
infinitely,
but
we
always
at
any
point.
We
have
a
kind
of
partial
set
of
answers.
These
are
the
answers
we
found
so
far.
D
A
A
You're
not
actually
is
not
a
matter
of
thinking
of
it.
That
way,
that's
actually
literally
what
happens
and
then,
since
it
has
the
tree,
we
can
go.
Look.
We
can
go
look
for
answers
within
tree.
The
way
that
we
handle
this
in
the
code.
We're
gonna,
I'm,
gonna,
start
mapping
now
to
the
more
concrete
code,
but
is
it's
basically
we
don't.
The
goal
is
usually
not
to
run
till
a
fixpoint
part
of
the
way
reason
I
showed
it
this
way
of
like
building
up
and
applying
these
steps.
A
One
by
one
is
that
the
goal
is
to
iteratively
produce
the
answers
and
decide
if
it
makes
sense
to
keep
going.
So
in
the
case
of
if
we
were
actually
asking
this
query
in
the
RUS
compiler,
we
know
that
we
kind
of
don't
want
to
guess
the
value
for
x.
So
if,
for
some
reason
we
haven't
figured
out
what
x
is
yet
as
soon
as
we
get
two
different
answers
that
don't
well,
they
aren't
compatible
with
one
another
like.
If
we
got
you
32,
+,
f,
32,
we
can
just
kind
of
stop.
A
A
But
this
is
one
of
the
challenges
and
we
have
also
some
safeguards
in
the
engine
that
I
don't
plan
to
get
to
today
that
basically
stop
it
from
producing.
If
things
are
getting
too
big
and
it
seems
like
we're
producing
too
many
answers,
they
start
to
just
say
like
just
produce
uncertain
values,
and
they
will
stop
it
so
that
it
always
eventually
stops.
A
Right,
so
this
is
the
way
that
the
paper
looks
at
things:
I
failed
to
reference
back
on
that
I
meant
to
I'm.
Just
gonna
show
you
real
fast
in
case
you're,
curious
to
read
it.
This
is
the
way
they
notate
things.
So
I
mentioned
there's
these
trees.
This
is
an
example
of
the
tree.
Here's
the
root
node
here
are
the
children
on
their
children
and
we
didn't
get
to
failure,
but
sometimes
you
have
failures
where
that
basically
means
this
was
not
provable.
There
was.
A
This
was
false,
so
children
can
either
yield
and
eventually
a
child
either
yield
an
answer
or
fail
and
the,
and
they
have
basically
here's
the
set
of
things
which
say
these
are
the
operations
I've
mentioned
these
three
so
far,
so,
like
program
clause
resolution
positive
return,
new
sub
goal.
These
are
the
things
where
we
say
taking
the
tree
in
what
this
is
like.
The
state
machine
transition
rules
take
the
tree.
If
this
conditions
apply,
we
can
add
a
new
node
to
the
tree.
This
is
saying
it
can
take
a
program
clause.
A
A
A
So
let
me
try
to
show
you
how
this
stuff,
this
kind
of
abstract
stuff
I've
been
talking
about,
is
represented
in
the
code
itself.
First
of
all,
the
forest
of
trees
is
in
that
type
creatively
called
the
forest
and
it
has
a
list
of
lists
of
trees,
which
I
call
tables
I
confess.
This
is
a
little
incongruous
and
a
stack.
The
stack
is
when
we're
not
actively
doing
anything.
The
stack
is
empty,
but
I
like
to
see
the
scapular
we'll
see
you
later.
A
That's
how
we
detect
cycles
for
your
question
and
we
can
just
ignore
the
stack
for
them.
So
the
list
of
tables
the
tables
is
just
a
vector
we
map
here
we
have
so
this
this
big
type.
So,
what's
going
on
here,
first
of
all
meet
step
back
this
see
in
the
chalk.
Engine
itself
is
very
generic.
It
just
thinks
about
logical
things
and
doesn't
know
anything
about
rust
and
so
on,
and
so
this
see
supplies
like
all
the
concrete
types
for
what
how
do
you
represent
a
composition?
A
How
do
you
represent
a
type,
a
kind
of
stuff?
So
in
this
case
this
you
canonical
Bowl
environment.
This
is
saying,
basically
here
we're
mapping
from
the
canonical
goal
that
we're
trying
to
prove
to
an
index
of
an
actual
table.
So
if
we
come
back
up
here,
the
canonical
goal
might
would
be
like
one
of
these
or
your
copy
of
option,
A,
something
like
that
and
that's
where
we
that's
how
we
detect.
If
you
already
have
a
table
for
that
goal,
we
can
find
the
index.
A
A
That's
like
work
to
do
and
that's
where
there
are
still
sub-goals
remaining,
and
so
when
we
have
some
intermediate
node
like
this
one.
Will
this
this
one
wasn't
was
a
case
where
we
actually
were
able
to
produce
three
different
sub
children.
I
said
what
we
would
do
is
we
would
take
that
one.
This
would
be
us
before
we
actually
produce
these
three
sub
children.
A
This
would
be
a
strand,
we
would
find
the
rules
and
we
would
produce
three
more
strands
that
need
to
be
processed
one
for
each
rule
that
we
could
apply
right
and
then
some
of
those
strands
would
get
converted
to
answers.
There's
no
more
rules
left,
maybe
all
that's
the
basic
idea.
So
so
the
strands
are
work
left
to
do
and
the
answers
are
answers
we've
already
found
and
what
we
do
is
we
have.
A
A
A
That's
not
a
term
from
from
any
paper
or
anything
so
I
think
of
it
as
a
thread,
because
what
we're
gonna
do
later,
I'm
going
to
talk
a
little
bit
about
like
the
scheduling
aspect
of
this,
the
sort
of
a
search
order,
but
ideas,
you're
gonna,
your
incremental
e
growing,
this
tree
right
and
it
kind
of
matters
the
order
in
which
we
choose
to
evaluate
how
we
choose
to
walk
the
tree.
So
the
strands
are
like
a
given
direction.
A
A
A
A
Basically
the
thing
we're
trying
to
prove
the
delayed
things
which
we
didn't
do
and
the
sub
goals
we'll
see
it
in
a
second,
and
it
consists
then,
of
a
selected
sub
goal,
which
is
basically
what
part
the
strand
is
working
on
now,
if
any
will
come
back
to
life.
So
the
let
me
talk
to
two
more
things
to
say
about
strands,
so
the
strand
is
basically
an
X
clause.
There's
a
little
bit
of
extra
state
called
the
selected
sub
goal,
but
it's
basically
with
a
label
from
one
of
those
nodes
in
the
tree.
A
And
an
X
Clause,
oh
I,
wanted
to
talk
about
the
canonical
stream,
no
I,
don't
actually
the
canonical
strand
is
just
a
strand.
That's
not
active.
That's
been
canonicalized
the
details
of
that
have
to
do
with
how
rust
rust
sees
infants
tables
work
like
why
we
need
that.
Otherwise,
you
could
just
keep
strands
as
they
were.
In
fact,
earlier
versions
didn't
have
a
notion
of
canonical
school,
so
TL
DR
doesn't
really
matter
we'll
come
back
to
India.
A
This
is
the
list
of
things
we
have
yet
to
prove
the
sub
goals.
This
is
the
list
of
delayed
literals
that
are
needed
for
negative
reasoning
that
we
haven't
used
yet,
and
this
is
the
way
we
represent,
that
the
thing
we're
trying
to
prove-
and
you
see
it's
just
a
substitution,
so
we
hope
we
don't
repeat
the
the
information.
That's
always
the
same
for
everything
within
the
table.
A
Here
is
a
gold
here
is
a
canonical
gold
G,
so,
for
example,
this
might
be
in
terms
of
our
stuff
we've
been
doing.
This
is
basically
something
like
that
and
you
can
say
give
me
answer
n
from
that
goal
and
usually
you
would
start
at
zero
and
then
you
would
go
to
one.
You
can
keep
asking
for
more
answers,
if
you
like
actually
I
think
you
actually
get
depends
on
where
you
draw
the
line.
A
Okay,
well,
this
is
where
you
get
the
iterator
to
see
it
are
over
the
answers
for
some
gold
and
it
gives
you
back
a
stream
of
answers
and
internally,
what
that's
going
to
do
is
keep
a
counter
and
it's
gonna
call.
This
method
called
ensure
answer
recursively.
So
what
this
tries
to
do
is
it
says,
given
some
goal,
that
we're
trying
to
prove
the
table,
the
table
for
some
goal
find
the
answer
number
end
and
the
reason
I
call
it
ensure
is
that
this
state
persist
between
queries.
A
A
The
first
thing
it
does
is
it
loads
the
table
that
were
which
corresponds
to
the
goal
and
it
checks.
If
there's
an
answer
already
and
if
so,
it
just
returns,
it
all
done.
Otherwise,
it
checks
for
cycles
on
the
stack.
Do
you
know
that
for
a
second?
Otherwise
it
calls
this
pursue
so
pursue
next
strand.
If
we
visualize
it,
others
might
work.
If
you
had
like,
let's
say
the
first
thing
you
did
was
you
asked
for
a
copy
of
you,
32
I
might
make
a
table
which
corresponds
to.
A
A
32
first,
it
would
have
created
the
other
table
for
coffee
32
yeah.
So
what
do
I
mean
by
ask?
What
I
mean
by
ask
is
that
you
invoke
like
at
the
outermost
level?
It
means
you
tell
the
forest
to
iterate
over
the
answers
for
that
cold
right,
but
internally
there's
it
might
ask
in
some
sense
as
well,
by
calling
Insurance,
Services
and
so
I
guess
there
are
multiple
people
who
can
be
asking,
but.
B
A
A
We've
basically
now
descended
into
some
sub
tree
and
where
we're
trying
to
take
the
next
step
based
on
its
current
state.
So
we
have
the
X
clause,
it
has
a
list
of
pending
sub
goals
that
may
or
may
not
be
empty,
and
we
want
to
examine
it
and
figure
out
what
to
do
so,
we'll
go
and
say:
okay
if
no
sub
goal
has
been
selected.
So
if
we
come
back
to
let's
actually
work,
let's
say
we
were
trying
to
do
here.
A
We
would
create
the
table
for
copy
of
a,
and
we
would
I
didn't
mention
this,
but
when
we
create
a
table
for
a
given
goal,
if
you
remember,
whenever
we
did
things
there
was
this
root.
Node
was
kind
of
special
and
then
the
immediate
children
of
the
root
node.
They
all
came
from
the
program
clauses
that
we
had
from
our
program
here,
all
right,
and
so
those
two
steps
are
kind
of
special
and
different,
because
that's
where
you
actually
load
from
the
program.
A
Results
from
the
from
the
program
clauses:
you
don't
have
to
do
it
that
way,
but
it's
convenient
to
do
it
all
at
once
and
actually
tutor
me
and
wear
your
real
name.
Sorry,
if
you
have
Lucas
any
case
that
I
call
back,
you
were
writing
that's
exactly.
What
does
this
sure?
Is
it's
exactly
where
we
get
the
list
of
things
from
so
so
we
would
be
in
a
state
like
so
where
we
have
a
table
with
three
strands.
As
soon
as
we
create
the
table,
we
would
populate
it
with
three
strands,
but
no
answers.
A
A
And
we
would
then
try
to
process
it,
and
in
this
case
it's
a
very
simple
strand
because
there's
no
answers,
so
what
we
would
say
is
first
thing
we
try
to
do
is
find
some
sub
goal
within
the
strand
to
focus
on
right
now
there
are
no
sub
goals
at
all,
so
we
you
do
that.
We
call
this
function,
pursue
answer
which
basically
means
I'm
pursuing
this
strand
to
see
if
I
release
one
answer
and
I
indeed,
I
found
in
the
answer.
There's
a
lot
of
logic
here,
but
it's
mostly
around
negative
reasoning.
A
What's
going
to
happen
in
this
case
is
because
there's
nothing
left
to
do
we'll.
Just
call
this
an
answer.
I
said
we
would
add,
then
a
equals.
U
32
to
our
list
of
answers
and
we're
done,
and
we
would
return
back
saying,
there's
answer
zero.
You
asked
for
it
now.
If
they
came
and
asked
for
answer
one,
it
would
pop
off
the
next
strand
and
process
that
which
would
get
us
a
equals.
F
32.
A
And
now,
if
they
ask
for
answer
to
this
is
where
things
get
a
little
more
interesting,
because
when
we
top
this
strand,
it
actually
has
sub
goals.
So
we
would
select
this
sub
goal
to
work
on
and
I'm
gonna
denote
that
we'll
see.
So
we
would
make
this
the
the
active
strand
like
so
you
would
sort
of
mark
this.
One
is
the
active
sub
goal
and
what
that
means
is
we're
gonna,
go
we're
gonna,
remember
our
answer
index,
which
starts
out
as
0
and
we're
gonna
go
ask
the
table
for
this
sub
goal.
A
If
it
has
an
answer
0,
which
in
this
case
is
the
same
table,
we
started
with
so
we
have
a
cycle
now
where
we're
asking
ourselves.
What
is
the
answer
0,
but
it
turns
out
you
have
an
answer
for
that,
like
you,
don't
actually
because
there's
a
cached
answer,
there
is
no
cycle,
we
don't
to
worry
about
the
cycle.
We
can
supply
the
answer.
So
we'll
get
back
the
answer
a
equals,
u
32,
and
we
will
then
apply
that
to
our
strand
and
make
a
new
strand.
A
A
It
gave
rise
to
another
chain
of
reasoning
by
using
a
previous
answer,
and
if
we
keep
doing
this
well
like
if
we
pursue
this,
one
will
get
option
of
you,
32
and
so
on
and
we'll
just
keep
finding
more
answers
as
people
ask-
and
this
will
keep
growing.
Oh
I
realized
I
was
running
short
of
time,
so
I
kind
of
ran
through
this
last
part
really
fast,
but
did
that
make
sense
so
far?
Any
questions
on
that
last
part.