I don't understand why "Evaluation failed to fixpoint"

84 views
Skip to first unread message

Ionuț G. Stan

unread,
Apr 27, 2017, 10:07:18 AM4/27/17
to Eve talk
Hi again,

I can't seem to understand why I get an error for these blocks:
http://play.witheve.com/#gist:7fb7ed6d791c0d8c8ecfaefb7d2bcab1-fixpoint.eve

I've read about Eve's execution model and the difference between `bind`
and `commit`, but I still can't understand why the above doesn't work
with `bind`, but does with `commit`.

Can anyone shed some light? Thanks!

--
Ionuț G. Stan | http://igstan.ro | http://bucharestfp.ro

Chris Granger

unread,
Apr 27, 2017, 1:55:11 PM4/27/17
to Ionuț G. Stan, Eve talk
Hi Ionuț,

That code fails to "fixpoint" because binds always stay up to date with their inputs. On the first run of the second block, the person doesn't have an age, so it adds the age 21 to them. It then runs the block again because an age has been added and the block has the constraint that we only add the age 21 to people without an age. Now that there is one, it needs to remove the value it added. It then does that in a loop forever. To fix the block you could change your not to:

age = if r.age then r.age
          else 21

By doing this you're saying the age is whatever it happens to be set to at the time or 21 otherwise, this causes the block to reach a stable state (aka fixpoint) of 21.

Cheers,
Chris.

--
You received this message because you are subscribed to the Google Groups "Eve talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to eve-talk+u...@googlegroups.com.
To post to this group, send email to eve-...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/eve-talk/a0f14d02-341a-d825-3a13-41992dae844f%40gmail.com.
For more options, visit https://groups.google.com/d/optout.

Ionuț G. Stan

unread,
Apr 28, 2017, 9:12:15 AM4/28/17
to Chris Granger, Eve talk
Hi Chris,

I'm not sure I get it, but I'll try to put down what I think I understand.

Before reading your response, I was viewing `search` blocks as
predicates only. Now, after reading your response, it seems that
`search` is trying to unify the incoming records with the pattern it
describes. So it's more than just a predicate that guards the following
`bind` blocks. Is that true?

The thing is, I don't understand why execution would enter the second
block a second time. It's true that the inputs it is bound too have
changed, but they don't satisfy the age-not-present condition anymore.
At least that's how I saw things when I wrote the code.
> <mailto:eve-talk%2Bunsu...@googlegroups.com>.
> To post to this group, send email to eve-...@googlegroups.com
> <mailto:eve-...@googlegroups.com>.

Josh Cole

unread,
May 1, 2017, 6:27:16 PM5/1/17
to Eve talk, ibd...@gmail.com
Hey Ionuț,

Let's start with a smaller example so that we can discuss how bind works.

Take the following block, which marks anyone under the age of 18 as underage (in the U.S.) for voting.


search
  person
