From 746b13c076f3d890ae9b460ee29e2f742f6f146e Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Thu, 9 Nov 2023 21:37:11 -0500 Subject: [PATCH] Add a readme and link to it --- README.md | 193 ++++++++++++++++++++++++++++++++++ index.html | 4 +- src/datalog/dusa-tokenizer.ts | 2 +- src/dusa.css | 15 ++- 4 files changed, 210 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 56cf22e..2664756 100644 --- a/README.md +++ b/README.md @@ -1 +1,194 @@ # Dusa Language + +[![Coverage Status](https://coveralls.io/repos/github/robsimmons/dusa/badge.svg?branch=main)](https://coveralls.io/github/robsimmons/dusa?branch=main) + +Dusa is a logic programming language that shares properties of Datalog (as implemented in systems like +[Soufflé](https://souffle-lang.github.io/program)) and Answer Set Programming (as implemented in systems +like [Potassco](https://potassco.org/)). + +Dusa lives online at [dusa.rocks](https://dusa.rocks/). + +# Quick start + +## Introduction to Datalog + +Datalog-like languages try to use logical implication to express the sorts of problems that, in a +language like SQL, you would solve with database joins. The simplest declarations in Dusa are just +declaring facts, like who a character's parent is. + + parent "Arya" "Catelyn". + parent "Arya" "Eddard". + parent "Brandon" "Rickard". + parent "Eddard" "Lyarra". + parent "Eddard" "Rickard". + parent "Rickard" "Edwyle". + parent "Rickard" "Marna". + parent "Sansa" "Catelyn". + parent "Sansa" "Eddard". + +You can use these facts and logical implication to derive more facts, like "if X's parent is Y, and Y's +parent is Z, then the grandparent of X is Z." That looks like this: + + grandparent X Z :- parent X Y, parent Y Z. + +It's also easy to have inferences that build on each other: an ancestor is either your parent or an +ancestor of your parent. In Dusa, that looks like this: + + ancestor X Y :- parent X Y. + ancestor X Z :- parent X Y, ancestor Y Z. + +Using these rules, Dusa will calculate all of Arya's ancestors: Catelyn, Eddard, Edwyle, Marna, and +Rickard. + +## Propositions: relations and functions + +The propositions in the previous section were all _relations_. Each of `parent`, `grandparent`, +and `ancestor` were relations between two characters. + +It's also possible to have propositions that are functions. + +- Relations look like this: `prop t1 t2 ... tn-1 tn` +- Functions look like this: `prop t1 t2 ... tn-1 is tn` + +A function describes a unique key-value relationship. Familiar relationships don't work like that: Arya +has multiple parents and Eddard has multiple children. But we could use `weapon Char is W` as a +functional proposition to describe a character's favorite weapon. + + weapon "Arya" is "smallsword". + weapon "Eddard" is "greatsword". + weapon "Sansa" is "bow". + +## Integrity constraints + +Functional propositions create integrity constraints on the database of facts that Dusa maintains. +If these constraints are violated by saying that multiple keys map to the same value, then the database +is thrown out completely. + +Consider trying to make `sibling` a functional proposition instead of a relational proposition in our +example, like this: + + sibling A is B :- parent A P, parent B P, A != B. + +This will work initially, deriving that Arya and Sansa are siblings, as are Brandon and Eddard. But if +we then add a seemingly innoccuous additional fact... + + parent "Bran" "Eddard". + +...then Dusa will report that there are no solutions. By trying to derive both `sibling "Arya" is +"Sansa"` and `sibling "Arya" is "Bran"`, the database failed an integrity constraint. The right solution +here is to make the `sibling` relationship a relation, not a function. + +Integrity constraints can also be added with the `#forbid` and `#demand` directives. If we want to +insist that no two characters have the same weapon, we can write. + + #forbid weapon Char1 is W, weapon Char2 is W, Char1 != Char2. + +Note that it's necessary to say `Char1 != Char2`. If we left that out, Dusa could match both `Char1` +and `Char2` to `"Arya"` and therefore invalidate the database for violating an integrity constraint. + +A `#demand` predicate expresses something that must be true in order for the database to be valid. This +can be used like an assertion in programming, invalidating the database if an expected fact doesn't +hold. If we want to make sure we derive Marna as an ancestor of Arya, we can write this: + + #demand ancestor "Arya" "Marna". + +## Introduction to answer set programming + +Answer set programming is a way of writing Datalog-like programs to compute acceptable models (answer +sets) that meet certain contraints. Whereas traditional Datalog aims to compute just one database (or +zero databases, if an integrity constraint fails), answer set programming allows different choices to +be made that let multiple possible databases diverge. + +Dusa allows this kind of programming by supporting mutually exclusive assignments to a functional +predicate. Any assignment which satisfies all integrity constraints is a valid solution. (Answer set +programming calls them "answer sets" or "models," Dusa calls them "solutions," but they're the same +concept.) + +If we have three suspects, Amy, Harry, and Sally, we can assign each of them guilt or +innocence with the following program: + + suspect amy. + suspect harry. + suspect sally. + + guilt Susp is { innocent, guilty } :- suspect Susp. + +Dusa will, in no particular order, generate eight different solutions, corresponding to the two +different guilt assignments for the three suspects. + +If we then add a constraint that only one suspect may be guilty... + + #forbid guilt Susp1 is guilty, guilt Susp2 is guilty, Susp1 != Susp2. + +...Dusa will only be able to generate four solutions, one where each suspect is guilty and one where all +suspects are innocent. If we want someone to be guilty, which would limit us to three models, we can specify +that too: + + #demand guilt _ is guilty. + +# Syntax + +## Lexical tokens + +- A `` matches `/[A-Z][a-zA-Z0-9_]*/` +- A `` matches `/_[a-zA-Z0-9_]*/` and represents variable names that you wish to be ignored. +- An `` matches `/[a-z][a-zA-Z0-9_]` +- A `` is a regular string constant with no escape characters: two double quotes `"` + surrounding any ASCII character in the range 32-126 except for `"` and `\`. +- An `` matches `/0|-?[1-9][0-9]*/` + +## Grammar + + ::= | "" + ::= "#builtin" [ "." ] + | "#demand" "." + | "#forbid" "." + | ":-" "." + + ::= | "," + ::= "!=" + | "==" + | + | "is" + + ::= + | "is" + | "is" "{" "}" + ::= | "?" | "," + ::- | "?" + + ::= | + ::= | + ::= | + | | + | | + | "(" ")" + ::= + | + | + ::= "INT_PLUS" | "INT_MINUS" + | "NAT_ZERO" | "NAT_SUCC" + | "STRING_CONCAT" + +## Built-in values and constructors + +On their own, built-in numbers and strings act no different than random uninterpreted constants, +but they can be manipualted with special constructors added by `#builtin` declarations. + +A `#builtin` declarations change the lexer to represent certain identifiers as operations on built-in +types. If you write + + #builtin INT_PLUS plus + #builtin NAT_SUCC s + +then the identifiers `plus` and `s` will be parsed as `` instead of as regular +identifiers until those built-ins are redefined. + +- The `NAT_ZERO` builtin takes no arguments and represents the natural number zero. +- The `NAT_SUCC` builtin takes one natural number argument, and adds one to it. If `NAT_SUCC` is `s`, + then the premise `s X == 0` will always fail, since `X` would have to be negative for that solution + to work. +- The `INT_PLUS` builtin takes two or more integer arguments and adds them all. +- The `INT_MINUS` builtin takes two integer arguments and returns an integer, subtracting the second + from the first. +- The `STRING_CONCAT` builtin takes two or more string arguments and concatenates them. diff --git a/index.html b/index.html index 0a221a5..3bb1341 100644 --- a/index.html +++ b/index.html @@ -23,7 +23,9 @@
- +
diff --git a/src/datalog/dusa-tokenizer.ts b/src/datalog/dusa-tokenizer.ts index d3296db..738bdbe 100644 --- a/src/datalog/dusa-tokenizer.ts +++ b/src/datalog/dusa-tokenizer.ts @@ -43,7 +43,7 @@ const CONST_TOKEN = /^[a-z][a-zA-Z0-9_]*$/; const WILDCARD_TOKEN = /^_[a-zA-Z0-9_]*$/; const VAR_TOKEN = /^[A-Z][a-zA-Z0-9_]*$/; const INT_TOKEN = /^-?(0|[1-9][0-9]*)$/; -const STRING_CONTENTS = /^[a-zA-Z0-9`~!@#$%^&*()\-_+=,<.>?;:'{[}\]| ]*/; +const STRING_CONTENTS = /^[ !#-[\[-~]*/; const TRIV_TOKEN = /^\(\)/; function issue(stream: StringStream, msg: string): Issue { diff --git a/src/dusa.css b/src/dusa.css index eae7875..2abf13d 100644 --- a/src/dusa.css +++ b/src/dusa.css @@ -111,9 +111,18 @@ main { padding: 0 0 10px 0; } -.dk-logo { +.dk-logo a { font-size: 1.5rem; padding-right: var(--dk-medium-padding); + color: var(--oksolar-text-emph); + text-decoration: none; +} + +.dk-logo a:hover { + color: var(--oksolar-text-emph-highlight); + text-decoration-color: var(--oksolar-text-emph-highlight); + text-decoration-line: underline; + text-decoration-style: solid; } .dk-session { @@ -252,7 +261,9 @@ main { } .dk-view-edit-warning a { - text-decoration: solid underline var(--oksolar-text-emph); + text-decoration-color: var(--oksolar-text-emph); + text-decoration-line: underline; + text-decoration-style: solid; color: var(--oksolar-text-emph); }