►
From YouTube: how chalk-engine works, part 2
Description
Further discussion on how chalk-engine works, and some of the problems we see in practice that we have to think about how to resolve.
A
Okay,
so
I
kick
off
the
recording.
You
all
are
seeing
the
documentary
ticket
I,
hope
I'm
sharing
this,
in
other
words
this
okay,
okay,
so
I'm
gonna
kind
of
last
time,
I
kind
of
started.
In
with
this
theoretical
thing
we
got
to
talk
engine
at
the
end
and
actually,
where
did
we
leave
it?
But
I'm
probably
gonna
start
over
truck
engine
a
little
bit
because
it
never
hurts
to
say
things
twice.
A
Right,
okay,
I
see
and
then
we'll
go,
go,
go
quickly
over
those
basics
and
then
go
into
a
little
more
depth
and
one
of
the
things
I
would
like
to
get
to
if
I
get
it.
If
we
get
as
far
as
I
want
we'll
see,
we'll
talk
a
little
bit
about
delaying
and
some
of
the
other
subtle
stuff
which
truck
engine
doesn't
totally
do
correctly
right
now,
I
realize
so
right.
So
the
high-level
idea.
A
A
Guess
I
should
I
can
stay
like
this,
where
a
goal
has
an
environment
and
this
or
a
better
name
than
gold.
Let's
call
it
query
for
some
query
trade
query
where
a
query
is
an
environment
and
a
goal,
and
the
goal
is
something
like
no
emojis
something
like
either
what
we
call
a
domain
goal,
which
might
be
like,
basically,
a
predicate
like
implemented
betrayed
or
all
these
kind
of
medicals
like
do
goals
have
to
hold,
or
that,
if
you
assume
this
clause
is
true,
then
we
can
prove
that
cool.
A
These
sort
of
things
right
and
the
reason
that
we
actually
call
it
domain
goals
is
that
the
the
logic
for
these
kind
of
Combinator's
here
is
actually
built
into
the
engine,
but
the
logic
for
domain
goals
is
supplied
by
a
call
that
long
so,
essentially,
no
matter
what
kind
of
domain
this
truck
engine
is
applied
to
and
works
the
same
to
solve
two
goals.
You
saw
first,
the
one
than
the
other,
but
but
the
specifics
of
what
rules
exist
for
a
given
domain
goal
will
vary
right.
A
So,
there's
a
callback
for
domain
goals
that
gives
up
basically
to
solve
this
goal.
G
in
that
environment
e
here
are
the
options,
and
this
is
the
work
in
chalk
number
216,
that
the
true
me
was
doing.
Lucas
I
think
non
user
names
was
basically
implementing
that
callback
in
chalk
solve,
because
previously
it
only
existed
while
the
callback
existed,
but
in
a
very
simple
form
so
and
the
table
the
name
table
comes
from
this
term
called
table.
A
Ling
and
I
actually
thought
it
might
be
useful
to
talk
a
little
bit
about
how
a
traditional
Prolog
sulfur
works,
because
I
remember
there
being
some
questions
in
it
and
I
thought
it
might
elaborate
elucidate
where
the
name
comes
from
I'm
not
going
to
spend
a
lot
of
time
on
it,
but
it'll
also
be
important.
They
like,
if
you
have
a
traditional
solver,
and
it
has
some
goal
like
something
like
this.
A
This
would
be
something
that
is
real
kind
of
true,
that's
add
a
few
more
things.
The
way
this
solver
would
traditionally
work
is
it
would
go
in
a
depth
first,
it
doesn't
have
any
bollocks.
All
of
us
didn't
have
any
like
cheap
data
structures,
they're
purely
stack
based
and
what
they
would
do
is
they
would
solve
it
by
recursive.
But
if
you,
if
you
started
them
off
with
what
is
the
answer
to
foo
of
X,
they
would
find
a
rule
and
just
just
depth-first
search
and
try
to
enumerate
out
ways
that
rule
could
be
true.
A
So
first
it
would
go
into
bar
all
right,
say:
okay,
let's
solve
bar
of
X,
and
then
it
would
go
through
these
rules
and
say:
aha
well,
here's
one
way
bar
of
X
can
be
true
if
X
is
11
all
right
and
then
it
would
kind
of
pop
back
and
say:
okay,
if
we
know
now,
we
have
a
solution
for
bar
of
X.
Let's
look
at
Baz
of
X,
and
so
now
we
know
X
is
11,
so
we
would
search
for
Baz
of
11.
A
A
I
need
to
keep
things
on
the
stack
for
a
little
longer,
but
well,
not
really
that
actually
I,
don't
think
Prolog
solvers
and
their
traditional
form
ever
kept
things
in
the
stack,
but
they
would
just
have
to
need
to
save
checkpoints
in
restore
as
they
search,
but
they
could
wind
up
doing
quite
a
lot
of
work
and-
and
there
was
one
particular
problem
that
is
really
hard
to
solve.
Unless
you
make
tables.
B
A
This
is
a
very
naive
one.
This
will
be
an
infinite,
an
infinite
loop
for
a
pool
locks
over,
because
what
it
would
do
is,
it
would
say,
I
have
to
solve
foo
of
X.
Well,
let
me
solve
foo
of
X
and
that
pushes
another
thing
on
the
stack.
So
it's
just
like
a
function
calling
itself
it's
gonna,
be
cursed
forever
for
a
traditional
Prolog
sober
and
what
tables
basically
would
do
is.
A
So
if
we
have
this
set
of
rules,
there's
only
one
real
answer
here,
which
is
X
must
be
22.
So
if
I
ask
like
what
are
all
the
X's
for
which
foo
of
X
is
true,
it
has
to
be
22
because
at
least
if
X
is
inductive,
because
this,
this
kind
of
is
an
infinite
loop
right.
There's
no
answer
coming
out
of
here
that
the
only
answer
that
you
would
have
would
be
an
infinite
proof
tree.
That's
like
you
could
serve.
A
It
will
never
terminate,
but
if
X
is
but
on
this
option
we
can
prove
the
bar
of
22
is
true
right
there
and
therefore
foo
of
X
is
true,
so
we
have
a
little
sort
of
proof
for
that.
There's
only
really
one
possible
answer
22,
but,
as
I
said,
our
traditional
products
over
will
actually
just
loop
forever,
instead
of
giving
us
that
answer
because
it
gets
stuck
here.
A
A
A
Just
that
actually
I'm
gonna
stop
this
I'm
realizing
I'm,
going
way
down
into
how
tabeling
works,
and
it's
kind
of
not
that
important,
because
this
is
how
the
we'll
sort
of
see
it
through
the
way
a
chalk
engine
does.
It
was
just
a
little
different,
but
basically
there's
this
way.
There's
this
version
of
Prolog
solvers
called
tabling,
and
the
idea
was
that
they
added
a
side
table
of
answers
and
they
handled
recursion
more
elegantly,
which
is
exactly
what
the
chocolate
is
doing.
A
A
Clinton
here,
I'm
gonna
use
it
I'm
using
this
question
mark
zero,
because
the
idea
is
this
is
a
canonical
goal,
which
means
we've
renumber
sort
of
renamed
all
the
variables
in
the
canonical
ordering
and
I'm
gonna
give
them
numbers
to
make
that
clear.
I
think
before
I
used
letters
the
alphabet,
so
the
idea
would
be
that
these
know.
What's
the
difference.
A
A
A
Okay,
and
so
the
straight
has
this
substitution
and
what
else
does
it
have?
Let's
try
to
get
it
right
right,
the
X
clause
and
yeah.
So
one
thing
I
realized
I,
didn't
fully
explain
before.
So
it
has
the
X
clause
which
basically
contains
the
delay
set
and
ignore
for
the
moment
and
the
sub-goals
we
have
yet
to
prove.
A
It
can
either
not
yet
have
started,
searching
through
a
particular
sub
goal
for
answers,
or
it
can
have
started,
in
which
case
it's
waiting
enough
of
the
selected
sub
goal
is
distinguishing.
So
if
we
come
back
to
our
example,
let's
say
we
were
trying
to
solve
solving
clone
of
question
Marty.
We
would
to
start,
we
would
create
the
table
because
in
the
very
beginning
we
don't
have
any
tables
yet
right.
A
So
we're
gonna
create
a
table
for
clone
of
question,
mark
T
and
create
the
initial
set
of
strands,
and
to
do
that,
we're
going
to
use
our
callback
to
figure
out
way
to
solve
the
main
goal.
So
the
thing
is
we're
solving
a
domain
goal
clone
of
T,
and
we
don't
know
what
the
ways
are
to
solve
the
main
goals.
So
we
use
the
callback,
it
will
tell
us.
There
are
two
possibilities:
either.
A
A
A
For
doing
this
rule
we
basically
have
have
a
sub-goal
list
of
clone
of
question
mark
x,
and
no,
this
isn't
quite
right,
I'm,
sorry!
So,
looking
at
this
goal,
the
first
thing
we
see
is:
we
have
Veck
of
t
in
here
right,
so
we
know
we're
trying
to
of
the
shippi
day
trying
to
solve
clone
of
questionmark
day.
We
have
this
rule
for
how
to
prove
it.
So
we
have
to
unify
BEC
of
T.
A
B
A
A
A
A
What
happens
with
string
1
then,
is
we
the
current
the
current
state
is.
It
does
not
have
a
selected
sub
goal
so
when
you're
in
a
strand,
what
you
want
to
do
is
you
always
want
to
either
you're
in
it
you
either.
You
have
no
nothing
left
to
prove,
or
else
like
there.
The
sub
goal
list
is
empty,
in
which
case
you're
your
an
answer,
or
you
have
to
select
one
of
those
sub
goals
and
start
drawing
answers
from
it.
A
A
A
A
A
We
had
to
solve
clone
of
T,
but
that
kind
of
required
us
to
solve
what
we
were
already
solving
so
we're
a
little
bit
stuck,
but
it
could
happen
that
we
could
find
answers
through
another
route
right
in
particular
this
one.
So
what
we
do
in
the
event
where
we,
where
it's
already
on
the
stack,
is
we're
going
to
pause
this
strand,
basically
and
I'm,
going
to
show
exactly
others
we're
I'm,
trying
to
give
a
high-level
feeling
we're
gonna
pause,
this
strand
and
pop
back
up
until
we
get
to
the
head
of
this
cycle.
A
So
that
means
that
we're
basically
done
so
in
the
case
of
strand
two
we'll
say
no
sub
goals.
This
is
an
answer,
but
we'll
add
it
to
our
answer
list
and
we're
going
to
return.
So
the
current
state
now
of
the
table
is
that
it
has
an
answer
which
is
question:
mark
dead,
equals,
u
sighs
and
it
has
actually
I
think
the
way
that
the
solver
works.
It
would
actually
have
an
empty
list
of
strands
at
this
exact
moment,
and
that's
because
we
took
this
other
strand,
then
we
put
it.
A
You
know
we're
holding
it
to
the
side
at
the
moment,
so
it's
not
in
the
table,
it's
in
this
this
list
of
cycles
and
then,
when
we
return
back
out
when
we
return
back
out
to
this
point
of
ensuring
the
answer,
we're
going
to
say.
Okay,
we
found
an
answer
0,
let's
take
those
strands
that
were
cyclic
and
we'll
put
them
back
in
the
table
now
because
it
might
be
didn't
they.
We
tried
them
before.
A
We
had
an
answer
0
and
we
hit
a
cycle
right,
but
maybe
now
that
there
is
an
answer
0
they
will.
They
will
actually
be
you
well
so
we'll
put
them
back
in
the
table.
So
we're
gonna,
add
strand
one
back
into
the
table
and
that's
where
we
leave
this
first
sort
of
round
is
that
we
have
a
table
which
is
solving.
A
A
Which
is
this
sort
of,
like
maybe
question
mark
day,
is
back
of
question
mark
X,
but
then
we
have
to
prove
clone
of
question
mark
X.
So
when
do
we
check
that
that's
a
factor
of
cyclic
strands?
When
do
we
check
that?
It's
when
do?
What
do
we
do
with
this
vector
of
cyclic
strands?
Is
that
the
question
yeah?
At
which
point?
Do
we
actually
check
it?
A
So
in
this
case
we're
gonna,
add
the
cyclic
strands
back
into
the
table,
because
we
found
an
answer:
I'm,
not
sure
what
you
mean
by
check
it
like.
How
did
we
determine
that
it
was
a
cycle
in
the
first
place
now,
what
one
do
we
pop
it
out
to
them?
Okay,
I
see.
That
would
be
the
next
thing,
a
man.
That's
we
don't
we
don't,
basically
not
so
far,
because
we
found
our
first
answer
and
all
we
were
asked
for
was
one
answer
and
we
found
it.
A
A
Another
answer,
for
this
particular
query
know
is
when
we're
gonna
pop
this
strand
back
out
again,
because
now
we'll
say
well,
we've
only
have
we
don't
have
an
answer,
one
so
far,
but
we
still
have
ways
to
make
new
answers.
So,
let's
pop
out
this
strand,
right
and
and
actually
I
left
one
little
bit
incomplete.
A
B
A
The
most
interesting
one
is
is
this:
this
is
the
index
in
our
list
of
sub
goals,
but
this
is
the
the
number
of
this
is
the
index
in
the
list
of
answers
for
that
goal.
So
if
we
come
back
here,
I
sort
of
glossed
over
this
I
said
we're.
Gonna
select
the
sub
goal,
clone
of
twitten
of
question,
mark
X
right
and
what
that
means
is
our
selected
sub
goal.
Value
is
going
to
be
essentially
a
pair.
The
actual
data
structure
has
a
few
more
things,
but
that's
sort
of
fishin
see.
A
We
want
we're
in
the
process
of
iterating
through
all
the
answers
of
this
sub
goal,
that
there
are,
because
for
any
answer
to
that,
we're
our
will
get
solved
and
we're
currently
at
answers,
your
honor,
and
so
when
we
come
back
now
we're
gonna
pop
off
what
we
called
strand
one
from
the
list
of
strands
and
activate
it
and
we're
gonna.
We
already
have
a
selected
sub
goal,
so
we're
going
to
go
to
the
selected
sub
goal,
which
is
this
one.
A
And
ask
the
table
for
answer
zero
right,
so
we're
gonna
go
and
say:
okay
for
a
clone
of.
If
we
canonicalize
clone
of
question
mark
x,
we
got
this
two
that
we
were
called
table.
Does
it
have
this?
Does
it?
What
is
the
first
answer
in
that
table?
Does
it
have
a
zero
of
the
answer,
and
the
answer
is
that
it
does
it's
you
size.
So
in
this
case
now
that
we
have
an
actual
answer,
we're
not
going
to
get
back
a
cycle
anymore.
Wait.
A
A
So
this
is
yes,
it's
kind
of
like
the
question
is
basically:
is
there
some
finite
way?
You
could
arrange
the
rules
such
that
you
would
find
an
answer.
Do
you
think
about
it
and,
like
maybe
I,
think
it
might
be
helpful?
I
find
it
helpful
anyway
to
try
to
arrange
them
when
I
try
to
show
what
I'm
saying
so
like
here
are
two
rules.
Let's
call
them
rule
one
or
no
yeah
I
already
gave
them
names,
and
so
the
question
is
like
we
can
show
clock
that
your
size
is
an
answer
because.
A
A
A
A
So
that's
what
we're
kind
of
trying
to
do
is
find
these
these
tables.
These
are
stacks
of
answers,
and
it
kind
of
sort
of
I
should
recall
that
our
query
always
was
this,
so
it
kind
of
makes
sense
that
we're
getting
an
infinite
chain,
because
I
asked
you
to
tell
me
all
like
what
are
all
the
cloneable
types.
That's
what
this
query
is
saying,
go
ahead
and
give
me
all
the
cloneable
types
and
there's
an
infinite
set.
A
A
A
A
Okay,
I'll
keep
going
but
wondering
about
if
I
can
draw
a
picture
of
some
kind.
So
the
basically
what
happens
here
is
when
we
do
find
an
answer.
What
we
do
is
we
do
two
things.
We
split
the
strand
into
two
possibilities,
one
of
which
uses
the
answer
we
found
and
one
of
which
looks
for
a
next
answer.
A
A
So
what
we're
gonna
do
is
the
second,
when
we
ask
to
ensure
answer,
one
we're
gonna
pick
off
that
this
strand
as
I
said
we're
gonna
ask
for
its
interested
in
answer
zero,
and
now
there
is
an
answer
zero.
So
we
have.
We
have
a
result,
but
that
may
not
be
the
final
answer
like
there
could
be
more
answers
to
be
found
right.
There's
the
Veck
we've
we
found.
We
found
only
the
first
answer
from
this
sub
goal.
A
There
might
be
more
simple
answers
that
can
produce
so
we're
gonna
push
this
another
strand,
basically,
which
has
the
same
except
this
time
it
increments
the
counter-
and
it
says
we're
looking
for
sub
goal
number
one
this
time,
because
we
already
found
several
number
zero
and
then
we
can
go
on
with
our
own
life.
Alright.
So
our
current
strand,
the
current
strand
after
we
find
an
answer
we
get
to
discard
yet
so
goal.
A
So
we
wind
up
with
something
like
question
mark
day
goes
back
a
few
sighs
if
empty
list,
essentially,
which
is
an
answer,
and
so
that's
how
we
get
to
this
answer
was
because
once
we
leave,
we've
got
an
answer
for
this
of
gold.
Now
we
have
no
more
sub-goals
left,
we're
all
done,
but
we
still
have
a
strand
left
because
part
of
processing.
The
answer
was
to
push
the
new
strand
with
the
next
answer,
and
so
that's
how
we
wind
up
with
this
infinite
list
of
answers.
A
If
we
keep
asking
for
more
answers,
we'll
just
keep
getting
more,
but
what
would
ideally
happen.
This
particular
setup
will
happen.
Is
that
we'll
stop
from
the
outside
asking
for
more
answers,
because
we'll
see
that
we're
just
producing
an
infinite
to
many,
like
this
particular
query,
doesn't
give
us
any
unique
value
for
a
after
two
answers.
We
can
see
that,
and
so
we
can
stop
because
your
size
in
Bekaa
view
sizes
are
like
not
the
same
time.
A
A
Think
the
thing
that
I'm
trying
to
get
across
and
I'm
not
sure
if
it's
succeeding,
is
that
the
way
that
this
solver
works
at
the
highest
level
is
that
you
are
for
any
given
query.
It
is
producing
answers
that
are
getting
fed
into
other
queries,
and
so,
when
we
select
a
sub-goal,
we
basically
start
saying
that
for
each
answer
of
this
sub
goal,
I.
A
A
A
A
Right
so
then,
let
me
show
well
let
me
go
a
little
bit
to
the
problem
that
I'm
trying
to
solve
it.
The
non
innumerable
clauses
in
that
case,
so
one
of
the
problems
would
be
if
you
had
a
rule
like
this
well.
First
of
all,
first
problem
is
this
right:
if
you
have
I'm
just
gonna,
keep
it
in
the
abstract,
I'm
gonna
use
one
one:
sort
of
rusty,
treat
I.
A
Suppose
I
had
a
setup
like
this
right,
which
might
come
from
Mike
info
for
all
T
over
T.
Where
then,
there's
there's
two
traits
here,
there
are
2
sub-goals.
If
I
were
gonna
solve,
try
to
enumerate
the
type
say,
that's
their
work,
there's
2
sub-goals,
I
could
start
with
and
it
matters
a
lot
which
one
I
start
with
because
maybe
like
there's
exactly
one
answer
for
bar
of
a
and
it's
your
32.
So
if
I
start
with
that,
one
I'm
going
to
produce
an
answer
from
from
the
borrowed
VT
from
the
bar
of
a
table.
A
Of
question
Margay
instead
now
I
would
look
up
a
table
sized
question
mark
a
and
that's
kind
of
every
type
that
exists
right,
not
every
type
literally,
but
almost
every
Russ
type
is
sized.
So
that's
an
awful
lot
of
types
and
what
I
would
wind
up
doing
is
kind
of
searching
through
them
and
testing?
Is
this
type
bar?
Is
this
type
bar?
Is
this
type
bar
so
like?
Let's
say
it
might
yield
up?
You
know,
I
thirty
do
and
then
I
would
say.
A
Okay
now,
I
have
mu
of
I
32
at
bar
by
32,
and
so
I
can
look
up
a
table
for
bar
by
32.
That's
gonna
be
false.
Okay,
then,
in
my
yield
of
string
and
so
on,
right
and
eventually
it's
gonna,
give
me
you
32
and
I'm
gonna
and
I'm
gonna
find
that
answer.
So
it's
it's
gonna
inferior.
You
work
either
way
it
doesn't
really
matter
which
one
we
choose,
but
in
practice
it
actually
matters.
Of
course,
quite
a
lot
right
and
one
simple
way
to
solve.
This
is
don't
pick
size
right.
So
we
can.
A
This
is
what
I'm
saying
we
have
a
hook
that
the
key
that
a
that's
like
within
a
sub-goal
be
a
little
more
selective
about
which
thing
you
pick
first
right
now
we
always
pick
randomly
basically,
depending
on
the
order
in
which
they're
listed
just
like
Prolog
would
do
that's
not
so
smart.
It
might
be
better
to
pick.
A
You
know
we
could.
We
could
be
smarter
about
it,
but
that's
not
a
real
solution
because
we
might
be
sort
of
hidden
like
it
might
be.
Food
question
like
a
a
bar
off
question
or
day
and
that
as
a
question
my
day
and
borrow
question
mark
gave
sized
or
let's
say
that,
ask
and
borrowed
you
through.
So
the
bar
didn't
change
here,
but
food
did
and
the
only
thing
I
changed
about
foo
is
that
I
instead
of
saying
it
has
to
be
size?
A
It's
not
so
easy
for
me
to
to
know
which
one
I
should
order.
I
could
use
some
heuristics
perhaps
but
like
it
might
be
that
basically,
in
general,
it's
going
to
be
hard
for
us
to
do
that,
because
we
kind
of
get
locked
into
the
ordering.
We
have
to
process
the
way
that
the
current
system
is
set
up.
Basically
in
order
to
find
answers
for
best
I
have
to
process
all
of
its
sub
goals
before
any
of
those
answers
can
propagate
back
to
foo
and
then
be
fed
to
bar
right,
or
vice
versa.
A
They
potentially
apply
to
this
problem
too,
and
what
they
basically
let
you
do
is
to
say
when
you
get
back
an
answer,
it
includes
not
only
a
substitution
but
a
delay
literal
set
and
the
delayed
literal
is
basically
like
modulo
right.
So
you
can
kind
of
say
like
well
in
the
case
of
Baz
of
a
we
could
say.
A
So
this
pipe
the
stuff
before
the
pipe
is
the
delayed
literal
right,
and
what
this
is
basically
saying
is,
as
is
true
for
any
question
mark
a
if
question
mark
is
sized.
No,
that's
essential.
This
such
a
simple
example.
It's
been
pointless,
but
it's
kind
of
restating
the
rule
that
we
already
had.
But
the
point
is:
we've
kind
of
we
just
deferred
the
work
of
figuring
out
whether
a
was
sized
or
not,
and
we
said
no
here's
an
answer.
A
You
can
go,
take
this
answer
and
try
to
solve
bar
with
it
and
then
once
you're
done
with
that.
Maybe
you'll
come
back
and
solve
this
sized
problem.
So
that's
in
a
nutshell.
What
I
think
we
want
to
be
using
for
these
sorts
of
problems
is
allowing
us
to
say
when
we
get
to
the
point
where
we
would
have
to
enumerate
the
program
clauses
for
a
given
goal
and
thus
create
a
whole
bunch
of
strands.
We
might
instead
say
you
know
what
I
can't.
A
A
So
in
the
case
of
this
solver,
if
we
selected
bad
first
bad
luck,
but
it
doesn't
really
matter
because
it'll
just
produce
one
answer,
which
is
basically
a
no
up
it
gets
fed
bar
bar
will
solve
find
that
a
is
you
32
and
then
we'll
come
back
and
look
at
this
delayed
literal
and
say:
well
now
it's
not
sized
of
a
or
it's
still
size
debate,
but
a
is
your
32.
So
that's
actually
pretty
easy
for
us
to
solve.
That's
the
high
level
idea
and
this
these
delayed
things
can
propagate
through.
A
But
what's
a
little
bit
or
what's
worth
maybe
well,
the
question
is
raised
by
this.
This
way
is
when
do
you?
When
do
you
stop
the
lane?
If
you
have
a
little
ego,
how
long
do
you
delay
it
for
at
what
point
do
we
sort
of
underlay
it,
and
it's
maybe
worth
talking
a
little
bit
about
the
real
purpose
of
delayed
literals
or
the
original
purpose?
I
should
say
and
I
was
reading
into
this
before
this
talk,
because
I
was
trying
to
remember
what.
A
A
If
you
have
this
set
up,
this
is
called
a
negative
cycle.
There's
negative
reasoning
going
between
them,
and
that
is
that,
like
they
can't
both
be
true
clearly,
but
they
also
can't
both
be
false
because,
let's
say
if
P,
if,
if,
if
P
of
X
is
false,
well,
then
Q
of
X
must
be
true
right,
because
we
can
prove
that
it's
true,
because
not
P
of
X
is
true
and
vice
versa,
and
so
their
results
are
sort
of
linked.
A
But
it
depends
on
what
you,
what
answer
you
give
to
this
other
query,
Q
of
X,
that's
independent.
So
the
answer
that
that
we
end
up
with
is
actually
ambiguous,
and
this
is
where
there's
this
thing
called
the
well-founded
semantics
or
wfs,
which
basically
says
it's
kind
of
a
definition,
for
what
is
truth
mean
and
it
comes
up
with
three
results
for
any
given
predicate,
true/false
or
ambiguous,
and
the
idea
is
something
is
true.
B
A
There's
a
different
way
of
two
different
semantics
for
what
true
and
false
means,
and
it
would
actually
give
you
two
answers-
your
it
kind
of
the
reason
it's
called
answer
set.
Is
he
doesn't
give
you
an
answer
to
is
P
true
or
not?
It
gives
you
a
set
of
answers,
and
thus
it
can
help
handle
things
like
true,
false
and
false.
A
True,
because
there's
gonna
have
those
have
those
are
linked,
and
you
can
give
you
all
the
answers
at
once,
whereas
the
well-founded
semantics
is
through
more
narrow,
but
anyway
we
want
this
one,
but
it
turns
out
that
in
order
to
actually
compute
the
answers
to
this,
you
kind
of
have
to
have
the
same
concept
of
delaying,
because
what
wins
happening.
The
way
that
you
solve.
A
A
A
Fully
compute
all
the
other
possible
strands
for
Q
and
P,
and
if,
if
at
the
end
of
this
all
we're
left
with,
is
this
one
sort
of
delayed
literal
like
this?
We
can
you
can
either
I
say
if,
at
the
end
of
all
the
strands
right,
if,
if,
if
all
we're
left
with
at
the
end,
we
have
these
strands
and
they're
all
cycles.
It's
all
the
things
that
are
left
then.
A
If
there's
no
negative
with
them,
basically
they're
all
just
false,
there
are
no
answers,
and
if
there
is
then
it's
ambiguous.
Let
me
try
to
give
you
an
example:
I
realize
that's
kind
of
confusing,
but
because
I'm
confused
that's
why?
But
basically
what
we
do
is
or
negative
cycles
require
us
to
reorder.
A
Evaluation
and
delay
so
yeah
I,
don't
have
exactly
I,
don't
know
how
I
have
to
have
to
look
up
and
have
a
crisp
example
for
exactly
why
this
is.
But
it's
basically
similar
to
this
scenario.
I
was
trying
to
paint
here
where
you
kind
of
can't
locally
figure
out
when
you
have
negative
cycles.
What
the
answer
is,
so
what
you
want
to
do
is
delay.
A
C
A
A
A
But
what
happens
is
when
you
get
a
negative
cycle,
then
you,
you,
don't
consider
that
to
be
a
cycle.
Instead,
you
consider
you
delay
the
literal.
Instead,
you
you,
you
move
the
the
negative
edge
into
the
delay,
set
and
call
it
a
regular
answer,
and
the
reason
for
that
is
what
I'm
not
I.
Don't
have
crispy
on
tape
my
tongue,
but
it
comes
down
to
this
that,
basically
you
wouldn't.
It
would
be
wrong
I
guess
it
would
be
like
P
of
X,
if
not
let's,
maybe
we
can
even
make
an
example
of
it.
A
So
that's
not
a
very
useful
rule,
but
what
happened
is
that
you
would,
when
you
encounter
this
negative
cycle,
if
memory
serves,
you
would
basically,
instead
of
calling
out
a
cycle
of
the
normal
kind,
you
would
delay
the
P
of
X
literal
and
call
it
an
answer.
So
it
would
be
like
P
of
X
is
true
as
long
as
P
of
X
is
false,
and
then
you
would
go
produce
a
second
answer
here
and
I'm
trying
to
remember
why
yeah
I,
don't
exactly
have
it
on
tip
my
tongue?
C
A
Let's
take
a
look
at
the
actual
code,
so
it's
worth
asking:
why
does
rust
even
care
about
this
negative?
Actually,
they
don't.
As
it
happens,
we
don't
have
negative
reasoning
in
rust
and
all
these
complexities
are
a
good
reason
not
to
add
negative
reasoning
to
rest,
but
we
do
use.
It
is
in
exactly
one
place,
which
is
coherence
where,
if
you
look
at
what
the
coherence
rules
are
really
saying,
they're
basically
saying
you're
allowed
to
add
an
imple,
be
a
downstream
input
or
something
like
this.
A
If
there
is
no
upstream
mental
that
can
fix
it,
things
like
that,
and
so
we
use
it
in
a
kind
of
limited
way
and,
interestingly,
the
way
we
use
it,
it
could
never
form
a
negative
cycle
because
it's
basically
only
at
a
top
level
rule
and
that
rule
never
recursive
and
ask
for
other
rules.
They
could
have
negative
in.
A
So
maybe
none
of
this
matters
and
it's
possible
that
I
I've
been
tempted
to
just
rip
out
all
this
logic
or
at
least
I
think
it
would
make
sense
to
sort
of
special
case
this
delaying
logic
to
the
problem
we
actually
have,
which
is
the
size
problem
and
not
to
this
negative.
But
then
I,
thought
I,
don't
know,
it'd
be
nice.
A
The
strands
are
kept
in
canonical
form
when
they're
not
active,
that's
because
in
Russy
you
can't
have
an
inference
context
that
lives
longer
than
a
stack
frame
and
the
inactive
like
the
table
and
all
their
work
is
once
we
produce
an
answer,
all
the
stack
frames
that
are
processing
a
strand
have
to
pop
off.
So
all
the
strands
that
are
not
active
have
to
go
always
in
canonical
form,
so
they
don't
have
any
entrance
pieces
and
they
kind
of
get
rehydrated
afterwards.
A
A
It
could
be
that
we
we
asked
for
answer
number
one
or
whatever
answer
number
I,
and
there
were
no
more
strands
to
pursue.
In
that
case,
we
know
that
there
will
never
be
an
answer
number
I
and
we
can
give
back
no
more
solutions,
in
which
case
this
just
fails.
This
strand
it's
up
like
this
strand
eyes,
because
that
sub
goal
is
not
solvable
or
has
no
more
solutions
and
the
quantum
thing
I
forget
exactly
what
something
else
I
wanted
to
look
at,
but
I
think
there
are.
Basically
there
are
times
when
we.
A
A
There
are
various
points
here
where
we
sort
of
pop
back
and
that's
what
it
is
so
like
when
you
when
we
process
one
of
these
answers
like
here,
we
said:
okay,
we'll
go
down
strand
one
and
we'll
we'll
put
it
on
the
shelf.
Now,
because
we
got
a
cycle
and
we'll
come
back
and
process
strand,
two
and
stuff
like
that
and
I
forget
exactly
where.
But
there
are
some
places
where
we
kind
of.
A
We
return
a
quote:
I
call
quantum
exceeded
where
we
don't
want
to
just
keep
searching
forever.
So
if
we
spent
enough
time
looking
in
this
strand,
we
return
back
a
sort
of
ambiguous
result,
saying
come
back
again
later
and
we'll
keep
going.
But
this
way
we
can
because
we
want
to
ensure
that
research
does
back
space
more
thoroughly,
so
there
are
places
where
we
could
have
kept
going
if
we
wanted
to,
but
because
we
don't
want
to
be
depth-first
search,
we
don't
that's
what
quantum
acceded
is
about,
and
in
that
case
all
it
does.
A
Is
it
it
just
pushes
the
strand
back
on
the
table
for
later
and
returns.
So
you
can
see
that
the
strand
is
like
a
like
a
owned
value
of
it
gets
rehydrate
of
the
table,
lives
on
the
stack
for
a
while
and
then
either
gets
put
back
into
the
table,
or
if
it's,
if
it
doesn't
get
put
back
in
the
table
like
case
where
we
just
returned
in
error,
that
means
it's
dead.
A
A
Similarly,
if
there
are
no
more
answers,
that's
good.
We
succeeded,
but
if
we
get
cycles
and
so
on
then
yeah,
okay,
I
guess
we
wind
up
doing
the
same
thing.
But
if
we
go
up
with
this,
this
minimums
the
point
of
this
minimums
code
here,
because
it's
tracking
how
far
up
the
stack
was
this
cycle,
and
you
see
that
there's
like
a
positive
and
a
negative
saying
like
we
had
a
thing
on
the
stack.
A
A
I
think
I'm
gonna
stop
you're,
actually
I'm
looking
at
the
time
and
realizing.
This
is
like
well
over
an
hour,
but
we
should
talk
about
the
Coe
induction,
but
the
TLDR
is
that
we
don't
do
it
right,
but
it's
the
same
kind
of
thing
where
what
we
wind
up
doing
is
we
inappropriately
when
we
basically
Coe
induction,
mean
cycles,
are
okay,
it's
the
short
version
and
we
decide
that
it
cycles.
Okay.
So
we
treat
it
like
a
successful
answer,
but
actually.
A
Let
me
start
with
this
example:
if
foo
is
Co
inductive,
then
this
means
screw
of
X
holds
for
any
X.
So,
unlike
the
inductive
case
where
this
would
hold
for
nothing
because
there's
no
finite
tree,
it's
actually
fine
in
this
conductive
logic
rules,
if
not
very
interesting,
but
if
you're
added
in
this
bar,
because
there's
no
rules
for
bar
this,
this
is
basically
still
false
right.
A
We
can't
prove
foo
for
any
X,
because
we
can't
prove
bar
for
any
X
and
we
have
to
prove
both
foo
and
bar,
but
our
logic
will
say
that
it's
might
can
give
the
wrong
answer.
Maybe
Don
this
simple
of
an
example,
but
with
a
few
more
levels,
because
we
would
sort
of
incorrectly
decide.
Oh,
this
recursive
thing
is
true:
there's
a
this
is
a
correct.
This
is
true
because
it's
already
on
the
stack.
A
So
it's
a
cycle,
so
it's
true,
but
we
don't
realize
that
we
will
later
disprove
it
through
bar
and
that
can
lead
us
to
false
things
and
I
think
the
answer
would
be
when
we
see
these
cycles.
Instead
of
just
saying
it's
true,
we
should
delay
and
say
true
of
X
is
true
or
true
of
X
is
true
and
propagate
that
back
as
far
as
we
have
to
so
late
literals,
where
it's
at
I
guess
it's
the
short
version
of
this.