From: Jason Eisner Date: Fri, 15 Nov 2013 21:58:46 +0000 (-0500) Subject: merged in Jason's changes, mostly a lot of "todo" items added to spec/index.rst in... X-Git-Url: https://hydra-www.ietfng.org/gitweb/?a=commitdiff_plain;h=fc55d13d2c981823db6c65858175670975f29a32;p=dyna2 merged in Jason's changes, mostly a lot of "todo" items added to spec/index.rst in late August 2013 --- diff --git a/docs/TODO.LSA b/docs/TODO.LSA index e96bbfb..7e9e746 100644 --- a/docs/TODO.LSA +++ b/docs/TODO.LSA @@ -28,6 +28,11 @@ impacts speed of compilation) ----- Backend +",/2" runtime error if first argument is not true or false + Probably OK for this one to crash the program! + +Check that we have = aggregation working correctly. + Could we maybe get a better chart representation? And better queries into the chart? We should be able to extract adorned queries from the planner's output without too much effort... @@ -38,6 +43,10 @@ Maybe something better for initializers or update API? (Low priority) ----- Documentation +Be sure to mention, repeatedly, that this is experimental software and is +likely to break both early and often. Explain the difference between panic +messages and errors. + ----- REPL ----- Whole pipeline @@ -68,6 +77,3 @@ DOpAMine improvements for logging of hyper-edges Graphical view of the hypergraph Tim has something pretty neat working - -",/2" runtime error if first argument is not true or false - Probably OK for this one to crash the program! diff --git a/docs/sphinx/bib.rst b/docs/sphinx/bib.rst index a417290..8fbb828 100644 --- a/docs/sphinx/bib.rst +++ b/docs/sphinx/bib.rst @@ -1,8 +1,15 @@ +.. -*- compile-command: "make html" -*- .. Bibliography Bibliography ############ +The publications below are referred to from this documentation site. +In addition, the old website has a list of `publications about Dyna +`_ as well as +some `publications that use Dyna +`_. + .. [filardo-eisner-2012] Nathaniel W. Filardo and Jason Eisner. :t:`A flexible solver for finite arithmetic circuits`. ICLP LIPIcs, 2012. diff --git a/docs/sphinx/index.rst b/docs/sphinx/index.rst index 155baf9..2e71500 100644 --- a/docs/sphinx/index.rst +++ b/docs/sphinx/index.rst @@ -6,6 +6,10 @@ nowadays there is explicit support for themes (I like "agogo" or "sphinxdoc"), as explained in the sphinx manual. +.. todo:: how to obtain / install Dyna. Also, licensing (see + http://bugs.dyna.org/rt/Ticket/Display.html?id=52, also + http://bugs.dyna.org/rt/Ticket/Display.html?id=569). + Welcome to Dyna! ================================= @@ -44,6 +48,7 @@ Contents: Indices and tables ================== +* :doc:`spec/errors` * :doc:`spec/glossary` * :ref:`genindex` * :ref:`search` diff --git a/docs/sphinx/spec/index.rst b/docs/sphinx/spec/index.rst index 16c09e6..9ed95a3 100644 --- a/docs/sphinx/spec/index.rst +++ b/docs/sphinx/spec/index.rst @@ -1,14 +1,66 @@ + .. -*- compile-command: "make -C .. html" -*- .. Specification index This file is enumerated in the toctree directive of index.rst +.. todo:: set up the default role to be code, so that `foo` and + ``foo`` are identical. + .. todo:: Fill in to-do items from various sources, then break this into - multiple files. (I believe that in the HTML rendering, each file is a webpage.) - -################################## -Specification of the Dyna Language -################################## + multiple files. (I believe that in the HTML rendering, each file + is a webpage.) + + Sources: + + https://mail.google.com/mail/?shva=1#apps/label%3Adyna+OR+label%3Adynasty+OR+label%3Adyna%2Fbugs+OR+label%3Adyna%2Fbuild+OR+label%3Adyna%2Fdistro+OR+label%3Adyna%2Fdynac+OR+label%3Adyna%2Fdynamite+OR+label%3Adyna%2Finference+OR+label%3Adyna%2Fserver+OR+label%3Adyna%2Fstorage+OR+label%3Adyna%2Fsyntax+OR+label%3Adyna%2Ftransforms + DONE - http://dyna.org + http://dyna.org/Design and perhaps also http://dyna.org/wiki/index.php?title=Special:LongPages + http://bugs.dyna.org + DONE - Bugs + DONE - Comments + DONE - Distro + DONE - Documentation + DONE - Dynac + DONE - Dynamite + Dynasty + haskell-interpreter + Help + Inference + Misc + Reading + Server + Storage + Syntax + Transforms + + http://cs.jhu.edu/~jason/papers/#Dyna + http://cs.jhu.edu/~darcey/dyna-tutorial.pdf + ~/grants/*dyna* + ~/jot/dyna + ~/jot/dynasty + ~/jot/dopp + ~/hw/dyna/docs/inference2.txt + ~/hw/dyna/docs/manpage.txt + ~/hw/dyna/docs/manpage-NOTES.txt + ~/jot/dopp + ~/hw/dyna/CITE + ~/hw/dyna/docs/frozen3.txt + ~/hw/dyna/docs/frozen2.txt + ~/hw/dyna/docs/frozen.txt + ~/hw/dyna/docs/frozen-SCRAPS.txt + ~/hw/dyna/docs/nwf-inference-notes.txt + ~/jot/dynabases + ~/hw/dyna/docs/pseudospec.tex + ~/jot/dynaspec + ~/Mail/dyna + ~/hw/dyna/TO-DO-2005 + ~/hw/dyna/SEND-TO + + +###################################### + Specification of the Dyna Language +###################################### ************ Introduction @@ -19,9 +71,13 @@ What is Dyna? .. todo:: keep it brief +.. todo:: Some materials at http://www.dyna.org/ and http://www.dyna.org/wiki/index.php?title=Documentation#Overview. + Intended users ============== +.. todo:: include teaching: http://www.dyna.org/wiki/index.php?title=Teaching + Key features ============ @@ -30,9 +86,9 @@ Relation to other work .. todo:: where to learn more -******************************** - How to read this specification -******************************** +****************************** +How to read this specification +****************************** Organization ============ @@ -56,7 +112,7 @@ Sidebars Notifications ============= -.. todo: deprecation, bugs, future work +.. todo:: deprecation, bugs, future work Links to examples ================= @@ -71,12 +127,16 @@ Glossary/Index Terms (i.e., ground terms) *************************** +.. todo:: old design at http://www.dyna.org/wiki/index.php?title=Term + Overview ======== Primitive terms =============== +.. todo:: Old design at http://www.dyna.org/wiki/index.php?title=Primitive_%28future_version%29 + Booleans -------- @@ -101,6 +161,11 @@ Compound terms Functors -------- +.. todo:: old design at http://www.dyna.org/wiki/index.php?title=Atom +.. todo:: What space are these in? How do they relate to strings and + dynabases? See https://github.com/nwf/dyna/issues/49, and + consider RDF names. + Single quotes ^^^^^^^^^^^^^ .. todo:: Escape codes as for strings except we need \' @@ -115,10 +180,15 @@ Operator syntax Keyword arguments ----------------- +.. todo:: see Python defaults, keywords, varargs at http://docs.python.org/3/tutorial/controlflow.html#more-on-defining-functions List syntax ----------- +.. todo:: old documentation at http://www.dyna.org/wiki/index.php?title=Syntactic_sugar_for_terms +.. todo:: extracting functors and args; whether extracting a functor + from a dynabase or frozen term is null or an error + Reserved functors ----------------- @@ -128,27 +198,49 @@ Reserved functors ``$error`` ^^^^^^^^^^ +.. todo:: how to test for errors (catch errors) - maybe a forward + reference. Trying to unify two errors -- including during + query or update propagation -- probably needs to give an + error, or errors might silently vanish when they pass + through equality, leading to unexpected results! +.. todo:: dealing with errors as arguments, e.g., f(X/Y) = ... + may yield f($error(...)). Presumably this means that + f(X) yields some f($error(...)) matches: are their + values also errors? + + ``$null`` ^^^^^^^^^ +Sets +==== + +.. todo:: See sets and rsets in frozen3.txt + Dynabases ========= -Full discussion in :ref:`frozen`. +Full discussion in :ref:`dynabase`. + +Gensyms +------- Frozen terms ============ -Full discussion in :ref:`dynabase`. - +Full discussion in :ref:`frozen`. ********************************* Patterns (i.e., non-ground terms) ********************************* +.. todo:: old documentation is at http://www.dyna.org/wiki/index.php?title=Pattern + Variables ========= +.. todo:: Old documentation at http://www.dyna.org/wiki/index.php?title=Variable + Variable names -------------- @@ -164,12 +256,16 @@ Types Type declarations ----------------- +.. todo:: old design at http://www.dyna.org/wiki/index.php?title=Term#Union_types + Typed variables --------------- Co-inductive types ------------------ +.. todo:: how do we deal with types for varargs and keyword args? + Possible future extensions -------------------------- Guarded types? Nonlinear types? Parametric types? @@ -185,6 +281,8 @@ Unification Frozen terms ============ + +.. todo:: see frozen3.txt. .. _dynabase: @@ -195,10 +293,11 @@ Dynabases Overview ======== - Items ===== +.. todo:: old documentation at http://www.dyna.org/wiki/index.php?title=Item + Null items ---------- @@ -216,23 +315,57 @@ Quoting items with ``&`` Evaluating terms with ``*`` --------------------------- +Assertions +========== + Queries ======= Simple queries -------------- +.. todo:: what does a query for simply ``X`` get? How about ``d.X`` + or ``d->X`` where X is a dynabase? Does it range over + primitives? Expressions? + + Complex queries --------------- -.. todo:: joins with commas +.. todo:: joins with commas, and "for" clauses + +.. todo:: when is f(X),g(X) considered to be incompatible with the + types of f and g? Expressions ----------- -.. todo:: (auto-evaluation) ("nested queries") +.. todo:: Call these "nested queries"? Auto-evaluation. + Old discussion at + http://www.dyna.org/wiki/index.php?title=Expression and at + http://www.dyna.org/wiki/index.php?title=Syntactic_sugar_for_inference_rules . + +.. todo:: when is f(g(X)) considered to be incompatible with the type + of f and the evaluation type of g? + +.. todo:: do primitives evaluate to themselves, etc. + +.. todo:: can you quote the * operator? (What is the order of + desugaring?) + +.. todo:: using prefix ^ to evaluate variables in the parent lexical scope. + See frozen3.txt. Aggregating queries ------------------- +.. todo:: i.e., prefix aggregators. original discussion at http://www.dyna.org/wiki/index.php?title=Syntactic_sugar_for_inference_rules +.. todo:: use ^ to lift a variable out of the lexical scope of the + aggregator even if it's not mentioned outside. For example, + ``query (+= foo(I,^J))`` will return a separate answer for + each J, e.g. + (+= foo(I,2)) = 5. + (+= foo(I,3)) = 7. + And ``query (*= (+= foo(I,^J)))`` will return 35 in this case. + Accessors --------- .. todo:: Dot and arrow expressions to access elements of a dynabase @@ -247,6 +380,23 @@ Some discussion of current approach is in :doc:`/manual/pragmas`. Output format: Finite, sorted, consolidated, ground, etc. Det/semidet/etc. Overall, or per-variable? What if it binds a sequence of variables? +.. todo:: error results + +.. todo:: user might want to specify modes that are promised (speeds + up planner, like type declaration) and modes that are + withheld (says that planner shouldn't use these modes since + they're expensive or bloat the code or since we don't + promise that they'll be possible in a future version of the + program). Can combine these by specifying modes + exhaustively. + +.. todo:: When a dynabase is extended, it might support fewer modes + because the new rules can't be planned. This means that the + extended dynabase has a more restricted type than the + original (i.e., a supertype) and can't be assigned to any + variable that requires the original type to successfully + do mode planning. + Lambdas ======= @@ -279,9 +429,9 @@ Const declaration Snapshots ========= -************************************ - Inspecting and modifying dynabases -************************************ +********************************** +Inspecting and modifying dynabases +********************************** Abstract API ============ @@ -295,17 +445,23 @@ Command line interface Graphical interface =================== +.. todo:: old Dynasty description and links at + http://www.dyna.org/wiki/index.php?title=Dynasty . + Over 216 tickets on the Dynasty queue at + http://bugs.dyna.org, with lots of design discussion. + Programming interface ===================== -*************** - Dyna programs -*************** - +************* +Dyna programs +************* -Programs +Overview ======== +.. todo:: Old description at http://www.dyna.org/wiki/index.php?title=Program + File format =========== .. todo:: UTF-8, BOM @@ -314,23 +470,65 @@ File format Rules ===== +.. todo:: Old documentation at http://www.dyna.org/wiki/index.php?title=Inference_rule + Definition ---------- Aggregation ----------- -Semantics ---------- +Guards +------ -Cycles -^^^^^^ +.. todo:: refer back to guards + +Fixpoint semantics +------------------ + +.. todo:: perhaps also discuss execution policies Errors ^^^^^^ +.. todo:: See discussion of current error policy in :doc:`/tutorial/errors`. + +Cycles +^^^^^^ + +Stability +^^^^^^^^^ + +to nwf: + I think I really want the semantics of dynabase extension + to be the same as the semantics of updates. This means that + when you extend a dynabase, you don't disturb randomness or + cycles that are not transequents of your extension. Whether + dynabases become new in an update is not answerable from + within Dyna, I think, because the old dynabase can no longer + be accessed; but it should be answerable from outside, e.g., + d.e may be different before and after we update d.e.x += 1. + This may be up to the implementation. (Certainly snapshots + of those two are different.) But maybe two snapshots both + before the update should be the same. + + (All queries are against snapshots, so how do we actually get a + live version of e? Maybe we can't. Or maybe queries are not + totally against snapshots after all -- the snapshot is taken only + to get the path to e but the thing that that path points to is live + by default, so the recursive snapshotting doesn't go all the way + down. Anyway, if we do get two snapshots of e before and after, + then they must be different in the sense that they get different + results when we query them.) + + See discussion of current implementation in :doc:`/tutorial/errors`. +Gensyms +------- + +.. todo: how gensyms capture variables + Head destructuring ------------------ @@ -340,6 +538,9 @@ Dynabase literals Syntax ------ +.. todo:: using ^ to construct and evaluate terms in the parent + lexical scope + Ownership --------- @@ -351,6 +552,7 @@ Declarations Some documentation of currently implemented declarations is in :doc:`/manual/pragmas`. +.. todo:: old design: see http://www.dyna.org/wiki/index.php?title=List_of_declarations Type declarations ----------------- @@ -387,6 +589,37 @@ Syntax declarations Declaring new aggregators ------------------------- +Declaration inference +===================== + +.. todo:: and compile-time errors. See + http://www.dyna.org/wiki/index.php?title=Declaration_inference + +Type inference +-------------- + +.. todo:: if the user defines f(0) and f(1), should we guess + that f only takes integers, so that it's a type error + to query f("hello") from the repl or as a subgoal, or + to update the dynabase with such an aggregand? + What if the user defines f(&g(3))? + Are we to generalize from examples to the minimal + basic or natural types that cover those examples? + +.. todo:: can we infer parametric types? + +Aggregator inference +-------------------- + +.. todo:: similar to above, if the user says that += is the + aggregator for f(0), do we conclude that it is + the aggregator for f? for all f(int)? if f(0) and + f(1) have different aggregators, is that an error/warning + unless otherwise declared? In general it may be ok to + have a separate consistent aggregator for each item, + but if the repl can create new aggregators for things + that feed into a rule, we might have to recompile the + way we handle updates for those things ... Scripting commands ================== @@ -409,12 +642,31 @@ Overview Standard syntactic sugar ======================== +.. todo:: semicolons + +.. todo:: prefix aggregators and ^ + +.. todo:: type restrictors on variables and on evaluated and quoted subexpressions + +.. todo:: some ideas at + http://www.dyna.org/wiki/index.php?title=List_of_keywords + +.. todo:: "in" (overloaded for lists, ranges, sets, frozen terms, + possibly maps or general dynabases) + Default syntax table ==================== Changing the syntax table ========================= +.. todo:: old documentation of declaring new operators (similar to + Prolog) is at + http://www.dyna.org/wiki/index.php?title=Syntactic_sugar_for_terms. + A possible new design is in :doc:`/manual/pragmas`. + +.. todo:: nwf started working with Jay's parser: http://bugs.dyna.org/rt/Ticket/Display.html?id=588 + Printing ======== @@ -424,9 +676,9 @@ Readable printing Prettyprinting -------------- -****************** - Standard library -****************** +**************** +Standard library +**************** There is currently some documentation in :doc:`/manual/builtins`. @@ -438,9 +690,22 @@ Generic operators and aggregators Boolean operators and aggregators ================================= +.. todo:: note tricks like forcing null to false by using ``|| + false``. Or in the 2-valued case where false is not + possible, ``?`` can be used. + Numeric operators and aggregators ================================= +.. todo:: include discussion of with_key and with_val. In general + we may want some kind of multiple-value-return stuff (related to + coercion), which would also be useful for the Lisp examples + and for doing a version of member that allows duplicates by + binding additional hidden variables that refer to the entry + (that is rather like with_key). + +.. todo:: also k-best derivations: http://bugs.dyna.org/rt/Ticket/Display.html?id=257 + Randomness ========== @@ -460,22 +725,31 @@ Other standard encodings ======================== .. todo:: see ~/jot/dyna 12/14/12 et seq. -****************************** - Inspecting program execution -****************************** +*************************** +Analyzing program execution +*************************** $rule ===== +$gradient +========= + +.. todo:: Rationale at + http://www.dyna.org/wiki/index.php?title=Training_weights +.. todo:: Old design at http://www.dyna.org/wiki/index.php?title=DynaMITE + Voodoo items ============ -Reflection on types, modes, cost estimates, cardinality estimates, plans, etc. -============================================================================== +Reflection +========== + +.. todo:: reflection on types, modes, cost estimates, cardinality estimates, plans, etc. -******************************* - Controlling program execution -******************************* +***************************** +Controlling program execution +***************************** Storage classes =============== @@ -511,6 +785,7 @@ Appendices .. toctree:: + errors glossary diff --git a/docs/sphinx/tutorial/index.rst b/docs/sphinx/tutorial/index.rst index 8e9426e..57f16e6 100644 --- a/docs/sphinx/tutorial/index.rst +++ b/docs/sphinx/tutorial/index.rst @@ -13,3 +13,5 @@ Tutorial dijkstra errors darcey + +.. todo:: from old tutorial: http://www.dyna.org/wiki/index.php?title=Grandfather_example