diff --git a/README.md b/README.md index 05edfca..0c8d000 100644 --- a/README.md +++ b/README.md @@ -336,9 +336,16 @@ Pre-commit hooks are configured in `.pre-commit-config.yaml`. This project is licensed under the GNU General Public License v3.0 or later. See [LICENSE.md](LICENSE.md) for details. +## Documentation + +For comprehensive documentation including tutorials, API reference, and examples, visit: + +- **[DS Documentation](https://ustc-knowledgecomputinglab.github.io/ds)** + ## Repository - **GitHub**: [USTC-KnowledgeComputingLab/ds](https://github.com/USTC-KnowledgeComputingLab/ds) +- **Documentation**: [ustc-knowledgecomputinglab.github.io/ds](https://ustc-knowledgecomputinglab.github.io/ds) - **npm package**: [atsds](https://www.npmjs.com/package/atsds) - **PyPI package**: [apyds](https://pypi.org/project/apyds/) diff --git a/docs/api/cpp.md b/docs/api/cpp.md index eadc7be..8d59f99 100644 --- a/docs/api/cpp.md +++ b/docs/api/cpp.md @@ -550,3 +550,73 @@ std::unique_ptr rule_to_text(rule_t* rule, length_t length); - `length`: Maximum size for the resulting text **Returns:** A unique_ptr to the text, or nullptr if length exceeded. + +--- + +## Complete Example + +Here's a complete example demonstrating the C++ API: + +```cpp +#include +#include +#include +#include +#include + +int main() { + const int buffer_size = 1000; + + // Create terms using utility functions + auto term = ds::text_to_term("(f `x `y)", buffer_size); + + std::cout << "Term: " << ds::term_to_text(term.get(), buffer_size).get() << std::endl; + + // Work with rules + auto fact = ds::text_to_rule("(parent john mary)", buffer_size); + auto rule = ds::text_to_rule("(father `X `Y)\n----------\n(parent `X `Y)\n", buffer_size); + + std::cout << "\nFact:\n" << ds::rule_to_text(fact.get(), buffer_size).get(); + std::cout << "Rule premises: " << rule->premises_count() << std::endl; + std::cout << "Rule conclusion: " << ds::term_to_text(rule->conclusion(), buffer_size).get() << std::endl; + + // Search engine + ds::search_t search(1000, 10000); + + // Add rules and facts + search.add("p q"); // p implies q + search.add("q r"); // q implies r + search.add("p"); // fact: p + + std::cout << "\nRunning inference:" << std::endl; + + // Execute search + auto target = ds::text_to_rule("r", buffer_size); + bool found = false; + + while (!found) { + auto count = search.execute([&](ds::rule_t* candidate) { + std::cout << " Derived: " << ds::rule_to_text(candidate, buffer_size).get(); + + // Check if this is our target + if (candidate->data_size() == target->data_size() && + memcmp(candidate->head(), target->head(), candidate->data_size()) == 0) { + found = true; + return true; // Stop + } + return false; // Continue + }); + + if (count == 0) { + std::cout << " (no more inferences)" << std::endl; + break; + } + } + + if (found) { + std::cout << "Target found!" << std::endl; + } + + return 0; +} +``` diff --git a/docs/api/python.md b/docs/api/python.md index ef49eb2..fb37a3a 100644 --- a/docs/api/python.md +++ b/docs/api/python.md @@ -452,3 +452,63 @@ def callback(candidate): search.execute(callback) ``` + +--- + +## Complete Example + +Here's a complete example demonstrating most of the API: + +```python +import apyds + +# Configure buffer size for operations +apyds.buffer_size(2048) + +# Create terms +var = apyds.Variable("`X") +item = apyds.Item("hello") +lst = apyds.List("(a b c)") +term = apyds.Term("(f `x `y)") + +print(f"Variable: {var}, name: {var.name}") +print(f"Item: {item}, name: {item.name}") +print(f"List: {lst}, length: {len(lst)}") +print(f"Term: {term}, type: {type(term.term)}") + +# Work with rules +fact = apyds.Rule("(parent john mary)") +rule = apyds.Rule("(father `X `Y)\n----------\n(parent `X `Y)\n") + +print(f"\nFact: {fact}") +print(f"Rule premises: {len(rule)}, conclusion: {rule.conclusion}") + +# Grounding +term_a = apyds.Term("`a") +dictionary = apyds.Term("((`a hello))") +grounded = term_a // dictionary +print(f"\nGrounding `a with ((` hello)): {grounded}") + +# Matching +mp = apyds.Rule("(`p -> `q)\n`p\n`q\n") +axiom = apyds.Rule("((A) -> B)") +matched = mp @ axiom +print(f"\nMatching modus ponens with (A -> B):\n{matched}") + +# Search engine +search = apyds.Search(1000, 10000) +search.add("p q") # p implies q +search.add("q r") # q implies r +search.add("p") # fact: p + +print("\nRunning inference:") +for i in range(3): + count = search.execute(lambda r: print(f" Derived: {r}") or False) + if count == 0: + break + +# Using context manager for buffer size +with apyds.scoped_buffer_size(4096): + big_term = apyds.Term("(a b c d e f g h i j)") + print(f"\nBig term: {big_term}") +``` diff --git a/docs/api/typescript.md b/docs/api/typescript.md index e1a74ff..cbf6b49 100644 --- a/docs/api/typescript.md +++ b/docs/api/typescript.md @@ -447,3 +447,79 @@ search.execute((candidate) => { return false; // Continue searching }); ``` + +--- + +## Complete Example + +Here's a complete example demonstrating most of the TypeScript API: + +```typescript +import { + buffer_size, + string_t, + variable_t, + item_t, + list_t, + term_t, + rule_t, + search_t +} from "atsds"; + +// Configure buffer size +buffer_size(2048); + +// Create terms +const varX = new variable_t("`X"); +const item = new item_t("hello"); +const lst = new list_t("(a b c)"); +const term = new term_t("(f `x `y)"); + +console.log(`Variable: ${varX.toString()}, name: ${varX.name().toString()}`); +console.log(`Item: ${item.toString()}, name: ${item.name().toString()}`); +console.log(`List: ${lst.toString()}, length: ${lst.length()}`); +console.log(`Term: ${term.toString()}`); + +// Work with rules +const fact = new rule_t("(parent john mary)"); +const rule = new rule_t("(father `X `Y)\n----------\n(parent `X `Y)\n"); + +console.log(`\nFact: ${fact.toString()}`); +console.log(`Rule premises: ${rule.length()}, conclusion: ${rule.conclusion().toString()}`); + +// Grounding +const termA = new term_t("`a"); +const dictionary = new term_t("((`a hello))"); +const grounded = termA.ground(dictionary); +if (grounded) { + console.log(`\nGrounding \`a with ((\`a hello)): ${grounded.toString()}`); +} + +// Matching +const mp = new rule_t("(`p -> `q)\n`p\n`q\n"); +const axiom = new rule_t("((A) -> B)"); +const matched = mp.match(axiom); +if (matched) { + console.log(`\nMatching modus ponens with (A -> B):\n${matched.toString()}`); +} + +// Search engine +const search = new search_t(1000, 10000); +search.add("p q"); // p implies q +search.add("q r"); // q implies r +search.add("p"); // fact: p + +console.log("\nRunning inference:"); +for (let i = 0; i < 3; i++) { + const count = search.execute((r) => { + console.log(` Derived: ${r.toString()}`); + return false; + }); + if (count === 0) break; +} + +// Copying and comparison +const rule1 = new rule_t("(a b c)"); +const rule2 = rule1.copy(); +console.log(`\nRule comparison: ${rule1.key() === rule2.key()}`); // true +``` diff --git a/docs/concepts/rules.md b/docs/concepts/rules.md index a6e837d..b4f8f38 100644 --- a/docs/concepts/rules.md +++ b/docs/concepts/rules.md @@ -11,7 +11,7 @@ A rule consists of: ### Text Representation -Rules are written with premises and conclusion separated by dashes: +Rules are written with premises and conclusion separated by dashes (at least four dashes): ``` premise1 @@ -33,6 +33,31 @@ Or explicitly: (parent john mary) ``` +!!! info "Rule Format Details" + - Premises are separated by newlines + - The separator line must contain at least 4 dashes (`----`) between premises and conclusion + - Whitespace around premises and conclusion is trimmed + - A rule without an premises is a fact + +### Compact Rule Format + +For rules with multiple premises, you can use space-separated terms on a single line: + +``` +(`P -> `Q) `P `Q +``` + +This is equivalent to: + +``` +(`P -> `Q) +`P +---------- +`Q +``` + +The last term is the conclusion, and all preceding terms are premises. + ### Examples **Modus Ponens** (if P implies Q and P is true, then Q is true): diff --git a/docs/concepts/search.md b/docs/concepts/search.md index 75fd747..13e216e 100644 --- a/docs/concepts/search.md +++ b/docs/concepts/search.md @@ -9,6 +9,16 @@ The search engine: 1. Maintains a collection of rules and facts 2. Iteratively applies rules to generate new facts 3. Notifies you of each new inference via a callback +4. Automatically prevents duplicate inferences + +!!! info "How It Works" + The search engine uses a forward-chaining inference approach: + + 1. When you call `execute()`, the engine tries to match the first premise of each rule with existing facts + 2. When a match is found, variables in the rule are substituted and a new rule (with one fewer premise) is created + 3. If the new rule has no premises, it becomes a new fact + 4. The callback is invoked for each newly derived rule + 5. Duplicate rules are automatically filtered out ## Creating a Search Engine @@ -21,7 +31,7 @@ The search engine: search = apyds.Search() # Create with custom sizes - search = apyds.Search(limit_size=2000, buffer_size=20000) + search = apyds.Search(limit_size=1000, buffer_size=10000) ``` === "TypeScript" @@ -33,7 +43,7 @@ The search engine: const search = new search_t(); // Create with custom sizes - const search2 = new search_t(2000, 20000); + const search2 = new search_t(1000, 10000); ``` === "C++" @@ -47,8 +57,8 @@ The search engine: ### Parameters -- **limit_size**: Maximum size (in bytes) for each stored rule/fact (default: 1000) -- **buffer_size**: Size of the internal buffer for intermediate operations (default: 10000) +- **limit_size**: Maximum size (in bytes) for each stored rule/fact (default: 1000). Rules or facts larger than this are rejected. +- **buffer_size**: Size of the internal buffer for intermediate operations (default: 10000). Increase this if you work with complex rules. ## Adding Rules and Facts @@ -66,11 +76,6 @@ Use the `add()` method to add rules and facts to the knowledge base. # Add a rule with premises search.add("(father `X `Y)\n----------\n(parent `X `Y)\n") - - # Add multiple facts and rules - search.add("(father john mary)") - search.add("(father john bob)") - search.add("(mother mary alice)") ``` === "TypeScript" @@ -298,6 +303,7 @@ Clears all rules and facts: 2. **Limit Size**: Restricts maximum rule/fact complexity - too small may reject valid rules 3. **Iterative Execution**: Call `execute()` in a loop to continue inference until convergence 4. **Early Termination**: Return `true` from callback to stop as soon as target is found +5. **Deduplication**: The engine automatically deduplicates facts, avoiding redundant computation ## See Also diff --git a/docs/concepts/terms.md b/docs/concepts/terms.md index 89a9547..dace095 100644 --- a/docs/concepts/terms.md +++ b/docs/concepts/terms.md @@ -17,7 +17,10 @@ Variables are placeholders that can be unified with other terms during inference `Q ``` -Variables are used in rules to represent any term that can match during unification. +Variables are used in rules to represent any term that can match during unification. During the inference process, variables can be bound to specific terms through unification. + +!!! tip "Variable Naming" + Variable names can contain any characters except backtick, whitespace and parentheses. By convention, single uppercase letters like `` `X``, `` `P``, `` `Q`` are often used for simple logic, while descriptive names like `` `person`` or `` `result`` improve readability in complex rules. ### Items @@ -35,6 +38,10 @@ Items can represent: - **Constants**: Atomic values like `john`, `mary`, `42` - **Functors**: Symbols that combine other terms, like `father`, `->`, `!` +- **Operators**: Special symbols used in logical expressions, like `->` for implication or `!` for negation + +!!! note "Item Characters" + Items can contain any characters except backtick, whitespace and parentheses. Special symbols like `->`, `!`, `<-`, `&&`, `||` are commonly used as logical operators. ### Lists @@ -47,7 +54,19 @@ Lists are ordered sequences of terms enclosed in parentheses. They can contain a (! (! X)) ``` -Lists are the primary way to build complex structures in the deductive system. +Lists are the primary way to build complex structures in the deductive system. They can represent: + +- **Relations**: `(father john mary)` - "John is the father of Mary" +- **Logical expressions**: `(P -> Q)` - "P implies Q" +- **Nested structures**: `(! (! X))` - "not not X" (double negation) +- **Data collections**: `(1 2 3 4 5)` - a list of numbers + +!!! example "List Nesting" + Lists can be nested to any depth: + ``` + ((a b) (c d) (e f)) + (if (> `x 0) (positive `x) (non-positive `x)) + ``` ## Creating Terms @@ -107,19 +126,12 @@ Lists are the primary way to build complex structures in the deductive system. #include int main() { - // Create a variable - auto var = ds::text_to_variable("`X", 1000); - - // Create an item - auto item = ds::text_to_item("hello", 1000); - - // Create a list - auto lst = ds::text_to_list("(a b c)", 1000); - std::cout << "List length: " << lst->length() << std::endl; - // Create a generic term auto term = ds::text_to_term("(f `x)", 1000); - + // Access the underlying type + auto list = term->list(); + auto item = list->term(0)->item(); + auto variable = list->term(1)->variable(); return 0; } ``` @@ -256,7 +268,7 @@ Renaming adds prefixes and/or suffixes to all variables in a term. This is usefu ## Buffer Size -Operations like grounding and renaming require buffer space for intermediate results. You can control this using buffer size functions. +Operations like grounding and renaming require buffer space for intermediate results in TypeScript/Javascript and Python. You can control this using buffer size functions. === "TypeScript" diff --git a/docs/getting-started/installation.md b/docs/getting-started/installation.md index 3e59aac..2c33b0b 100644 --- a/docs/getting-started/installation.md +++ b/docs/getting-started/installation.md @@ -20,6 +20,19 @@ The package includes: - Node.js 20+ or a modern browser with WebAssembly support +### Browser Usage + +The package works in browsers that support WebAssembly: + +```html + +``` + ## Python The Python package `apyds` wraps the C++ core via pybind11. @@ -31,7 +44,17 @@ pip install apyds ### Requirements - Python 3.10-3.14 -- Pre-built wheels are available for common platforms +- Pre-built wheels are available for common platforms (Linux, macOS, Windows) + +### Virtual Environment (Recommended) + +It's recommended to use a virtual environment: + +```bash +python -m venv venv +source venv/bin/activate # On Windows: venv\Scripts\activate +pip install apyds +``` ### Development Installation @@ -49,7 +72,7 @@ The C++ library is the core implementation. Both Python and TypeScript bindings ### Prerequisites -- C++20 compatible compiler +- C++20 compatible compiler (GCC 10+, Clang 10+, MSVC 2019+) - CMake 3.30+ ### Building from Source @@ -99,6 +122,30 @@ cmake -B build cmake --build build ``` +## Running Tests + +After installation, you can verify everything works by running the tests: + +### TypeScript/JavaScript Tests + +```bash +npm test +``` + +### Python Tests + +```bash +pip install pytest +pytest +``` + +### C++ Tests + +```bash +cd build +ctest +``` + ## Verifying Installation === "TypeScript" @@ -108,17 +155,17 @@ cmake --build build const term = new term_t("(hello world)"); console.log(term.toString()); + // Output: (hello world) ``` === "Python" ```python import apyds - print(apyds.__version__) + print(f"Version: {apyds.__version__}") - # Create a simple term term = apyds.Term("(hello world)") - print(term) + print(term) # (hello world) ``` === "C++" diff --git a/docs/getting-started/quickstart.md b/docs/getting-started/quickstart.md index 3f612c1..9d93b64 100644 --- a/docs/getting-started/quickstart.md +++ b/docs/getting-started/quickstart.md @@ -52,14 +52,7 @@ Terms are the basic building blocks of the deductive system. A term can be: #include int main() { - auto var = ds::text_to_variable("`X", 1000); - auto item = ds::text_to_item("hello", 1000); - auto lst = ds::text_to_list("(a b c)", 1000); auto term = ds::text_to_term("(f `x a)", 1000); - - std::cout << "Variable: " << ds::variable_to_text(var.get(), 1000).get() << std::endl; - std::cout << "Item: " << ds::item_to_text(item.get(), 1000).get() << std::endl; - std::cout << "List: " << ds::list_to_text(lst.get(), 1000).get() << std::endl; std::cout << "Term: " << ds::term_to_text(term.get(), 1000).get() << std::endl; return 0; } @@ -111,8 +104,8 @@ Rules represent logical inference steps. A rule has premises (conditions) and a auto fact = ds::text_to_rule("(parent john mary)", 1000); auto rule = ds::text_to_rule("(father `X `Y)\n----------\n(parent `X `Y)\n", 1000); - std::cout << "Fact: " << ds::rule_to_text(fact.get(), 1000).get() << std::endl; std::cout << "Rule premises: " << rule->premises_count() << std::endl; + std::cout << "Rule conclusion: " << ds::rule_to_text(fact->conclusion(), 1000).get() << std::endl; return 0; } ``` diff --git a/docs/index.md b/docs/index.md index 9895fc4..9445cfd 100644 --- a/docs/index.md +++ b/docs/index.md @@ -12,54 +12,49 @@ A deductive system for logical inference, implemented in C++. The library provid - **WebAssembly**: Run inference in the browser or Node.js environments - **Type-Safe**: Strong typing support in TypeScript and Python -## Quick Links - -- **[Installation](getting-started/installation.md)** - Install DS for your preferred language -- **[Quick Start](getting-started/quickstart.md)** - Get up and running in minutes -- **[Core Concepts](concepts/terms.md)** - Learn about terms, rules, and inference -- **[API Reference](api/python.md)** - Complete API documentation - ## Supported Languages -=== "Python" - - ```python - import apyds - - search = apyds.Search(1000, 10000) - search.add("(`P -> `Q) `P `Q") # Modus ponens - search.add("(! (! X))") # Premise: !!X - - target = apyds.Rule("X") - # ... execute search - ``` - === "TypeScript" ```typescript - import { rule_t, search_t } from "atsds"; + import { term_t } from "atsds"; + + const term = new term_t("(hello world)"); + console.log(term.toString()); + // Output: (hello world) + ``` - const search = new search_t(1000, 10000); - search.add("(`P -> `Q) `P `Q"); // Modus ponens - search.add("(! (! X))"); // Premise: !!X +=== "Python" - const target = new rule_t("X"); - // ... execute search + ```python + import apyds + print(f"Version: {apyds.__version__}") + + term = apyds.Term("(hello world)") + print(term) # (hello world) ``` === "C++" ```cpp #include - #include + #include + #include + + int main() { + auto term = ds::text_to_term("(hello world)", 1000); + std::cout << ds::term_to_text(term.get(), 1000).get() << std::endl; + return 0; + } + ``` - ds::search_t search(1000, 10000); - search.add("(`P -> `Q) `P `Q"); // Modus ponens - search.add("(! (! X))"); // Premise: !!X +## Quick Links - auto target = ds::text_to_rule("X", 1000); - // ... execute search - ``` +- **[Installation](getting-started/installation.md)** - Install DS for your preferred language +- **[Quick Start](getting-started/quickstart.md)** - Get up and running in minutes +- **[Core Concepts](concepts/terms.md)** - Learn about terms, rules, and inference +- **[API Reference](api/python.md)** - Complete API documentation +- **[Examples](examples/basic.md)** - Working code examples ## License diff --git a/package.json b/package.json index 865b04c..5e54a0a 100644 --- a/package.json +++ b/package.json @@ -8,7 +8,10 @@ "url": "https://github.com/USTC-KnowledgeComputingLab/ds.git" }, "type": "module", + "exports": "./dist/tsds.mjs", "main": "dist/tsds.mjs", + "module": "dist/tsds.mjs", + "browser": "dist/tsds.mjs", "types": "dist/tsds.d.mts", "files": [ "dist/ds.mjs",