= [#person]
  person
.age < 18


bind
  person
+= #underage



Once you've created the block and added it to the program, it will begin running. When it starts we'll parade the existing facts in the system past it as potential input. If anything matches, it will get processed. From then on, every new fact added to the system (including those from this and other blocks!) will also be considered as input.

Let's create some people to test that out.



commit
 
[#person name: "Jeff" age: 14 birthday: "09-07"]
 
[#person name: "Jorge" age: 23 birthday: "01-13"]
 
[#person name: "Jen" age: 17 birthday: "05-01"]

 
// we'll use this later on...
 
[#celebrate-birthday date: "05-01"]



As we would expect, both Jeff and Jen will be tagged #underage. Now, what happens if Jen's birthday passes? Let's celebrate!


search
  celebrate = [#celebrate date]
  person = [#person birthday: date]

commit
   celebrate := none // We wouldn't want to celebrate twice!
   person.age := person.age + 1


So, Jen is 18 now. This new fact enters the system and gives every block a chance to run again. We really want the block to stop saying that Jen is underage since she no longer meets its requirements. Luckily for us, that's exactly how bind works in Eve. Since her age doesn't pass the `< 18` test, the block stops asserting that she's `#underage` and everything is right with world.

That same logic carries over to your case. Let's look at the following setup.

Here's a person with no age:


commit
  [#person name: "Jeff"]


And a block to attach a default age to people:


search
  person 
= [#person]
 
not(person.age)


bind
  person
.age := 21


First, we introduce Jeff to the block. Since he matches, (he is a person and he's got no age) we assign an age to him. This new fact enters the system about Jeff, so we need to check to make sure he still matches. Unfortunately, now that Jeff has an age (even though it's one we provided!) he no longer matches our terms. Therefore, we stop asserting that Jeff has an age. Where this goes from bad to worse is that this change affects the block yet again. It considers whether Jeff (now ageless again) matches and indeed he does. We reassert the age and continue the cycle until Eve detects the divergence and stops executing.

There are several ways to fix this problem, depending on what you want to happen. For a case of defaults like this, you can either do as Chris suggests above with an if/else, or you can change the bind to a commit. Commits are permanent, unlike binds, so they won't get retracted even when the inputs that caused them to trigger cease existing. So long as that's really the behavior you're looking for, commit should be a one word fix for your existing block. :)

Please feel free to ask any other questions you have here on the mailing list as well. Chances are if there's something in the language you struggle with, other people are struggling too. Helping you helps us improve the language and documentation for everybody!

co...@kodowa.com

unread,
May 1, 2017, 6:45:01 PM5/1/17
to Eve talk
Adding to Josh's response, I like to think through these problems stepping through time. To be clear, I make no claims that this is how the runtime is actually working in terms of timesteps, it's just a way I've found helpful in debugging these kinds of issues.

Considering your block

search
  r
= [#person name]
 
not(r = [age])

bind
  r
.age := 21


Let's start at T0 with the record [#person name: "Jeff"]

This record matches the block, and so we bind an age to it.

T1: [#person name: "Jeff" age: 21]

But now this record no longer matches the block. Therefore, the block doesn't run anymore, and the bound age disappears:

T2: [#person name: "Jeff"]

Now we've reached the initial state, where the record does match the block, and the age is bound again. The loop repeats forever.

Using commit instead of bind fixes this; once you commit the age, it's on the record until it's removed explicitly. By contrast, the binding age means it's on the record as long as the record matches the search. Here's the step-by-step breakdown when you use commit:

T0 [#person name: "Jeff"] - the initial record
T1 [#person name: "Jeff" age: 21] - the record matches the block, so we commit an age
T2:[#person name: "Jeff" age: 21] - the record no longer matches the block, but we've committed the age so it remains. This prevents the block from running again, and the evaluation reaches a steady state.

I hope this perspective adds something to the explanation Josh gave.

Corey

Ionuț G. Stan

unread,
May 2, 2017, 7:31:29 AM5/2/17
to Josh Cole, Eve talk, ibd...@gmail.com
Thanks. Having read both explanations I think it finally clicked.

I guess what I was having trouble with is realizing that the data
recorded by a `bind` block lives *as long as* the `search` conditions
are met. Whenever the search conditions stop holding, the bind block
ceases to "evaluate". I'm using evaluate, although I understand it's not
a long running computation taking place there, just because I find it
easier to explain the record undoing effects, whatever those may be.
> <javascript:>
> > <mailto:ionut....@gmail.com <javascript:>>> wrote:
> >
> > Hi again,
> >
> > I can't seem to understand why I get an error for these blocks:
> >
> http://play.witheve.com/#gist:7fb7ed6d791c0d8c8ecfaefb7d2bcab1-fixpoint.eve
> <http://play.witheve.com/#gist:7fb7ed6d791c0d8c8ecfaefb7d2bcab1-fixpoint.eve>
>
> >
> > I've read about Eve's execution model and the difference
> between `bind`
> > and `commit`, but I still can't understand why the above
> doesn't work
> > with `bind`, but does with `commit`.
> >
> > Can anyone shed some light? Thanks!
> >
> > --
> > Ionuț G. Stan | http://igstan.ro | http://bucharestfp.ro
> >
> > --
> > You received this message because you are subscribed to the
> Google
> > Groups "Eve talk" group.
> > To unsubscribe from this group and stop receiving emails from it,
> > send an email to eve-talk+u...@googlegroups.com <javascript:>
> > <mailto:eve-talk%2Bunsu...@googlegroups.com <javascript:>>.
> > To post to this group, send email to eve-...@googlegroups.com
> <javascript:>
> > <mailto:eve-...@googlegroups.com <javascript:>>.
> <https://groups.google.com/d/msgid/eve-talk/a0f14d02-341a-d825-3a13-41992dae844f%40gmail.com>.
>
> > For more options, visit https://groups.google.com/d/optout
> <https://groups.google.com/d/optout>.
> >
>
>
> --
> Ionuț G. Stan | http://igstan.ro | http://bucharestfp.ro
>
> --
> You received this message because you are subscribed to the Google
> Groups "Eve talk" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to eve-talk+u...@googlegroups.com
> <mailto:eve-talk+u...@googlegroups.com>.
> To post to this group, send email to eve-...@googlegroups.com
> <mailto:eve-...@googlegroups.com>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/eve-talk/e597e12b-97a3-4862-a229-bc5bcf85efac%40googlegroups.com
> <https://groups.google.com/d/msgid/eve-talk/e597e12b-97a3-4862-a229-bc5bcf85efac%40googlegroups.com?utm_medium=email&utm_source=footer>.
Reply all
Reply to author
Forward
0 new messages