Initial #lazy directive for the lazy/magic/demand transformation

docs/astro.config.mjs

@@ -54,6 +54,7 @@ export default defineConfig({
             { label: 'Terms and variables', link: '/docs/language/terms/' },
             { label: 'Constraints', link: '/docs/language/constraints/' },
             { label: 'Builtins', link: '/docs/language/builtin/' },
+            { label: 'Lazy predicates', link: '/docs/language/lazy/' },
             { label: 'Syntax specification', link: '/docs/language/syntax/' },
           ],
         },

docs/src/content/docs/docs/language/lazy.mdx

@@ -0,0 +1,80 @@
+---
+title: Lazy predicates (experimental)
+---
+
+import Dusa from '../../../../components/Dusa.astro';
+
+**WARNING: this is an unusually experimental feature introduced in 0.1.3 and
+is likely to break, change, or be removed in future releases.**
+
+Lazy predicates allow a limited form of "backward-chaining," or 
+"Prolog-style," or "top-down" logic programming in Dusa. Normally, a program
+like this one will never terminate, because you can always generate new
+`nat` facts once you start generating them:
+
+<Dusa predicates={['nat']} code={`
+
+nat z.
+nat (s N) :- nat N.
+
+`}/>
+
+However, by making `nat` a "lazy" predicate, we only derive the `nat` facts
+that we absolutely need to run other parts of our program.
+
+<Dusa predicates={['nat', 'p', 'q']} code={`
+
+#lazy nat
+nat z.
+nat (s N) :- nat N.
+
+p (s (s z)).
+p "hello".
+p 4.
+
+q X :- p X, nat X.
+
+`}/>
+
+[Explore this example](https://dusa.rocks/#jsonz=q1YqUbJSyi9IzVPSUUrJTy7NTc0DiSjnJFZVKuQllsTkAQmFKj0IrVGs4KepYKULklHwAwrG5BWABIGoSlNTD8SLUcpIzcnJj1EC80zAagoVIkCaChQidMA6I4CiSrUA)
+
+Dusa implements lazy predicates by applying a program transformation called
+the "magic sets" or "demand" transformation. It's helpful to have a bit of a
+mental model of how this transformation actually works. The program above is
+transformed into (more or less) this program by the demand transformation:
+
+<Dusa predicates={['nat', 'p', 'q']} code={`
+
+#lazy nat
+nat z :- demand_nat z.
+nat (s N) :- demand_nat (s N), nat N.
+demand_nat N :- demand_nat (s N).
+
+p (s (s z)).
+p "hello".
+p 4.
+
+q X :- p X, nat X.
+demand_nat X :- p X.
+
+`}/>
+
+## Inputs and outputs
+
+The simple lazy transformation currently implemented treats the arguments to
+a lazy predicate as "inputs", which means that whenever they appear in a
+premise they have to be bound by previous premises. The exception is the value
+of a functional predicate, which is treated as an output. That allows for the
+writing of (some) Prolog-style logic programs that compute values, like this:
+
+<Dusa predicates={['plus']} code={`
+
+#lazy plus
+plus z N is N.
+plus (s N) M is (s P) :- plus N M is P.
+
+#demand plus (s (s (s (s z)))) (s (s (s z))) is N.
+
+`}/>
+
+[Explore this example](https://dusa.rocks/#jsonz=q1YqUbJSyi9IzVPSUUrJTy7NTc0DiSjnJFZVKhTklBbH5IFIhSoFP4XMYgU_PShfo1jBT1PBFySmUawQoKlgpQtWruAHEQzQi8mLyVNOSc1NzEtRgGmBoypNTU1NVC7EeKVaAA)

docs/src/content/docs/docs/language/syntax.md

@@ -19,6 +19,7 @@ treated like whitespace.
 
     <program>         ::= <declaration> <program> | ""
     <declaration>     ::= "#builtin" <builtin> <identifier> [ "." ]
+                       |  "#lazy" <identifier> ["."]
                        |  "#demand" <premises> "."
                        |  "#forbid" <premises> "."
                        |  <conclusion> [ ":-" <premises> ] "."

package.json

@@ -1,6 +1,6 @@
 {
   "name": "dusa",
-  "version": "0.1.2",
+  "version": "0.1.3",
   "type": "module",
   "main": "lib/client.js",
   "unpkg": "./dusa.umd.js",

src/bytecode.ts

@@ -26,6 +26,7 @@ export interface ProgramN<Int> {
   demands: string[];
   rules: RuleN<Int>[];
   arities: { [pred: string]: { args: number; value: boolean } };
+  lazy: string[];
 }
 
 /**

src/client.test.ts

@@ -209,3 +209,21 @@ test('Builtin INT_MINUS (issue #29)', () => {
     solutions(new Dusa("#builtin INT_MINUS minus.\ny 4.\nx N :- y N', minus N 1 is N'."), 'x'),
   ).toStrictEqual(['x 5']);
 });
+
+test('Lazy execution', () => {
+  expect(
+    solutions(
+      new Dusa(`
+      #lazy lt
+      lt z (s N).
+      lt (s N) (s M) :- lt N M.
+
+      p (s (s (s z))).
+      p (s z).
+      p z.
+
+      res X Y :- p X, p Y, lt X Y.
+    `),
+    ),
+  ).toStrictEqual(['res (s z) (s (s (s z))), res z (s (s (s z))), res z (s z)']);
+});

src/client.ts

@@ -143,12 +143,12 @@ export class Dusa {
       if (parsed.errors !== null) {
         throw new DusaError(parsed.errors);
       }
-      const { errors, arities, builtins } = check(parsed.document);
+      const { errors, arities, builtins, lazy } = check(parsed.document);
       if (errors.length !== 0) {
         throw new DusaError(errors);
       }
 
-      bytecodeProgram = compile(builtins, arities, parsed.document);
+      bytecodeProgram = compile(builtins, arities, lazy, parsed.document);
     } else {
       bytecodeProgram = source;
     }
@@ -224,12 +224,12 @@ export class Dusa {
     if (parsed.errors !== null) {
       throw new DusaError(parsed.errors);
     }
-    const { errors, arities, builtins } = check(parsed.document);
+    const { errors, arities, builtins, lazy } = check(parsed.document);
     if (errors.length !== 0) {
       throw new DusaError(errors);
     }
 
-    const bytecodeProgram = compile(builtins, arities, parsed.document);
+    const bytecodeProgram = compile(builtins, arities, lazy, parsed.document);
     return bytecodeToJSON(bytecodeProgram);
   }
 }

src/language/binarize.test.ts

@@ -12,11 +12,12 @@ import { BUILT_IN_PRED } from './dusa-builtins.js';
 import { check } from './check.js';
 import { ParsedDeclaration } from './syntax.js';
 import { Pattern } from './terms.js';
+import { transformLazy } from './lazy.js';
 
 export function srcToBinarized(source: string) {
   const parsed = parse(source);
   if (parsed.errors !== null) throw parsed.errors;
-  const { errors, arities, builtins } = check(parsed.document);
+  const { errors, arities, builtins, lazy } = check(parsed.document);
   if (errors.length !== 0) throw errors;
   const decls = parsed.document.filter((x): x is ParsedDeclaration => x.type !== 'Builtin');
   const flattened = flattenDecls(
@@ -37,7 +38,7 @@ export function srcToBinarized(source: string) {
       return `${str}-${count}`;
     }
   }
-  const named = flattened.map((decl) => ({
+  const named = transformLazy(lazy, flattened).map((decl) => ({
     decl,
     name: decl.type === 'Rule' ? nextName(decl.conclusion.name) : nextName(decl.type),
   }));

src/language/bytecode.test.ts

@@ -9,6 +9,7 @@ function srcToBytecode(source: string) {
   return generateBytecode(
     makeIntermediatePredicatesMatchJoinOrder(generateIndices(binarized)),
     new Map(),
+    new Set(),
   );
 }
 
@@ -21,6 +22,7 @@ test('builtins and functional predicates', () => {
     demands: [],
     forbids: [],
     arities: {},
+    lazy: [],
     seeds: ['$seed'],
     rules: [
       {
@@ -73,6 +75,7 @@ test('builtins and functional predicates', () => {
     demands: [],
     forbids: [],
     arities: {},
+    lazy: [],
     seeds: ['$seed'],
     rules: [
       {

src/language/bytecode.ts

@@ -91,6 +91,7 @@ function generateRule(rule: BinarizedRule): BytecodeRule {
 export function generateBytecode(
   program: BinarizedProgram,
   aritiesMap: Map<string, { args: number; value: boolean }>,
+  lazySet: Set<string>,
 ): BytecodeProgram {
   const arities: { [pred: string]: { args: number; value: boolean } } = {};
   for (const [pred, arity] of aritiesMap.entries()) {
@@ -102,6 +103,7 @@ export function generateBytecode(
     demands: program.demands,
     rules: program.rules.map(generateRule),
     arities,
+    lazy: [...lazySet],
   };
 }
 

src/language/check.test.ts

@@ -24,12 +24,14 @@ test('Static checks', () => {
       ['b', { args: 2, value: true }],
       ['c', { args: 0, value: true }],
     ]),
+    lazy: new Set(),
     errors: [],
   });
 
   expect(runCheck('a.\na 4.')).toStrictEqual({
     builtins: new Map(),
     arities: new Map([['a', { args: 0, value: false }]]),
+    lazy: new Set(),
     errors: [
       {
         type: 'Issue',
@@ -43,6 +45,7 @@ test('Static checks', () => {
   expect(runCheck('a is 4.\na 4.')).toStrictEqual({
     builtins: new Map(),
     arities: new Map([['a', { args: 0, value: true }]]),
+    lazy: new Set(),
     errors: [
       {
         type: 'Issue',
@@ -59,6 +62,7 @@ test('Static checks', () => {
       ['a', { args: 0, value: false }],
       ['b', { args: 2, value: false }],
     ]),
+    lazy: new Set(),
     errors: [
       {
         type: 'Issue',
@@ -179,6 +183,7 @@ test('Error messages for patterns', () => {
       ['c', { args: 1, value: false }],
     ]),
     builtins: new Map([['plus', 'INT_PLUS']]),
+    lazy: new Set(),
     errors: [],
   });
   expect(runCheck('#builtin INT_PLUS plus\na :- c _, b (plus 1 X).')).toStrictEqual({
@@ -188,6 +193,7 @@ test('Error messages for patterns', () => {
       ['c', { args: 1, value: false }],
     ]),
     builtins: new Map([['plus', 'INT_PLUS']]),
+    lazy: new Set(),
     errors: [
       {
         type: 'Issue',
@@ -199,3 +205,68 @@ test('Error messages for patterns', () => {
   });
   expect(runForErrors('a 3.\nb (a X).'));
 });
+
+test('Lazy', () => {
+  expect(runCheck('lt z (s N). lt (s N) (s M) :- lt N M.')).toStrictEqual({
+    arities: new Map([['lt', { args: 2, value: false }]]),
+    builtins: new Map(),
+    lazy: new Set(),
+    errors: [
+      {
+        type: 'Issue',
+        severity: 'error',
+        msg: "The variable 'N' can't be used in the conclusion of a rule without being used somewhere in a premise.",
+        loc: { start: { line: 1, column: 9, index: 8 }, end: { line: 1, column: 10, index: 9 } },
+      },
+    ],
+  });
+
+  expect(runCheck('#lazy lt\nlt z (s N).\nlt (s N) (s M) :- lt N M.')).toStrictEqual({
+    arities: new Map([['lt', { args: 2, value: false }]]),
+    builtins: new Map(),
+    lazy: new Set(['lt']),
+    errors: [],
+  });
+
+  expect(runCheck('#lazy s.\n#builtin NAT_SUCC s')).toStrictEqual({
+    arities: new Map(),
+    builtins: new Map([['s', 'NAT_SUCC']]),
+    lazy: new Set(['s']),
+    errors: [
+      {
+        type: 'Issue',
+        severity: 'error',
+        msg: `Cannot declare 's' as a lazy predicate when it is declared elsewhere as a builtin.`,
+        loc: { start: { line: 1, column: 1, index: 0 }, end: { line: 1, column: 9, index: 8 } },
+      },
+    ],
+  });
+
+  expect(runCheck('lt 1 2 is { tt, ff }.\n#lazy lt')).toStrictEqual({
+    arities: new Map([['lt', { args: 2, value: true }]]),
+    builtins: new Map(),
+    lazy: new Set(['lt']),
+    errors: [
+      {
+        type: 'Issue',
+        severity: 'error',
+        msg: "Lazily-computed relations can't use choices (lt is {...}) or open rules (lt is? ...).",
+        loc: { start: { line: 1, column: 1, index: 0 }, end: { line: 1, column: 21, index: 20 } },
+      },
+    ],
+  });
+
+  expect(runCheck('#lazy lt\nlt z (s N).\nlt (s N) (s M) :- lt N M2.')).toStrictEqual({
+    arities: new Map([['lt', { args: 2, value: false }]]),
+    builtins: new Map(),
+    lazy: new Set(['lt']),
+    errors: [
+      {
+        type: 'Issue',
+        severity: 'error',
+        msg: `The variable 'M2' is the input to a lazily-computed predicate, so must be bound by a previous premise.`,
+        loc: { start: { line: 3, column: 24, index: 44 }, end: { line: 3, column: 26, index: 46 } },
+      },
+    ],
+  });
+});