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.

diff --git a/docs/sphinx/tutorial/errors.rst b/docs/sphinx/tutorial/errors.rst
index d3c01f81cb430735a60f47832302e404e7f9e54c..53c647ae455f644e3d5558b7b7037d1afced48aa 100644 (file)
--- 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 (file)
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 (file)
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 b73b74c1bd1380272b48ff8534289ddcd4244b73..e87ba34464e3b8780cd42ac4a8bb3ad802c52f03 100644 (file)
--- 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 762c421a22c2af61ce3afce4cca1f78cb04c8b71..0581db06fb42b38ecb4cbe8c963007693f03e229 100644 (file)
--- 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                                                     {{{