From 7724643928a8f5475c7a68cf2fe06a98f56ec47c Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Fri, 7 Jun 2013 12:28:20 -0400 Subject: [PATCH] fix error :: String Rework conjunction handling in normalizer -- it was erroneously discarding the left hand side, rather than unifying with true. While here, add both a test-case (examples/fib-limit.dyna) and some documentation for users. Closes github issue nwf/dyna#14. --- docs/sphinx/tutorial/errors.rst | 72 +++++++++++++++++++++++++++-- examples/expected/fib-limit.py.out | 19 ++++++++ examples/fib-limit.dyna | 8 ++++ src/Dyna/Analysis/ANF.hs | 24 ++++++---- src/Dyna/Backend/Python/Selftest.hs | 6 ++- 5 files changed, 116 insertions(+), 13 deletions(-) create mode 100644 examples/expected/fib-limit.py.out create mode 100644 examples/fib-limit.dyna diff --git a/docs/sphinx/tutorial/errors.rst b/docs/sphinx/tutorial/errors.rst index d3c01f8..53c647a 100644 --- a/docs/sphinx/tutorial/errors.rst +++ b/docs/sphinx/tutorial/errors.rst @@ -35,7 +35,9 @@ attempt to run it? Our interpreter produces a chart with an annotation:: ============ because b is 0: division by zero - + in rule test.dyna:4:1-test.dyna:4:12 + a += 1 / b. + This last ``Errors`` display indicates that the answers available in the ``Charts`` section is not reliable. @@ -45,15 +47,23 @@ This last ``Errors`` display indicates that the answers available in the interpreter produces an ``Errors`` section, then the entire chart must be considered suspect. +If we run the interactive interpreter and add the rule ``b += 1.``, the +error condition has cleared as it should. If we then add ``b += -1.``, it +will return. + Non-Termination =============== +Productive Nontermination +------------------------- + As mentioned before, Dyna2 currently uses *agenda-driven semi-naive forward chaining* for its reasoning. This algorithm has several excellent theoretical properties, but suffers from a potentially show-stopping problem: *it might not stop*. -A Dyna program which includes a definition of the Fibonacci numbers :: +A Dyna program which includes a definition of the Fibonacci numbers (*e.g.*, +``examples/fib.dyna``) :: fib(1) += 1. fib(2) += 1. @@ -63,8 +73,64 @@ will compile and be accepted by the interpreter, but will attempt to prove a ``fib`` item for every positive natural number! Clearly, this task is going to take a while. -If your program goes away for longer than you expect, it is entirely +If your program *does* go away for longer than you expect, it is entirely possible that it is caught in such an infinite loop. In that case, you may send it a ``SIGINT`` by hitting Control-C. The interpreter will then print out the chart as far as it had determined it. If this is far bigger than expected, your program probably has a productive infinite loop. + +Fixing The Fib Example +`````````````````````` + +One way out of this problem is to impose a limit on the program, by writing +instead something like:: + + f(X) += f(X-1) + f(X-2) for X < lim. + lim := 10. + +This will limit the system to proving the first ``lim`` Fibonacci numbers. +Of course, that can expand or contract as you define ``lim``. + +.. index:: + single: counting to infinity + +Counting To Infinity +-------------------- + +Unfortunately, another kind of nontermination error can arise in cyclic +programs, which is not so easy to fix: the so-called *count-to-infinity* +problem. + +If we were to have ``examples/dijkstra.dyna`` loaded in the interpreter and +then run :: + + :- start := "NoSuch". + +Where there is no such ``"NoSuch`` vertex, the interpreter will appear to be +pondering this change to the universe for "a while", as we say. If we +interrupt it (with Control-C) after a while, the chart will contain, among +other things:: + + path/1 + ================= + path("DFW") := 10124432 + path("LAX") := 10124063 + path("MyHouse") := 10122046 + path("NoSuch") := 0 + path("ORD") := 10123630 + path("SFO") := 2779 + +This arises from the fact that our graph contains a cycle:: + + edge("DFW","ORD") := 802. + edge("ORD","DFW") := 802. + edge("LAX","ORD") := 1749. + +Note that it is also possible to "count to infinity" in other directions, +such as by counting down to :math:`-\infty` or by approaching a finite +solution but as in Zeno's paradox. + +.. admonition:: bug + + There is, as of yet, no good solution to this problem; the best + work-around might just be to start the program over. diff --git a/examples/expected/fib-limit.py.out b/examples/expected/fib-limit.py.out new file mode 100644 index 0000000..2d35826 --- /dev/null +++ b/examples/expected/fib-limit.py.out @@ -0,0 +1,19 @@ + +Charts +============ +f/1 +================= +f(1) := 1 +f(2) := 1 +f(3) := 2 +f(4) := 3 +f(5) := 5 +f(6) := 8 +f(7) := 13 +f(8) := 21 +f(9) := 34 + +lim/0 +================= +lim := 10 + diff --git a/examples/fib-limit.dyna b/examples/fib-limit.dyna new file mode 100644 index 0000000..8dbb70e --- /dev/null +++ b/examples/fib-limit.dyna @@ -0,0 +1,8 @@ +f(1) += 1 . +f(2) += 1 . + +% Fix the productive divergence by imposing an arbitrary, but tunable +% limit. +f(X) += f(X-1) + f(X-2) for X < lim. + +lim := 10. diff --git a/src/Dyna/Analysis/ANF.hs b/src/Dyna/Analysis/ANF.hs index b73b74c..e87ba34 100644 --- a/src/Dyna/Analysis/ANF.hs +++ b/src/Dyna/Analysis/ANF.hs @@ -37,6 +37,9 @@ -- "Dyna.Backend.Python"'s @findHeadFA@ function. -- XXX This module does not use Control.Lens but should. +-- +-- XXX The handling of underscores is not quite right and frequently leads +-- to dead assignments. -- FIXME: "str" is the same a constant str. @@ -375,20 +378,23 @@ normConjunct :: (Functor m, MonadReader ANFDict m, MonadState ANFState m) normConjunct ss f i si r sr n d rev = case (n,d) of (0,Nothing) -> do - go Nothing Nothing + di <- nextVar "_b" + dr <- nextVar "_c" + go di dr newWarn "Quoted functor discarded" ss (0,Just d') -> do di <- nextVar "_b" dr <- nextVar "_c" - go (Just di) (Just dr) + go di dr doStruct (selfstruct di dr) d' - (1,Just d') -> go Nothing (Just d') + (1,Just d') -> do + di <- newLoad "_b" (Right $ (dynaUnitTerm,[])) + go di d' (_,_ ) -> do - di <- nextVar "_b" + di <- newLoad "_b" (Right $ (dynaUnitTerm,[])) dr <- nextVar "_c" - go (Just di) (Just dr) - t <- newLoad "_x" (Right $ selfstruct di dr) - ct <- timesM (newEval "_x" . Left) (n-1) t + go di dr + ct <- timesM (newEval "_x" . Left) (n-1) dr maybe (return ()) (doUnif ct) d @@ -396,8 +402,8 @@ normConjunct ss f i si r sr n d rev = selfstruct ni nr = (f,if rev then [nr,ni] else [ni,nr]) go di dr = do - normTerm_ ADEval (0,False) (si:ss) di i - normTerm_ ADEval (0,False) (sr:ss) dr r + normTerm_ ADEval (0,False) (si:ss) (Just di) i + normTerm_ ADEval (0,False) (sr:ss) (Just dr) r normTerm :: (Functor m, MonadState ANFState m, MonadReader ANFDict m) diff --git a/src/Dyna/Backend/Python/Selftest.hs b/src/Dyna/Backend/Python/Selftest.hs index 762c421..0581db0 100644 --- a/src/Dyna/Backend/Python/Selftest.hs +++ b/src/Dyna/Backend/Python/Selftest.hs @@ -70,7 +70,11 @@ mkExample name = goldens :: TF.Test goldens = TF.testGroup "Python Backend End-To-End" - $ map mkExample ["simple", "dijkstra", "papa2", "matrixops"] + -- Sorted roughly by likelihood that all subsequent examples + -- will be broken. ;) + $ map mkExample [ "simple", "fib-limit", "dijkstra" + , "papa2", "matrixops" + ] ------------------------------------------------------------------------}}} -- Harness toplevel {{{ -- 2.50.1