From 6b29bb3511ce80e3bfedc5f7ec2824a34b4c92bc Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 25 Nov 2025 12:29:48 +0000 Subject: [PATCH 1/7] Initial plan From bc3eaa5adf5a53fed9c4f18a98e597b34ac052c3 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 25 Nov 2025 12:41:49 +0000 Subject: [PATCH 2/7] Add MkDocs documentation setup with multi-language API docs Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com> --- .gitignore | 3 +- docs/api/cpp.md | 566 +++++++++++++++++++++++++++ docs/api/python.md | 71 ++++ docs/api/typescript.md | 440 +++++++++++++++++++++ docs/concepts/rules.md | 304 ++++++++++++++ docs/concepts/search.md | 305 +++++++++++++++ docs/concepts/terms.md | 238 +++++++++++ docs/examples/index.md | 166 ++++++++ docs/getting-started/installation.md | 136 +++++++ docs/getting-started/quickstart.md | 248 ++++++++++++ docs/index.md | 80 ++++ mkdocs.yml | 84 ++++ pyproject.toml | 5 + 13 files changed, 2645 insertions(+), 1 deletion(-) create mode 100644 docs/api/cpp.md create mode 100644 docs/api/python.md create mode 100644 docs/api/typescript.md create mode 100644 docs/concepts/rules.md create mode 100644 docs/concepts/search.md create mode 100644 docs/concepts/terms.md create mode 100644 docs/examples/index.md create mode 100644 docs/getting-started/installation.md create mode 100644 docs/getting-started/quickstart.md create mode 100644 docs/index.md create mode 100644 mkdocs.yml diff --git a/.gitignore b/.gitignore index 6e26988..a59b47f 100644 --- a/.gitignore +++ b/.gitignore @@ -12,4 +12,5 @@ node_modules coverage compile_commands.json _codeql_build_dir -_codeql_detected_source_root \ No newline at end of file +_codeql_detected_source_root +site \ No newline at end of file diff --git a/docs/api/cpp.md b/docs/api/cpp.md new file mode 100644 index 0000000..688d070 --- /dev/null +++ b/docs/api/cpp.md @@ -0,0 +1,566 @@ +# C++ API Reference + +The C++ API is the core implementation. Both Python and TypeScript bindings are built on top of it. + +All classes and functions are in the `ds` namespace. + +## Headers + +```cpp +#include // All basic types +#include // Search engine +#include // Helper functions +``` + +--- + +## string_t + +String handling class. Defined in ``. + +### Methods + +#### data_size() + +Get the size of the string data in bytes. + +```cpp +length_t data_size(); +``` + +#### head() + +Get a pointer to the first byte. + +```cpp +std::byte* head(); +``` + +#### tail() + +Get a pointer past the last byte. + +```cpp +std::byte* tail(); +``` + +#### print() + +Output the string to a buffer. + +```cpp +char* print(char* buffer, char* check_tail = nullptr); +``` + +#### scan() + +Read a string from a buffer. + +```cpp +const char* scan(const char* buffer, std::byte* check_tail = nullptr); +``` + +--- + +## variable_t + +Logical variable class. Defined in ``. + +Variables represent placeholders that can be unified with other terms. + +### Methods + +#### name() + +Get the name of the variable (without backtick prefix). + +```cpp +string_t* name(); +``` + +#### data_size() + +Get the size of the variable data in bytes. + +```cpp +length_t data_size(); +``` + +#### head() / tail() + +Get pointers to the data boundaries. + +```cpp +std::byte* head(); +std::byte* tail(); +``` + +#### print() / scan() + +Input/output operations. + +```cpp +char* print(char* buffer, char* check_tail = nullptr); +const char* scan(const char* buffer, std::byte* check_tail = nullptr); +``` + +--- + +## item_t + +Item (constant/functor) class. Defined in ``. + +Items represent atomic values or function symbols. + +### Methods + +#### name() + +Get the name of the item. + +```cpp +string_t* name(); +``` + +#### data_size() + +Get the size of the item data in bytes. + +```cpp +length_t data_size(); +``` + +#### head() / tail() + +Get pointers to the data boundaries. + +```cpp +std::byte* head(); +std::byte* tail(); +``` + +#### print() / scan() + +Input/output operations. + +```cpp +char* print(char* buffer, char* check_tail = nullptr); +const char* scan(const char* buffer, std::byte* check_tail = nullptr); +``` + +--- + +## list_t + +List class. Defined in ``. + +Lists contain ordered sequences of terms. + +### Methods + +#### length() + +Get the number of elements in the list. + +```cpp +length_t length(); +``` + +#### getitem() + +Get an element by index. + +```cpp +term_t* getitem(length_t index); +``` + +#### data_size() + +Get the size of the list data in bytes. + +```cpp +length_t data_size(); +``` + +#### head() / tail() + +Get pointers to the data boundaries. + +```cpp +std::byte* head(); +std::byte* tail(); +``` + +#### print() / scan() + +Input/output operations. + +```cpp +char* print(char* buffer, char* check_tail = nullptr); +const char* scan(const char* buffer, std::byte* check_tail = nullptr); +``` + +--- + +## term_t + +General term class. Defined in ``. + +A term can be a variable, item, or list. + +### Enum: term_type_t + +```cpp +enum class term_type_t : min_uint_t { + null = 0, + variable = 1, + item = 2, + list = 3 +}; +``` + +### Methods + +#### get_type() + +Get the type of this term. + +```cpp +term_type_t get_type(); +``` + +#### is_null() + +Check if the term is null. + +```cpp +bool is_null(); +``` + +#### variable() / item() / list() + +Get the underlying value as the specific type. Returns nullptr if the term is not of that type. + +```cpp +variable_t* variable(); +item_t* item(); +list_t* list(); +``` + +#### set_type() / set_null() / set_variable() / set_item() / set_list() + +Set the term type. + +```cpp +term_t* set_type(term_type_t type, std::byte* check_tail = nullptr); +term_t* set_null(std::byte* check_tail = nullptr); +term_t* set_variable(std::byte* check_tail = nullptr); +term_t* set_item(std::byte* check_tail = nullptr); +term_t* set_list(std::byte* check_tail = nullptr); +``` + +#### data_size() + +Get the size of the term data in bytes. + +```cpp +length_t data_size(); +``` + +#### head() / tail() + +Get pointers to the data boundaries. + +```cpp +std::byte* head(); +std::byte* tail(); +``` + +#### print() / scan() + +Input/output operations. + +```cpp +char* print(char* buffer, char* check_tail = nullptr); +const char* scan(const char* buffer, std::byte* check_tail = nullptr); +``` + +#### ground() + +Ground this term using a dictionary to substitute variables. + +```cpp +term_t* ground(term_t* term, term_t* dictionary, const char* scope, + std::byte* check_tail = nullptr); +``` + +#### match() + +Match two terms and produce a unification dictionary. + +```cpp +term_t* match(term_t* term_1, term_t* term_2, + const char* scope_1, const char* scope_2, + std::byte* check_tail = nullptr); +``` + +#### rename() + +Rename variables by adding prefix and suffix. + +```cpp +term_t* rename(term_t* term, term_t* prefix_and_suffix, + std::byte* check_tail = nullptr); +``` + +--- + +## rule_t + +Logical rule class. Defined in ``. + +A rule consists of premises and a conclusion. + +### Methods + +#### conclusion() + +Get the conclusion of the rule. + +```cpp +term_t* conclusion(); +``` + +#### only_conclusion() + +Get the conclusion only if there are no premises. Returns nullptr otherwise. + +```cpp +term_t* only_conclusion(); +``` + +#### premises() + +Get a premise by index. + +```cpp +term_t* premises(length_t index); +``` + +#### premises_count() + +Get the number of premises. + +```cpp +length_t premises_count(); +``` + +#### valid() + +Check if the rule is valid. + +```cpp +bool valid(); +``` + +#### data_size() + +Get the size of the rule data in bytes. + +```cpp +length_t data_size(); +``` + +#### head() / tail() + +Get pointers to the data boundaries. + +```cpp +std::byte* head(); +std::byte* tail(); +``` + +#### print() / scan() + +Input/output operations. + +```cpp +char* print(char* buffer, char* check_tail = nullptr); +const char* scan(const char* buffer, std::byte* check_tail = nullptr); +``` + +#### ground() + +Ground this rule using a dictionary. + +```cpp +rule_t* ground(rule_t* rule, term_t* dictionary, const char* scope, + std::byte* check_tail = nullptr); +rule_t* ground(rule_t* rule, rule_t* dictionary, const char* scope, + std::byte* check_tail = nullptr); +``` + +#### match() + +Match this rule with a fact. + +```cpp +rule_t* match(rule_t* rule_1, rule_t* rule_2, + std::byte* check_tail = nullptr); +``` + +#### rename() + +Rename variables in this rule. + +```cpp +rule_t* rename(rule_t* rule, rule_t* prefix_and_suffix, + std::byte* check_tail = nullptr); +``` + +--- + +## search_t + +Search engine class. Defined in ``. + +Manages a knowledge base and performs logical inference. + +### Constructor + +```cpp +search_t(length_t limit_size, length_t buffer_size); +``` + +**Parameters:** + +- `limit_size`: Maximum size for each stored rule/fact +- `buffer_size`: Size of the internal buffer for operations + +### Methods + +#### set_limit_size() + +Set the maximum rule/fact size. + +```cpp +void set_limit_size(length_t limit_size); +``` + +#### set_buffer_size() + +Set the internal buffer size. + +```cpp +void set_buffer_size(length_t buffer_size); +``` + +#### reset() + +Clear all rules and facts. + +```cpp +void reset(); +``` + +#### add() + +Add a rule or fact from text. + +```cpp +bool add(std::string_view text); +``` + +#### execute() + +Execute one round of inference. + +```cpp +length_t execute(const std::function& callback); +``` + +**Parameters:** + +- `callback`: Function called for each new inference. Return false to continue, true to stop. + +**Returns:** The number of new inferences generated. + +--- + +## Utility Functions + +Helper functions in ``. + +### text_to_* Functions + +Parse text into objects. Returns a unique_ptr to the created object. + +```cpp +std::unique_ptr text_to_string(const char* text, length_t size); +std::unique_ptr text_to_variable(const char* text, length_t size); +std::unique_ptr text_to_item(const char* text, length_t size); +std::unique_ptr text_to_list(const char* text, length_t size); +std::unique_ptr text_to_term(const char* text, length_t size); +std::unique_ptr text_to_rule(const char* text, length_t size); +``` + +### *_to_text Functions + +Convert objects to text. Returns a unique_ptr to a char array. + +```cpp +std::unique_ptr string_to_text(string_t* string, length_t size); +std::unique_ptr variable_to_text(variable_t* variable, length_t size); +std::unique_ptr item_to_text(item_t* item, length_t size); +std::unique_ptr list_to_text(list_t* list, length_t size); +std::unique_ptr term_to_text(term_t* term, length_t size); +std::unique_ptr rule_to_text(rule_t* rule, length_t size); +``` + +--- + +## Example + +```cpp +#include +#include +#include +#include +#include + +int main() { + // Create search engine + ds::search_t search(1000, 10000); + + // Add modus ponens rule + search.add("(`P -> `Q) `P `Q"); + + // Add axiom schemas + search.add("(`p -> (`q -> `p))"); + search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))"); + search.add("(((! `p) -> (! `q)) -> (`q -> `p))"); + + // Add premise + search.add("(! (! X))"); + + // Define target + auto target = ds::text_to_rule("X", 1000); + + // Search until target is found + while (true) { + bool found = false; + search.execute([&](ds::rule_t* candidate) { + if (candidate->data_size() == target->data_size() && + memcmp(candidate->head(), target->head(), candidate->data_size()) == 0) { + printf("Found: %s", ds::rule_to_text(candidate, 1000).get()); + found = true; + return true; + } + return false; + }); + if (found) break; + } + + return 0; +} +``` diff --git a/docs/api/python.md b/docs/api/python.md new file mode 100644 index 0000000..f88e30e --- /dev/null +++ b/docs/api/python.md @@ -0,0 +1,71 @@ +# Python API Reference + +This page documents the Python API for the `apyds` package. + +## Buffer Size Functions + +::: apyds.buffer_size + options: + show_root_heading: true + heading_level: 3 + +::: apyds.scoped_buffer_size + options: + show_root_heading: true + heading_level: 3 + +## String + +::: apyds.String + options: + show_root_heading: true + heading_level: 3 + members_order: source + +## Variable + +::: apyds.Variable + options: + show_root_heading: true + heading_level: 3 + members_order: source + +## Item + +::: apyds.Item + options: + show_root_heading: true + heading_level: 3 + members_order: source + +## List + +::: apyds.List + options: + show_root_heading: true + heading_level: 3 + members_order: source + +## Term + +::: apyds.Term + options: + show_root_heading: true + heading_level: 3 + members_order: source + +## Rule + +::: apyds.Rule + options: + show_root_heading: true + heading_level: 3 + members_order: source + +## Search + +::: apyds.Search + options: + show_root_heading: true + heading_level: 3 + members_order: source diff --git a/docs/api/typescript.md b/docs/api/typescript.md new file mode 100644 index 0000000..90855a1 --- /dev/null +++ b/docs/api/typescript.md @@ -0,0 +1,440 @@ +# TypeScript API Reference + +The TypeScript API is available through the `atsds` npm package. + +```typescript +import { + buffer_size, + string_t, + variable_t, + item_t, + list_t, + term_t, + rule_t, + search_t +} from "atsds"; +``` + +## buffer_size + +Gets the current buffer size, or sets a new buffer size and returns the previous value. + +```typescript +function buffer_size(size?: number): number; +``` + +**Parameters:** + +- `size` (optional): The new buffer size to set. If 0 or omitted, returns current size without modification. + +**Returns:** The previous buffer size value. + +**Example:** + +```typescript +const currentSize = buffer_size(); // Get current size +const oldSize = buffer_size(2048); // Set new size, returns old size +``` + +--- + +## string_t + +Wrapper class for deductive system strings. + +### Constructor + +```typescript +constructor(value: string | Buffer | string_t, size?: number) +``` + +**Parameters:** + +- `value`: Initial value (string, buffer, or another string_t) +- `size` (optional): Buffer capacity for internal storage + +### Methods + +#### toString() + +Convert the value to a string representation. + +```typescript +toString(): string +``` + +#### data() + +Get the binary representation of the value. + +```typescript +data(): Buffer +``` + +#### size() + +Get the size of the data in bytes. + +```typescript +size(): number +``` + +#### copy() + +Create a deep copy of this instance. + +```typescript +copy(): string_t +``` + +#### key() + +Get a key representation for equality comparison. + +```typescript +key(): string +``` + +**Example:** + +```typescript +const str1 = new string_t("hello"); +const str2 = new string_t(str1.data()); +console.log(str1.toString()); // "hello" +``` + +--- + +## variable_t + +Wrapper class for logical variables in the deductive system. + +### Constructor + +```typescript +constructor(value: string | Buffer | variable_t, size?: number) +``` + +**Parameters:** + +- `value`: Initial value (string starting with backtick, buffer, or another variable_t) +- `size` (optional): Buffer capacity for internal storage + +### Methods + +Inherits all methods from `string_t`, plus: + +#### name() + +Get the name of this variable (without the backtick prefix). + +```typescript +name(): string_t +``` + +**Example:** + +```typescript +const var1 = new variable_t("`X"); +console.log(var1.name().toString()); // "X" +console.log(var1.toString()); // "`X" +``` + +--- + +## item_t + +Wrapper class for items (constants/functors) in the deductive system. + +### Constructor + +```typescript +constructor(value: string | Buffer | item_t, size?: number) +``` + +### Methods + +Inherits all methods from `string_t`, plus: + +#### name() + +Get the name of this item. + +```typescript +name(): string_t +``` + +**Example:** + +```typescript +const item = new item_t("atom"); +console.log(item.name().toString()); // "atom" +``` + +--- + +## list_t + +Wrapper class for lists in the deductive system. + +### Constructor + +```typescript +constructor(value: string | Buffer | list_t, size?: number) +``` + +### Methods + +Inherits all methods from `string_t`, plus: + +#### length() + +Get the number of elements in the list. + +```typescript +length(): number +``` + +#### getitem() + +Get an element from the list by index. + +```typescript +getitem(index: number): term_t +``` + +**Example:** + +```typescript +const list = new list_t("(a b c)"); +console.log(list.length()); // 3 +console.log(list.getitem(0).toString()); // "a" +``` + +--- + +## term_t + +Wrapper class for logical terms in the deductive system. A term can be a variable, item, or list. + +### Constructor + +```typescript +constructor(value: string | Buffer | term_t, size?: number) +``` + +### Methods + +Inherits all methods from `string_t`, plus: + +#### term() + +Extracts the underlying term and returns it as its concrete type. + +```typescript +term(): variable_t | item_t | list_t +``` + +#### ground() + +Ground this term using a dictionary to substitute variables with values. + +```typescript +ground(other: term_t, scope?: string): term_t | null +``` + +**Parameters:** + +- `other`: A term representing a dictionary (list of pairs) +- `scope` (optional): Scope string for variable scoping + +**Returns:** The grounded term, or null if grounding fails. + +**Example:** + +```typescript +const a = new term_t("`a"); +const dict = new term_t("((`a b))"); +console.log(a.ground(dict)?.toString()); // "b" +``` + +#### rename() + +Rename all variables in this term by adding prefix and suffix. + +```typescript +rename(prefix_and_suffix: term_t): term_t | null +``` + +**Parameters:** + +- `prefix_and_suffix`: A term with format `((prefix) (suffix))` + +**Returns:** The renamed term, or null if renaming fails. + +**Example:** + +```typescript +const term = new term_t("`x"); +const spec = new term_t("((pre_) (_suf))"); +console.log(term.rename(spec)?.toString()); // "`pre_x_suf" +``` + +--- + +## rule_t + +Wrapper class for logical rules in the deductive system. + +### Constructor + +```typescript +constructor(value: string | Buffer | rule_t, size?: number) +``` + +### Methods + +Inherits all methods from `string_t`, plus: + +#### length() + +Get the number of premises in the rule. + +```typescript +length(): number +``` + +#### getitem() + +Get a premise term by index. + +```typescript +getitem(index: number): term_t +``` + +#### conclusion() + +Get the conclusion of the rule. + +```typescript +conclusion(): term_t +``` + +#### ground() + +Ground this rule using a dictionary. + +```typescript +ground(other: rule_t, scope?: string): rule_t | null +``` + +#### match() + +Match this rule with another rule using unification. + +```typescript +match(other: rule_t): rule_t | null +``` + +**Parameters:** + +- `other`: The rule to match against (must be a fact without premises) + +**Returns:** The matched rule, or null if matching fails. + +**Example:** + +```typescript +const mp = new rule_t("(`p -> `q)\n`p\n`q\n"); +const pq = new rule_t("((! (! `x)) -> `x)"); +console.log(mp.match(pq)?.toString()); +// "(! (! `x))\n----------\n`x\n" +``` + +#### rename() + +Rename all variables in this rule. + +```typescript +rename(prefix_and_suffix: rule_t): rule_t | null +``` + +--- + +## search_t + +Search engine for the deductive system. + +### Constructor + +```typescript +constructor(limit_size?: number, buffer_size?: number) +``` + +**Parameters:** + +- `limit_size` (optional): Size of the buffer for storing rules/facts (default: 1000) +- `buffer_size` (optional): Size of the buffer for internal operations (default: 10000) + +### Methods + +#### set_limit_size() + +Set the size of the buffer for storing final objects. + +```typescript +set_limit_size(limit_size: number): void +``` + +#### set_buffer_size() + +Set the buffer size for internal operations. + +```typescript +set_buffer_size(buffer_size: number): void +``` + +#### reset() + +Reset the search engine, clearing all rules and facts. + +```typescript +reset(): void +``` + +#### add() + +Add a rule or fact to the knowledge base. + +```typescript +add(text: string): boolean +``` + +**Returns:** True if successfully added, false otherwise. + +#### execute() + +Execute the search engine with a callback for each inferred rule. + +```typescript +execute(callback: (candidate: rule_t) => boolean): number +``` + +**Parameters:** + +- `callback`: Function called for each candidate rule. Return false to continue, true to stop. + +**Returns:** The number of rules processed. + +**Example:** + +```typescript +const search = new search_t(1000, 10000); +search.add("(`P -> `Q) `P `Q"); +search.add("(! (! X))"); + +search.execute((candidate) => { + console.log(candidate.toString()); + return false; // Continue searching +}); +``` diff --git a/docs/concepts/rules.md b/docs/concepts/rules.md new file mode 100644 index 0000000..cf7cd98 --- /dev/null +++ b/docs/concepts/rules.md @@ -0,0 +1,304 @@ +# Rules + +Rules are the core mechanism for representing logical inference in DS. This page explains how rules work and how to use them. + +## Rule Structure + +A rule consists of: + +- **Premises**: Zero or more conditions (above the line) +- **Conclusion**: The result when all premises are satisfied (below the line) + +### Text Representation + +Rules are written with premises and conclusion separated by dashes: + +``` +premise1 +premise2 +---------- +conclusion +``` + +A **fact** is a rule with no premises: + +``` +(parent john mary) +``` + +Or explicitly: + +``` +---------- +(parent john mary) +``` + +### Examples + +**Modus Ponens** (if P implies Q and P is true, then Q is true): + +``` +(`P -> `Q) +`P +---------- +`Q +``` + +**Family Relationship** (if X is the father of Y, then X is a parent of Y): + +``` +(father `X `Y) +---------- +(parent `X `Y) +``` + +## Creating Rules + +=== "Python" + + ```python + import apyds + + # Create a fact + fact = apyds.Rule("(parent john mary)") + + # Create a rule with premises + # Using explicit separator + rule = apyds.Rule("(father `X `Y)\n----------\n(parent `X `Y)\n") + + # Access rule components + print(f"Number of premises: {len(rule)}") # 1 + print(f"First premise: {rule[0]}") # (father `X `Y) + print(f"Conclusion: {rule.conclusion}") # (parent `X `Y) + ``` + +=== "TypeScript" + + ```typescript + import { rule_t } from "atsds"; + + // Create a fact + const fact = new rule_t("(parent john mary)"); + + // Create a rule with premises + const rule = new rule_t("(father `X `Y)\n----------\n(parent `X `Y)\n"); + + // Access rule components + console.log(`Number of premises: ${rule.length()}`); // 1 + console.log(`First premise: ${rule.getitem(0).toString()}`); // (father `X `Y) + console.log(`Conclusion: ${rule.conclusion().toString()}`); // (parent `X `Y) + ``` + +=== "C++" + + ```cpp + #include + #include + #include + + int main() { + // Create a fact + auto fact = ds::text_to_rule("(parent john mary)", 1000); + + // Create a rule with premises + auto rule = ds::text_to_rule("(father `X `Y)\n----------\n(parent `X `Y)\n", 1000); + + // Access rule components + std::cout << "Number of premises: " << rule->premises_count() << std::endl; + std::cout << "Conclusion: " << ds::term_to_text(rule->conclusion(), 1000).get() << std::endl; + + return 0; + } + ``` + +## Rule Operations + +### Grounding + +Grounding substitutes variables in a rule with values from a dictionary. + +=== "Python" + + ```python + import apyds + + # Create a rule with variables + rule = apyds.Rule("`a") + + # Create a dictionary + dictionary = apyds.Rule("((`a b))") + + # Ground the rule + result = rule.ground(dictionary) + print(result) # ----\nb\n + ``` + +=== "TypeScript" + + ```typescript + import { rule_t } from "atsds"; + + // Create a rule with variables + const rule = new rule_t("`a"); + + // Create a dictionary + const dictionary = new rule_t("((`a b))"); + + // Ground the rule + const result = rule.ground(dictionary); + console.log(result?.toString()); // ----\nb\n + ``` + +### Matching + +Matching unifies the first premise of a rule with a fact, producing a new rule with one fewer premise. + +=== "Python" + + ```python + import apyds + + # Modus ponens rule: if (P -> Q) and P then Q + mp = apyds.Rule("(`p -> `q)\n`p\n`q\n") + + # A fact: double negation elimination axiom + axiom = apyds.Rule("((! (! `x)) -> `x)") + + # Match: apply axiom to modus ponens + result = mp @ axiom # Uses @ operator + print(result) + # Output: + # (! (! `x)) + # ---------- + # `x + ``` + +=== "TypeScript" + + ```typescript + import { rule_t } from "atsds"; + + // Modus ponens rule + const mp = new rule_t("(`p -> `q)\n`p\n`q\n"); + + // Double negation elimination axiom + const axiom = new rule_t("((! (! `x)) -> `x)"); + + // Match + const result = mp.match(axiom); + console.log(result?.toString()); + // (! (! `x)) + // ---------- + // `x + ``` + +### Renaming + +Renaming adds prefixes and/or suffixes to all variables in a rule. + +=== "Python" + + ```python + import apyds + + # Create a rule + rule = apyds.Rule("`x") + + # Rename with prefix and suffix + spec = apyds.Rule("((pre_) (_suf))") + result = rule.rename(spec) + print(result) # ----\n`pre_x_suf\n + ``` + +=== "TypeScript" + + ```typescript + import { rule_t } from "atsds"; + + // Create a rule + const rule = new rule_t("`x"); + + // Rename with prefix and suffix + const spec = new rule_t("((pre_) (_suf))"); + const result = rule.rename(spec); + console.log(result?.toString()); // ----\n`pre_x_suf\n + ``` + +## Rule Comparison + +Rules can be compared for equality. Two rules are equal if they have the same binary representation. + +=== "Python" + + ```python + import apyds + + rule1 = apyds.Rule("(a b c)") + rule2 = apyds.Rule("(a b c)") + rule3 = apyds.Rule("(a b d)") + + print(rule1 == rule2) # True + print(rule1 == rule3) # False + ``` + +=== "TypeScript" + + ```typescript + import { rule_t } from "atsds"; + + const rule1 = new rule_t("(a b c)"); + const rule2 = new rule_t("(a b c)"); + const rule3 = new rule_t("(a b d)"); + + console.log(rule1.key() === rule2.key()); // true + console.log(rule1.key() === rule3.key()); // false + ``` + +## Logical Systems + +DS can encode various logical systems using rules: + +### Propositional Logic + +```python +import apyds + +search = apyds.Search(1000, 10000) + +# Modus ponens: P -> Q, P |- Q +search.add("(`P -> `Q) `P `Q") + +# Axiom schemas for propositional logic: +# 1. p -> (q -> p) +search.add("(`p -> (`q -> `p))") + +# 2. (p -> (q -> r)) -> ((p -> q) -> (p -> r)) +search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))") + +# 3. (!p -> !q) -> (q -> p) +search.add("(((! `p) -> (! `q)) -> (`q -> `p))") +``` + +### Custom Domains + +You can define rules for any domain: + +```python +import apyds + +search = apyds.Search(1000, 10000) + +# Family relationships +search.add("(father `X `Y)\n----------\n(parent `X `Y)\n") +search.add("(mother `X `Y)\n----------\n(parent `X `Y)\n") +search.add("(parent `X `Y) (parent `Y `Z)\n----------\n(grandparent `X `Z)\n") + +# Facts +search.add("(father john mary)") +search.add("(mother mary alice)") +``` + +## See Also + +- [Terms](terms.md) - Building blocks for rules +- [Search Engine](search.md) - Performing inference with rules diff --git a/docs/concepts/search.md b/docs/concepts/search.md new file mode 100644 index 0000000..ea8f399 --- /dev/null +++ b/docs/concepts/search.md @@ -0,0 +1,305 @@ +# Search Engine + +The search engine is the core inference mechanism in DS. It manages a knowledge base of rules and facts, and performs logical inference by matching rules with facts. + +## Overview + +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 + +## Creating a Search Engine + +=== "Python" + + ```python + import apyds + + # Create with default sizes + search = apyds.Search() + + # Create with custom sizes + search = apyds.Search(limit_size=2000, buffer_size=20000) + ``` + +=== "TypeScript" + + ```typescript + import { search_t } from "atsds"; + + // Create with default sizes + const search = new search_t(); + + // Create with custom sizes + const search2 = new search_t(2000, 20000); + ``` + +=== "C++" + + ```cpp + #include + + // Create search engine + ds::search_t search(1000, 10000); + ``` + +### 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) + +## Adding Rules and Facts + +Use the `add()` method to add rules and facts to the knowledge base. + +=== "Python" + + ```python + import apyds + + search = apyds.Search() + + # Add a fact + search.add("(parent john mary)") + + # 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" + + ```typescript + import { search_t } from "atsds"; + + const search = new search_t(); + + // Add a fact + search.add("(parent john mary)"); + + // Add a rule with premises + search.add("(father `X `Y)\n----------\n(parent `X `Y)\n"); + ``` + +=== "C++" + + ```cpp + ds::search_t search(1000, 10000); + + // Add a fact + search.add("(parent john mary)"); + + // Add a rule + search.add("(father `X `Y)\n----------\n(parent `X `Y)\n"); + ``` + +## Executing Search + +The `execute()` method performs one round of inference. It matches all rules against all facts and generates new conclusions. + +=== "Python" + + ```python + import apyds + + search = apyds.Search() + search.add("(father `X `Y)\n----------\n(parent `X `Y)\n") + search.add("(father john mary)") + + def callback(rule): + print(f"Found: {rule}") + return False # Continue searching + + # Execute one round + count = search.execute(callback) + print(f"Generated {count} new facts") + ``` + +=== "TypeScript" + + ```typescript + import { search_t } from "atsds"; + + const search = new search_t(); + search.add("(father `X `Y)\n----------\n(parent `X `Y)\n"); + search.add("(father john mary)"); + + const count = search.execute((rule) => { + console.log(`Found: ${rule.toString()}`); + return false; // Continue searching + }); + + console.log(`Generated ${count} new facts`); + ``` + +=== "C++" + + ```cpp + ds::search_t search(1000, 10000); + search.add("(father `X `Y)\n----------\n(parent `X `Y)\n"); + search.add("(father john mary)"); + + auto count = search.execute([](ds::rule_t* rule) { + printf("Found: %s\n", ds::rule_to_text(rule, 1000).get()); + return false; // Continue searching + }); + + printf("Generated %lu new facts\n", count); + ``` + +### Callback Function + +The callback receives each newly inferred rule and should return: + +- `False` (Python) / `false` (TypeScript/C++): Continue searching +- `True` (Python) / `true` (TypeScript/C++): Stop searching + +## Searching for a Target + +To search until a specific target is found: + +=== "Python" + + ```python + import apyds + + search = apyds.Search(1000, 10000) + + # Set up propositional logic + search.add("(`P -> `Q) `P `Q") # Modus ponens + search.add("(`p -> (`q -> `p))") # Axiom 1 + search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))") # Axiom 2 + search.add("(((! `p) -> (! `q)) -> (`q -> `p))") # Axiom 3 + search.add("(! (! X))") # Premise + + target = apyds.Rule("X") + + while True: + found = False + def check(candidate): + global found + if candidate == target: + print(f"Found: {candidate}") + found = True + return True + return False + search.execute(check) + if found: + break + ``` + +=== "TypeScript" + + ```typescript + import { rule_t, search_t } from "atsds"; + + const search = new search_t(1000, 10000); + + // Set up propositional logic + search.add("(`P -> `Q) `P `Q"); + search.add("(`p -> (`q -> `p))"); + search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))"); + search.add("(((! `p) -> (! `q)) -> (`q -> `p))"); + search.add("(! (! X))"); + + const target = new rule_t("X"); + + while (true) { + let found = false; + search.execute((candidate) => { + if (candidate.key() === target.key()) { + console.log("Found:", candidate.toString()); + found = true; + return true; + } + return false; + }); + if (found) break; + } + ``` + +## Configuration Methods + +### Set Limit Size + +Controls the maximum size for each stored rule/fact: + +=== "Python" + + ```python + search.set_limit_size(2000) + ``` + +=== "TypeScript" + + ```typescript + search.set_limit_size(2000); + ``` + +=== "C++" + + ```cpp + search.set_limit_size(2000); + ``` + +### Set Buffer Size + +Controls the internal buffer size for operations: + +=== "Python" + + ```python + search.set_buffer_size(20000) + ``` + +=== "TypeScript" + + ```typescript + search.set_buffer_size(20000); + ``` + +=== "C++" + + ```cpp + search.set_buffer_size(20000); + ``` + +### Reset + +Clears all rules and facts: + +=== "Python" + + ```python + search.reset() + ``` + +=== "TypeScript" + + ```typescript + search.reset(); + ``` + +=== "C++" + + ```cpp + search.reset(); + ``` + +## Performance Considerations + +1. **Buffer Size**: Larger buffers allow more complex intermediate results but use more memory +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 + +## See Also + +- [Terms](terms.md) - Building blocks for the search +- [Rules](rules.md) - How rules are structured and matched diff --git a/docs/concepts/terms.md b/docs/concepts/terms.md new file mode 100644 index 0000000..352b1a5 --- /dev/null +++ b/docs/concepts/terms.md @@ -0,0 +1,238 @@ +# Terms + +Terms are the fundamental building blocks of the deductive system. This page explains the different types of terms and how to work with them. + +## Term Types + +The deductive system supports three basic types of terms: + +### Variables + +Variables are placeholders that can be unified with other terms during inference. They are prefixed with a backtick (`` ` ``). + +``` +`X +`variable_name +`P +`Q +``` + +Variables are used in rules to represent any term that can match during unification. + +### Items + +Items represent constants or functors. They are atomic values without any special prefix. + +``` +hello +atom +father +! +-> +``` + +Items can represent: + +- **Constants**: Atomic values like `john`, `mary`, `42` +- **Functors**: Symbols that combine other terms, like `father`, `->`, `!` + +### Lists + +Lists are ordered sequences of terms enclosed in parentheses. They can contain any combination of variables, items, and nested lists. + +``` +(a b c) +(father john mary) +(-> P Q) +(! (! X)) +``` + +Lists are the primary way to build complex structures in the deductive system. + +## Working with Terms + +=== "Python" + + ```python + import apyds + + # Create a variable + var = apyds.Variable("`X") + print(f"Variable name: {var.name}") # X + + # Create an item + item = apyds.Item("hello") + print(f"Item name: {item.name}") # hello + + # Create a list + lst = apyds.List("(a b c)") + print(f"List length: {len(lst)}") # 3 + print(f"First element: {lst[0]}") # a + + # Create a generic term + term = apyds.Term("(f `x)") + # Access the underlying type + inner = term.term # Returns a List + ``` + +=== "TypeScript" + + ```typescript + import { variable_t, item_t, list_t, term_t } from "atsds"; + + // Create a variable + const var1 = new variable_t("`X"); + console.log(`Variable name: ${var1.name().toString()}`); // X + + // Create an item + const item = new item_t("hello"); + console.log(`Item name: ${item.name().toString()}`); // hello + + // Create a list + const lst = new list_t("(a b c)"); + console.log(`List length: ${lst.length()}`); // 3 + console.log(`First element: ${lst.getitem(0).toString()}`); // a + + // Create a generic term + const term = new term_t("(f `x)"); + // Access the underlying type + const inner = term.term(); // Returns a list_t + ``` + +=== "C++" + + ```cpp + #include + #include + #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); + + return 0; + } + ``` + +## Grounding + +Grounding substitutes variables in a term with values from a dictionary. The dictionary is a list of key-value pairs where each key is a variable and each value is its substitution. + +=== "Python" + + ```python + import apyds + + # Create a term with a variable + term = apyds.Term("`a") + + # Create a dictionary for substitution + # Format: ((variable value) ...) + dictionary = apyds.Term("((`a b))") + + # Ground the term + result = term.ground(dictionary) + print(result) # b + ``` + +=== "TypeScript" + + ```typescript + import { term_t } from "atsds"; + + // Create a term with a variable + const term = new term_t("`a"); + + // Create a dictionary for substitution + const dictionary = new term_t("((`a b))"); + + // Ground the term + const result = term.ground(dictionary); + console.log(result?.toString()); // b + ``` + +## Renaming + +Renaming adds prefixes and/or suffixes to all variables in a term. This is useful for avoiding variable name collisions during unification. + +=== "Python" + + ```python + import apyds + + # Create a term with a variable + term = apyds.Term("`x") + + # Create prefix and suffix specification + # Format: ((prefix) (suffix)) + spec = apyds.Term("((pre_) (_suf))") + + # Rename the term + result = term.rename(spec) + print(result) # `pre_x_suf + ``` + +=== "TypeScript" + + ```typescript + import { term_t } from "atsds"; + + // Create a term with a variable + const term = new term_t("`x"); + + // Create prefix and suffix specification + const spec = new term_t("((pre_) (_suf))"); + + // Rename the term + const result = term.rename(spec); + console.log(result?.toString()); // `pre_x_suf + ``` + +## Buffer Size + +Operations like grounding and renaming require buffer space for intermediate results. You can control this using buffer size functions. + +=== "Python" + + ```python + import apyds + + # Get current buffer size + current = apyds.buffer_size() + + # Set new buffer size (returns previous value) + old = apyds.buffer_size(4096) + + # Use context manager for temporary change + with apyds.scoped_buffer_size(8192): + # Operations here use buffer size of 8192 + pass + # Buffer size restored to previous value + ``` + +=== "TypeScript" + + ```typescript + import { buffer_size } from "atsds"; + + // Get current buffer size + const current = buffer_size(); + + // Set new buffer size (returns previous value) + const old = buffer_size(4096); + ``` + +## See Also + +- [Rules](rules.md) - How to create and work with inference rules +- [Search Engine](search.md) - Performing logical inference diff --git a/docs/examples/index.md b/docs/examples/index.md new file mode 100644 index 0000000..dbd4915 --- /dev/null +++ b/docs/examples/index.md @@ -0,0 +1,166 @@ +# Examples + +This section contains examples demonstrating the DS deductive system in various languages. + +## Propositional Logic Inference + +The classic example demonstrates double negation elimination using propositional logic axioms: + +- **Modus Ponens**: If P implies Q, and P is true, then Q is true +- **Axiom 1**: P → (Q → P) +- **Axiom 2**: (P → (Q → R)) → ((P → Q) → (P → R)) +- **Axiom 3**: (¬P → ¬Q) → (Q → P) + +Given the premise !!X (double negation of X), we can derive X. + +=== "Python" + + ```python + import apyds + + # Create a search engine + search = apyds.Search(1000, 10000) + + # Modus ponens: P -> Q, P |- Q + search.add("(`P -> `Q) `P `Q") + # Axiom schema 1: p -> (q -> p) + search.add("(`p -> (`q -> `p))") + # Axiom schema 2: (p -> (q -> r)) -> ((p -> q) -> (p -> r)) + search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))") + # Axiom schema 3: (!p -> !q) -> (q -> p) + search.add("(((! `p) -> (! `q)) -> (`q -> `p))") + + # Premise: !!X + search.add("(! (! X))") + + # Target: X (double negation elimination) + target = apyds.Rule("X") + + # Execute search until target is found + while True: + found = False + def callback(candidate): + global found + if candidate == target: + print("Found:", candidate) + found = True + return True # Stop search + return False # Continue searching + search.execute(callback) + if found: + break + ``` + +=== "TypeScript" + + ```typescript + import { rule_t, search_t } from "atsds"; + + // Create a search engine + const search = new search_t(1000, 10000); + + // Modus ponens: P -> Q, P |- Q + search.add("(`P -> `Q) `P `Q"); + // Axiom schema 1: p -> (q -> p) + search.add("(`p -> (`q -> `p))"); + // Axiom schema 2: (p -> (q -> r)) -> ((p -> q) -> (p -> r)) + search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))"); + // Axiom schema 3: (!p -> !q) -> (q -> p) + search.add("(((! `p) -> (! `q)) -> (`q -> `p))"); + + // Premise: !!X + search.add("(! (! X))"); + + // Target: X (double negation elimination) + const target = new rule_t("X"); + + // Execute search until target is found + while (true) { + let found = false; + search.execute((candidate) => { + if (candidate.key() === target.key()) { + console.log("Found:", candidate.toString()); + found = true; + return true; // Stop search + } + return false; // Continue searching + }); + if (found) break; + } + ``` + +=== "C++" + + ```cpp + #include + #include + #include + #include + #include + + int main() { + ds::search_t search(1000, 10000); + + // Modus ponens: P -> Q, P |- Q + search.add("(`P -> `Q) `P `Q"); + // Axiom schema 1: p -> (q -> p) + search.add("(`p -> (`q -> `p))"); + // Axiom schema 2: (p -> (q -> r)) -> ((p -> q) -> (p -> r)) + search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))"); + // Axiom schema 3: (!p -> !q) -> (q -> p) + search.add("(((! `p) -> (! `q)) -> (`q -> `p))"); + + // Premise: !!X + search.add("(! (! X))"); + + // Target: X (double negation elimination) + auto target = ds::text_to_rule("X", 1000); + + // Execute search until target is found + while (true) { + bool found = false; + search.execute([&](ds::rule_t* candidate) { + if (candidate->data_size() == target->data_size() && + memcmp(candidate->head(), target->head(), candidate->data_size()) == 0) { + printf("Found: %s", ds::rule_to_text(candidate, 1000).get()); + found = true; + return true; // Stop search + } + return false; // Continue searching + }); + if (found) break; + } + + return 0; + } + ``` + +## Running the Examples + +Example files are provided in the repository under `examples/`: + +- `examples/main.py` - Python example +- `examples/main.mjs` - TypeScript/JavaScript example +- `examples/main.cc` - C++ example + +### Python + +```bash +pip install apyds +python examples/main.py +``` + +### TypeScript/JavaScript + +```bash +npm install atsds +node examples/main.mjs +``` + +### C++ + +```bash +cmake -B build +cmake --build build +./build/main +``` diff --git a/docs/getting-started/installation.md b/docs/getting-started/installation.md new file mode 100644 index 0000000..4eedd9c --- /dev/null +++ b/docs/getting-started/installation.md @@ -0,0 +1,136 @@ +# Installation + +DS can be installed for Python, TypeScript/JavaScript, or used directly as a C++ library. + +## Python + +The Python package `apyds` wraps the C++ core via pybind11. + +```bash +pip install apyds +``` + +**Requirements:** + +- Python 3.10-3.14 +- Pre-built wheels are available for common platforms + +### Development Installation + +To install from source with development dependencies: + +```bash +git clone https://github.com/USTC-KnowledgeComputingLab/ds.git +cd ds +pip install -e ".[dev]" +``` + +## TypeScript/JavaScript + +The TypeScript/JavaScript package `atsds` wraps the C++ core via WebAssembly. + +```bash +npm install atsds +``` + +The package includes: + +- WebAssembly binaries (`.wasm`) +- TypeScript type definitions (`.d.mts`) +- ES module support + +### Requirements + +- Node.js 16+ or a modern browser with WebAssembly support + +## C++ + +The C++ library is the core implementation. Both Python and TypeScript bindings are built on top of it. + +### Prerequisites + +- C++20 compatible compiler (GCC 10+, Clang 10+, MSVC 2019+) +- CMake 3.30+ + +### Building from Source + +```bash +git clone https://github.com/USTC-KnowledgeComputingLab/ds.git +cd ds +cmake -B build +cmake --build build +``` + +### Using in Your Project + +Include the headers from `include/ds/` in your C++ project: + +```cpp +#include +#include +``` + +Link against the `ds` static library produced by the build. + +## Building All Components + +To build all language bindings from source: + +### TypeScript/JavaScript (requires Emscripten) + +```bash +# Install Emscripten SDK first +# https://emscripten.org/docs/getting_started/downloads.html + +npm install +npm run build +``` + +### Python + +```bash +pip install -e ".[dev]" +``` + +### C++ + +```bash +cmake -B build +cmake --build build +``` + +## Verifying Installation + +=== "Python" + + ```python + import apyds + print(apyds.__version__) + + # Create a simple term + term = apyds.Term("(hello world)") + print(term) + ``` + +=== "TypeScript" + + ```typescript + import { term_t } from "atsds"; + + const term = new term_t("(hello world)"); + console.log(term.toString()); + ``` + +=== "C++" + + ```cpp + #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; + } + ``` diff --git a/docs/getting-started/quickstart.md b/docs/getting-started/quickstart.md new file mode 100644 index 0000000..a0d624e --- /dev/null +++ b/docs/getting-started/quickstart.md @@ -0,0 +1,248 @@ +# Quick Start + +This guide will help you get started with DS in your preferred language. + +## Creating Terms + +Terms are the basic building blocks of the deductive system. A term can be: + +- **Variable**: Prefixed with backtick, e.g., `` `X``, `` `P`` +- **Item**: Constants or functors, e.g., `a`, `father`, `!` +- **List**: Ordered sequences in parentheses, e.g., `(a b c)` + +=== "Python" + + ```python + import apyds + + # Create different types of terms + var = apyds.Variable("`X") + item = apyds.Item("hello") + lst = apyds.List("(a b c)") + term = apyds.Term("(f `x a)") + + print(f"Variable: {var}") # `X + print(f"Item: {item}") # hello + print(f"List: {lst}") # (a b c) + print(f"Term: {term}") # (f `x a) + ``` + +=== "TypeScript" + + ```typescript + import { variable_t, item_t, list_t, term_t } from "atsds"; + + // Create different types of terms + const var1 = 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 a)"); + + console.log(`Variable: ${var1.toString()}`); // `X + console.log(`Item: ${item.toString()}`); // hello + console.log(`List: ${lst.toString()}`); // (a b c) + console.log(`Term: ${term.toString()}`); // (f `x a) + ``` + +=== "C++" + + ```cpp + #include + #include + #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; + } + ``` + +## Creating Rules + +Rules represent logical inference steps. A rule has premises (conditions) and a conclusion. + +=== "Python" + + ```python + import apyds + + # A fact (rule with no premises) + fact = apyds.Rule("(parent john mary)") + print(f"Fact: {fact}") + + # A rule with premises + # Format: premise1\npremise2\nconclusion\n + rule = apyds.Rule("(father `X `Y)\n----------\n(parent `X `Y)\n") + print(f"Rule premises: {len(rule)}") + print(f"Rule conclusion: {rule.conclusion}") + ``` + +=== "TypeScript" + + ```typescript + import { rule_t } from "atsds"; + + // A fact (rule with no premises) + const fact = new rule_t("(parent john mary)"); + console.log(`Fact: ${fact.toString()}`); + + // A rule with premises + const rule = new rule_t("(father `X `Y)\n----------\n(parent `X `Y)\n"); + console.log(`Rule premises: ${rule.length()}`); + console.log(`Rule conclusion: ${rule.conclusion().toString()}`); + ``` + +=== "C++" + + ```cpp + #include + #include + #include + + int main() { + 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; + return 0; + } + ``` + +## Using the Search Engine + +The search engine performs logical inference by matching rules with facts. + +=== "Python" + + ```python + import apyds + + # Create search engine + search = apyds.Search(1000, 10000) + + # Add modus ponens: P -> Q, P |- Q + search.add("(`P -> `Q) `P `Q") + + # Add axiom schemas + search.add("(`p -> (`q -> `p))") # Axiom 1 + search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))") # Axiom 2 + search.add("(((! `p) -> (! `q)) -> (`q -> `p))") # Axiom 3 + + # Add premise: !!X (double negation) + search.add("(! (! X))") + + # Define target: X + target = apyds.Rule("X") + + # Execute search + while True: + found = False + def callback(candidate): + global found + if candidate == target: + print(f"Found: {candidate}") + found = True + return True + return False + search.execute(callback) + if found: + break + ``` + +=== "TypeScript" + + ```typescript + import { rule_t, search_t } from "atsds"; + + // Create search engine + const search = new search_t(1000, 10000); + + // Add modus ponens: P -> Q, P |- Q + search.add("(`P -> `Q) `P `Q"); + + // Add axiom schemas + search.add("(`p -> (`q -> `p))"); // Axiom 1 + search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))"); // Axiom 2 + search.add("(((! `p) -> (! `q)) -> (`q -> `p))"); // Axiom 3 + + // Add premise: !!X (double negation) + search.add("(! (! X))"); + + // Define target: X + const target = new rule_t("X"); + + // Execute search + while (true) { + let found = false; + search.execute((candidate) => { + if (candidate.key() === target.key()) { + console.log("Found:", candidate.toString()); + found = true; + return true; + } + return false; + }); + if (found) break; + } + ``` + +=== "C++" + + ```cpp + #include + #include + #include + #include + #include + + int main() { + ds::search_t search(1000, 10000); + + // Add modus ponens: P -> Q, P |- Q + search.add("(`P -> `Q) `P `Q"); + + // Add axiom schemas + search.add("(`p -> (`q -> `p))"); + search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))"); + search.add("(((! `p) -> (! `q)) -> (`q -> `p))"); + + // Add premise: !!X (double negation) + search.add("(! (! X))"); + + // Define target: X + auto target = ds::text_to_rule("X", 1000); + + // Execute search + while (true) { + bool found = false; + search.execute([&](ds::rule_t* candidate) { + if (candidate->data_size() == target->data_size() && + memcmp(candidate->head(), target->head(), candidate->data_size()) == 0) { + printf("Found: %s", ds::rule_to_text(candidate, 1000).get()); + found = true; + return true; + } + return false; + }); + if (found) break; + } + + return 0; + } + ``` + +## Next Steps + +- Learn more about [Terms](../concepts/terms.md) +- Understand [Rules](../concepts/rules.md) +- Explore the [Search Engine](../concepts/search.md) +- Check the [API Reference](../api/python.md) diff --git a/docs/index.md b/docs/index.md new file mode 100644 index 0000000..446947a --- /dev/null +++ b/docs/index.md @@ -0,0 +1,80 @@ +# DS - A Deductive System + +A deductive system for logical inference, implemented in C++. The library provides bindings for Python (via pybind11) and TypeScript/JavaScript (via Emscripten/WebAssembly). + +## Features + +- **Multi-Language Support**: Use the same deductive system in C++, Python, or TypeScript/JavaScript +- **Logical Terms**: Work with variables, items (constants/functors), and lists +- **Rule-Based Inference**: Define rules and facts, perform logical deduction +- **Unification and Matching**: Unify terms and match rules +- **Search Engine**: Built-in search mechanism for iterative inference +- **WebAssembly**: Run inference in the browser or Node.js environments +- **Type-Safe**: Strong typing support in TypeScript and Python + +## Architecture + +``` +┌─────────────────────────────────────────────────────────────┐ +│ Application Layer │ +├──────────────────┬──────────────────┬───────────────────────┤ +│ Python (apyds) │ TypeScript (atsds)│ C++ Direct │ +│ via pybind11 │ via WebAssembly │ │ +├──────────────────┴──────────────────┴───────────────────────┤ +│ C++ Core Library │ +│ (include/ds/, src/) │ +└─────────────────────────────────────────────────────────────┘ +``` + +## 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"; + + const search = new search_t(1000, 10000); + search.add("(`P -> `Q) `P `Q"); // Modus ponens + search.add("(! (! X))"); // Premise: !!X + + const target = new rule_t("X"); + // ... execute search + ``` + +=== "C++" + + ```cpp + #include + #include + + ds::search_t search(1000, 10000); + search.add("(`P -> `Q) `P `Q"); // Modus ponens + search.add("(! (! X))"); // Premise: !!X + + auto target = ds::text_to_rule("X", 1000); + // ... execute search + ``` + +## License + +This project is licensed under the GNU General Public License v3.0 or later. diff --git a/mkdocs.yml b/mkdocs.yml new file mode 100644 index 0000000..432f4ee --- /dev/null +++ b/mkdocs.yml @@ -0,0 +1,84 @@ +site_name: DS - A Deductive System +site_description: A deductive system for logical inference, implemented in C++ with bindings for Python and TypeScript/JavaScript +site_author: Hao Zhang +repo_url: https://github.com/USTC-KnowledgeComputingLab/ds +repo_name: USTC-KnowledgeComputingLab/ds + +theme: + name: material + features: + - content.code.copy + - content.tabs.link + - navigation.tabs + - navigation.sections + - navigation.expand + - navigation.top + - search.suggest + - search.highlight + palette: + - scheme: default + primary: indigo + accent: indigo + toggle: + icon: material/brightness-7 + name: Switch to dark mode + - scheme: slate + primary: indigo + accent: indigo + toggle: + icon: material/brightness-4 + name: Switch to light mode + +nav: + - Home: index.md + - Getting Started: + - Installation: getting-started/installation.md + - Quick Start: getting-started/quickstart.md + - Core Concepts: + - Terms: concepts/terms.md + - Rules: concepts/rules.md + - Search Engine: concepts/search.md + - API Reference: + - Python API: api/python.md + - TypeScript API: api/typescript.md + - C++ API: api/cpp.md + - Examples: + - examples/index.md + +plugins: + - search + - mkdocstrings: + default_handler: python + handlers: + python: + options: + show_source: false + show_root_heading: true + show_root_full_path: false + heading_level: 2 + members_order: source + docstring_style: google + merge_init_into_class: true + show_signature_annotations: true + +markdown_extensions: + - pymdownx.highlight: + anchor_linenums: true + line_spans: __span + pygments_lang_class: true + - pymdownx.inlinehilite + - pymdownx.snippets + - pymdownx.superfences + - pymdownx.tabbed: + alternate_style: true + - admonition + - pymdownx.details + - attr_list + - md_in_html + - toc: + permalink: true + +extra: + social: + - icon: fontawesome/brands/github + link: https://github.com/USTC-KnowledgeComputingLab/ds diff --git a/pyproject.toml b/pyproject.toml index 179b9f1..0e9fa81 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -35,6 +35,11 @@ dev = [ "pytest~=9.0.1", "pytest-cov~=7.0.0", ] +docs = [ + "mkdocs~=1.6.1", + "mkdocs-material~=9.6.14", + "mkdocstrings[python]~=0.29.1", +] [tool.ruff] line-length = 120 From 4d11cc0fc51cf72fe451fdf41311ae4c678889a2 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 25 Nov 2025 12:43:23 +0000 Subject: [PATCH 3/7] Fix Python examples to use nonlocal instead of global Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com> --- docs/concepts/search.md | 2 +- docs/examples/index.md | 2 +- docs/getting-started/quickstart.md | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/concepts/search.md b/docs/concepts/search.md index ea8f399..75fd747 100644 --- a/docs/concepts/search.md +++ b/docs/concepts/search.md @@ -183,7 +183,7 @@ To search until a specific target is found: while True: found = False def check(candidate): - global found + nonlocal found if candidate == target: print(f"Found: {candidate}") found = True diff --git a/docs/examples/index.md b/docs/examples/index.md index dbd4915..829acaf 100644 --- a/docs/examples/index.md +++ b/docs/examples/index.md @@ -40,7 +40,7 @@ Given the premise !!X (double negation of X), we can derive X. while True: found = False def callback(candidate): - global found + nonlocal found if candidate == target: print("Found:", candidate) found = True diff --git a/docs/getting-started/quickstart.md b/docs/getting-started/quickstart.md index a0d624e..3f612c1 100644 --- a/docs/getting-started/quickstart.md +++ b/docs/getting-started/quickstart.md @@ -147,7 +147,7 @@ The search engine performs logical inference by matching rules with facts. while True: found = False def callback(candidate): - global found + nonlocal found if candidate == target: print(f"Found: {candidate}") found = True From da6b2cec55073e3cf229ae6e99b41ef2e0c67078 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 25 Nov 2025 13:29:57 +0000 Subject: [PATCH 4/7] Address PR feedback: fix architecture, reorder sections, update Node.js version, remove ?. usage Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com> --- docs/api/cpp.md | 2 +- docs/api/typescript.md | 19 ++++++--- docs/concepts/rules.md | 62 ++++++---------------------- docs/concepts/terms.md | 8 +++- docs/getting-started/installation.md | 58 +++++++++++++------------- docs/index.md | 18 ++++---- mkdocs.yml | 2 +- 7 files changed, 72 insertions(+), 97 deletions(-) diff --git a/docs/api/cpp.md b/docs/api/cpp.md index 688d070..c1925e9 100644 --- a/docs/api/cpp.md +++ b/docs/api/cpp.md @@ -1,6 +1,6 @@ # C++ API Reference -The C++ API is the core implementation. Both Python and TypeScript bindings are built on top of it. +This page documents the C++ API for the DS library. The documentation is generated from the C++ source code. All classes and functions are in the `ds` namespace. diff --git a/docs/api/typescript.md b/docs/api/typescript.md index 90855a1..e1a74ff 100644 --- a/docs/api/typescript.md +++ b/docs/api/typescript.md @@ -1,6 +1,6 @@ # TypeScript API Reference -The TypeScript API is available through the `atsds` npm package. +This page documents the TypeScript API for the `atsds` package. The documentation is generated from the TypeScript source code. ```typescript import { @@ -255,7 +255,10 @@ ground(other: term_t, scope?: string): term_t | null ```typescript const a = new term_t("`a"); const dict = new term_t("((`a b))"); -console.log(a.ground(dict)?.toString()); // "b" +const result = a.ground(dict); +if (result !== null) { + console.log(result.toString()); // "b" +} ``` #### rename() @@ -277,7 +280,10 @@ rename(prefix_and_suffix: term_t): term_t | null ```typescript const term = new term_t("`x"); const spec = new term_t("((pre_) (_suf))"); -console.log(term.rename(spec)?.toString()); // "`pre_x_suf" +const result = term.rename(spec); +if (result !== null) { + console.log(result.toString()); // "`pre_x_suf" +} ``` --- @@ -347,8 +353,11 @@ match(other: rule_t): rule_t | null ```typescript const mp = new rule_t("(`p -> `q)\n`p\n`q\n"); const pq = new rule_t("((! (! `x)) -> `x)"); -console.log(mp.match(pq)?.toString()); -// "(! (! `x))\n----------\n`x\n" +const result = mp.match(pq); +if (result !== null) { + console.log(result.toString()); + // "(! (! `x))\n----------\n`x\n" +} ``` #### rename() diff --git a/docs/concepts/rules.md b/docs/concepts/rules.md index cf7cd98..4ab0784 100644 --- a/docs/concepts/rules.md +++ b/docs/concepts/rules.md @@ -146,7 +146,9 @@ Grounding substitutes variables in a rule with values from a dictionary. // Ground the rule const result = rule.ground(dictionary); - console.log(result?.toString()); // ----\nb\n + if (result !== null) { + console.log(result.toString()); // ----\nb\n + } ``` ### Matching @@ -186,10 +188,12 @@ Matching unifies the first premise of a rule with a fact, producing a new rule w // Match const result = mp.match(axiom); - console.log(result?.toString()); - // (! (! `x)) - // ---------- - // `x + if (result !== null) { + console.log(result.toString()); + // (! (! `x)) + // ---------- + // `x + } ``` ### Renaming @@ -221,7 +225,9 @@ Renaming adds prefixes and/or suffixes to all variables in a rule. // Rename with prefix and suffix const spec = new rule_t("((pre_) (_suf))"); const result = rule.rename(spec); - console.log(result?.toString()); // ----\n`pre_x_suf\n + if (result !== null) { + console.log(result.toString()); // ----\n`pre_x_suf\n + } ``` ## Rule Comparison @@ -254,50 +260,6 @@ Rules can be compared for equality. Two rules are equal if they have the same bi console.log(rule1.key() === rule3.key()); // false ``` -## Logical Systems - -DS can encode various logical systems using rules: - -### Propositional Logic - -```python -import apyds - -search = apyds.Search(1000, 10000) - -# Modus ponens: P -> Q, P |- Q -search.add("(`P -> `Q) `P `Q") - -# Axiom schemas for propositional logic: -# 1. p -> (q -> p) -search.add("(`p -> (`q -> `p))") - -# 2. (p -> (q -> r)) -> ((p -> q) -> (p -> r)) -search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))") - -# 3. (!p -> !q) -> (q -> p) -search.add("(((! `p) -> (! `q)) -> (`q -> `p))") -``` - -### Custom Domains - -You can define rules for any domain: - -```python -import apyds - -search = apyds.Search(1000, 10000) - -# Family relationships -search.add("(father `X `Y)\n----------\n(parent `X `Y)\n") -search.add("(mother `X `Y)\n----------\n(parent `X `Y)\n") -search.add("(parent `X `Y) (parent `Y `Z)\n----------\n(grandparent `X `Z)\n") - -# Facts -search.add("(father john mary)") -search.add("(mother mary alice)") -``` - ## See Also - [Terms](terms.md) - Building blocks for rules diff --git a/docs/concepts/terms.md b/docs/concepts/terms.md index 352b1a5..4638526 100644 --- a/docs/concepts/terms.md +++ b/docs/concepts/terms.md @@ -158,7 +158,9 @@ Grounding substitutes variables in a term with values from a dictionary. The dic // Ground the term const result = term.ground(dictionary); - console.log(result?.toString()); // b + if (result !== null) { + console.log(result.toString()); // b + } ``` ## Renaming @@ -195,7 +197,9 @@ Renaming adds prefixes and/or suffixes to all variables in a term. This is usefu // Rename the term const result = term.rename(spec); - console.log(result?.toString()); // `pre_x_suf + if (result !== null) { + console.log(result.toString()); // `pre_x_suf + } ``` ## Buffer Size diff --git a/docs/getting-started/installation.md b/docs/getting-started/installation.md index 4eedd9c..4569e33 100644 --- a/docs/getting-started/installation.md +++ b/docs/getting-started/installation.md @@ -1,6 +1,24 @@ # Installation -DS can be installed for Python, TypeScript/JavaScript, or used directly as a C++ library. +DS can be installed for TypeScript/JavaScript, Python, or used directly as a C++ library. + +## TypeScript/JavaScript + +The TypeScript/JavaScript package `atsds` wraps the C++ core via WebAssembly. + +```bash +npm install atsds +``` + +The package includes: + +- WebAssembly binaries (`.wasm`) +- TypeScript type definitions (`.d.mts`) +- ES module support + +### Requirements + +- Node.js 20+ or a modern browser with WebAssembly support ## Python @@ -25,31 +43,13 @@ cd ds pip install -e ".[dev]" ``` -## TypeScript/JavaScript - -The TypeScript/JavaScript package `atsds` wraps the C++ core via WebAssembly. - -```bash -npm install atsds -``` - -The package includes: - -- WebAssembly binaries (`.wasm`) -- TypeScript type definitions (`.d.mts`) -- ES module support - -### Requirements - -- Node.js 16+ or a modern browser with WebAssembly support - ## C++ The C++ library is the core implementation. Both Python and TypeScript bindings are built on top of it. ### Prerequisites -- C++20 compatible compiler (GCC 10+, Clang 10+, MSVC 2019+) +- C++20 compatible compiler - CMake 3.30+ ### Building from Source @@ -101,6 +101,15 @@ cmake --build build ## Verifying Installation +=== "TypeScript" + + ```typescript + import { term_t } from "atsds"; + + const term = new term_t("(hello world)"); + console.log(term.toString()); + ``` + === "Python" ```python @@ -112,15 +121,6 @@ cmake --build build print(term) ``` -=== "TypeScript" - - ```typescript - import { term_t } from "atsds"; - - const term = new term_t("(hello world)"); - console.log(term.toString()); - ``` - === "C++" ```cpp diff --git a/docs/index.md b/docs/index.md index 446947a..37a111e 100644 --- a/docs/index.md +++ b/docs/index.md @@ -15,15 +15,15 @@ A deductive system for logical inference, implemented in C++. The library provid ## Architecture ``` -┌─────────────────────────────────────────────────────────────┐ -│ Application Layer │ -├──────────────────┬──────────────────┬───────────────────────┤ -│ Python (apyds) │ TypeScript (atsds)│ C++ Direct │ -│ via pybind11 │ via WebAssembly │ │ -├──────────────────┴──────────────────┴───────────────────────┤ -│ C++ Core Library │ -│ (include/ds/, src/) │ -└─────────────────────────────────────────────────────────────┘ +┌────────────────────────────────────────────────────────────┐ +│ Application Layer │ +├────────────────────┬────────────────────┬──────────────────┤ +│ TypeScript (atsds) │ Python (apyds) │ C++ Direct │ +│ via WebAssembly │ via pybind11 │ │ +├────────────────────┴────────────────────┴──────────────────┤ +│ C++ Core Library │ +│ (include/ds/, src/) │ +└────────────────────────────────────────────────────────────┘ ``` ## Quick Links diff --git a/mkdocs.yml b/mkdocs.yml index 432f4ee..bed2405 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -39,8 +39,8 @@ nav: - Rules: concepts/rules.md - Search Engine: concepts/search.md - API Reference: - - Python API: api/python.md - TypeScript API: api/typescript.md + - Python API: api/python.md - C++ API: api/cpp.md - Examples: - examples/index.md From fe95ba0ad295987e01d1678190408e996a074ea9 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 25 Nov 2025 13:48:30 +0000 Subject: [PATCH 5/7] Rewrite Python API docs manually for consistency, improve term/rule structure consistency Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com> --- docs/api/python.md | 471 +++++++++++++++++++++++++++++++++++++---- docs/concepts/rules.md | 221 +++++++++++++------ docs/concepts/terms.md | 170 +++++++++------ mkdocs.yml | 13 -- pyproject.toml | 1 - 5 files changed, 699 insertions(+), 177 deletions(-) diff --git a/docs/api/python.md b/docs/api/python.md index f88e30e..ef49eb2 100644 --- a/docs/api/python.md +++ b/docs/api/python.md @@ -2,70 +2,453 @@ This page documents the Python API for the `apyds` package. -## Buffer Size Functions +```python +from apyds import ( + buffer_size, + scoped_buffer_size, + String, + Variable, + Item, + List, + Term, + Rule, + Search, +) +``` -::: apyds.buffer_size - options: - show_root_heading: true - heading_level: 3 +## buffer_size -::: apyds.scoped_buffer_size - options: - show_root_heading: true - heading_level: 3 +Gets the current buffer size, or sets a new buffer size and returns the previous value. + +```python +def buffer_size(size: int = 0) -> int +``` + +**Parameters:** + +- `size` (optional): The new buffer size to set. If 0 (default), returns current size without modification. + +**Returns:** The previous buffer size value. + +**Example:** + +```python +current_size = buffer_size() # Get current size +old_size = buffer_size(2048) # Set new size, returns old size +``` + +--- + +## scoped_buffer_size + +Context manager for temporarily changing the buffer size. + +```python +@contextmanager +def scoped_buffer_size(size: int = 0) +``` + +**Parameters:** + +- `size`: The temporary buffer size to set. + +**Example:** + +```python +with scoped_buffer_size(4096): + # Operations here use buffer size of 4096 + pass +# Buffer size is restored to previous value +``` + +--- ## String -::: apyds.String - options: - show_root_heading: true - heading_level: 3 - members_order: source +Wrapper class for deductive system strings. + +### Constructor + +```python +def __init__(self, value: String | str | bytes, size: int | None = None) +``` + +**Parameters:** + +- `value`: Initial value (string, bytes, or another String) +- `size` (optional): Buffer capacity for internal storage + +### Methods + +#### \_\_str\_\_() + +Convert the value to a string representation. + +```python +def __str__(self) -> str +``` + +#### data() + +Get the binary representation of the value. + +```python +def data(self) -> bytes +``` + +#### size() + +Get the size of the data in bytes. + +```python +def size(self) -> int +``` + +**Example:** + +```python +str1 = String("hello") +str2 = String(str1.data()) # From binary +print(str1) # "hello" +``` + +--- ## Variable -::: apyds.Variable - options: - show_root_heading: true - heading_level: 3 - members_order: source +Wrapper class for logical variables in the deductive system. + +### Constructor + +```python +def __init__(self, value: Variable | str | bytes, size: int | None = None) +``` + +**Parameters:** + +- `value`: Initial value (string starting with backtick, bytes, or another Variable) +- `size` (optional): Buffer capacity for internal storage + +### Properties + +#### name + +Get the name of this variable (without the backtick prefix). + +```python +@property +def name(self) -> String +``` + +**Example:** + +```python +var1 = Variable("`X") +print(var1.name) # "X" +print(var1) # "`X" +``` + +--- ## Item -::: apyds.Item - options: - show_root_heading: true - heading_level: 3 - members_order: source +Wrapper class for items (constants/functors) in the deductive system. + +### Constructor + +```python +def __init__(self, value: Item | str | bytes, size: int | None = None) +``` + +### Properties + +#### name + +Get the name of this item. + +```python +@property +def name(self) -> String +``` + +**Example:** + +```python +item = Item("atom") +print(item.name) # "atom" +``` + +--- ## List -::: apyds.List - options: - show_root_heading: true - heading_level: 3 - members_order: source +Wrapper class for lists in the deductive system. + +### Constructor + +```python +def __init__(self, value: List | str | bytes, size: int | None = None) +``` + +### Methods + +#### \_\_len\_\_() + +Get the number of elements in the list. + +```python +def __len__(self) -> int +``` + +#### \_\_getitem\_\_() + +Get an element from the list by index. + +```python +def __getitem__(self, index: int) -> Term +``` + +**Example:** + +```python +lst = List("(a b c)") +print(len(lst)) # 3 +print(lst[0]) # "a" +``` + +--- ## Term -::: apyds.Term - options: - show_root_heading: true - heading_level: 3 - members_order: source +Wrapper class for logical terms in the deductive system. A term can be a variable, item, or list. + +### Constructor + +```python +def __init__(self, value: Term | str | bytes, size: int | None = None) +``` + +### Properties + +#### term + +Extracts the underlying term and returns it as its concrete type. + +```python +@property +def term(self) -> Variable | Item | List +``` + +### Methods + +#### ground() + +Ground this term using a dictionary to substitute variables with values. + +```python +def ground(self, other: Term, scope: str | None = None) -> Term | None +``` + +**Parameters:** + +- `other`: A term representing a dictionary (list of pairs) +- `scope` (optional): Scope string for variable scoping + +**Returns:** The grounded term, or None if grounding fails. + +**Example:** + +```python +a = Term("`a") +dict = Term("((`a b))") +result = a.ground(dict) +if result is not None: + print(result) # "b" +``` + +#### rename() + +Rename all variables in this term by adding prefix and suffix. + +```python +def rename(self, prefix_and_suffix: Term) -> Term | None +``` + +**Parameters:** + +- `prefix_and_suffix`: A term with format `((prefix) (suffix))` + +**Returns:** The renamed term, or None if renaming fails. + +**Example:** + +```python +term = Term("`x") +spec = Term("((pre_) (_suf))") +result = term.rename(spec) +if result is not None: + print(result) # "`pre_x_suf" +``` + +--- ## Rule -::: apyds.Rule - options: - show_root_heading: true - heading_level: 3 - members_order: source +Wrapper class for logical rules in the deductive system. + +### Constructor + +```python +def __init__(self, value: Rule | str | bytes, size: int | None = None) +``` + +### Properties + +#### conclusion + +Get the conclusion of the rule. + +```python +@property +def conclusion(self) -> Term +``` + +### Methods + +#### \_\_len\_\_() + +Get the number of premises in the rule. + +```python +def __len__(self) -> int +``` + +#### \_\_getitem\_\_() + +Get a premise term by index. + +```python +def __getitem__(self, index: int) -> Term +``` + +#### ground() + +Ground this rule using a dictionary. + +```python +def ground(self, other: Rule, scope: str | None = None) -> Rule | None +``` + +#### \_\_matmul\_\_() / match + +Match this rule with another rule using unification. + +```python +def __matmul__(self, other: Rule) -> Rule | None +``` + +**Parameters:** + +- `other`: The rule to match against (must be a fact without premises) + +**Returns:** The matched rule, or None if matching fails. + +**Example:** + +```python +mp = Rule("(`p -> `q)\n`p\n`q\n") +pq = Rule("((! (! `x)) -> `x)") +result = mp @ pq +if result is not None: + print(result) + # "(! (! `x))\n----------\n`x\n" +``` + +#### rename() + +Rename all variables in this rule. + +```python +def rename(self, prefix_and_suffix: Rule) -> Rule | None +``` + +--- ## Search -::: apyds.Search - options: - show_root_heading: true - heading_level: 3 - members_order: source +Search engine for the deductive system. + +### Constructor + +```python +def __init__(self, limit_size: int = 1000, buffer_size: int = 10000) +``` + +**Parameters:** + +- `limit_size` (optional): Size of the buffer for storing rules/facts (default: 1000) +- `buffer_size` (optional): Size of the buffer for internal operations (default: 10000) + +### Methods + +#### set_limit_size() + +Set the size of the buffer for storing final objects. + +```python +def set_limit_size(self, limit_size: int) -> None +``` + +#### set_buffer_size() + +Set the buffer size for internal operations. + +```python +def set_buffer_size(self, buffer_size: int) -> None +``` + +#### reset() + +Reset the search engine, clearing all rules and facts. + +```python +def reset(self) -> None +``` + +#### add() + +Add a rule or fact to the knowledge base. + +```python +def add(self, text: str) -> bool +``` + +**Returns:** True if successfully added, False otherwise. + +#### execute() + +Execute the search engine with a callback for each inferred rule. + +```python +def execute(self, callback: Callable[[Rule], bool]) -> int +``` + +**Parameters:** + +- `callback`: Function called for each candidate rule. Return False to continue, True to stop. + +**Returns:** The number of rules processed. + +**Example:** + +```python +search = Search(1000, 10000) +search.add("(`P -> `Q) `P `Q") +search.add("(! (! X))") + +def callback(candidate): + print(candidate) + return False # Continue searching + +search.execute(callback) +``` diff --git a/docs/concepts/rules.md b/docs/concepts/rules.md index 4ab0784..a6e837d 100644 --- a/docs/concepts/rules.md +++ b/docs/concepts/rules.md @@ -54,6 +54,23 @@ Or explicitly: ## Creating Rules +=== "TypeScript" + + ```typescript + import { rule_t } from "atsds"; + + // Create a fact + const fact = new rule_t("(parent john mary)"); + + // Create a rule with premises + const rule = new rule_t("(father `X `Y)\n----------\n(parent `X `Y)\n"); + + // Access rule components + console.log(`Number of premises: ${rule.length()}`); // 1 + console.log(`First premise: ${rule.getitem(0).toString()}`); // (father `X `Y) + console.log(`Conclusion: ${rule.conclusion().toString()}`); // (parent `X `Y) + ``` + === "Python" ```python @@ -72,23 +89,6 @@ Or explicitly: print(f"Conclusion: {rule.conclusion}") # (parent `X `Y) ``` -=== "TypeScript" - - ```typescript - import { rule_t } from "atsds"; - - // Create a fact - const fact = new rule_t("(parent john mary)"); - - // Create a rule with premises - const rule = new rule_t("(father `X `Y)\n----------\n(parent `X `Y)\n"); - - // Access rule components - console.log(`Number of premises: ${rule.length()}`); // 1 - console.log(`First premise: ${rule.getitem(0).toString()}`); // (father `X `Y) - console.log(`Conclusion: ${rule.conclusion().toString()}`); // (parent `X `Y) - ``` - === "C++" ```cpp @@ -117,6 +117,24 @@ Or explicitly: Grounding substitutes variables in a rule with values from a dictionary. +=== "TypeScript" + + ```typescript + import { rule_t } from "atsds"; + + // Create a rule with variables + const rule = new rule_t("`a"); + + // Create a dictionary + const dictionary = new rule_t("((`a b))"); + + // Ground the rule + const result = rule.ground(dictionary); + if (result !== null) { + console.log(result.toString()); // ----\nb\n + } + ``` + === "Python" ```python @@ -133,21 +151,28 @@ Grounding substitutes variables in a rule with values from a dictionary. print(result) # ----\nb\n ``` -=== "TypeScript" +=== "C++" - ```typescript - import { rule_t } from "atsds"; + ```cpp + #include + #include + #include - // Create a rule with variables - const rule = new rule_t("`a"); + int main() { + // Create a rule with variables + auto rule = ds::text_to_rule("`a", 1000); - // Create a dictionary - const dictionary = new rule_t("((`a b))"); + // Create a dictionary + auto dictionary = ds::text_to_rule("((`a b))", 1000); - // Ground the rule - const result = rule.ground(dictionary); - if (result !== null) { - console.log(result.toString()); // ----\nb\n + // Ground the rule + std::byte buffer[1000]; + auto result = reinterpret_cast(buffer); + result->ground(rule.get(), dictionary.get(), nullptr, buffer + 1000); + + std::cout << ds::rule_to_text(result, 1000).get() << std::endl; // ----\nb\n + + return 0; } ``` @@ -155,6 +180,27 @@ Grounding substitutes variables in a rule with values from a dictionary. Matching unifies the first premise of a rule with a fact, producing a new rule with one fewer premise. +=== "TypeScript" + + ```typescript + import { rule_t } from "atsds"; + + // Modus ponens rule + const mp = new rule_t("(`p -> `q)\n`p\n`q\n"); + + // Double negation elimination axiom + const axiom = new rule_t("((! (! `x)) -> `x)"); + + // Match + const result = mp.match(axiom); + if (result !== null) { + console.log(result.toString()); + // (! (! `x)) + // ---------- + // `x + } + ``` + === "Python" ```python @@ -175,24 +221,28 @@ Matching unifies the first premise of a rule with a fact, producing a new rule w # `x ``` -=== "TypeScript" +=== "C++" - ```typescript - import { rule_t } from "atsds"; + ```cpp + #include + #include + #include - // Modus ponens rule - const mp = new rule_t("(`p -> `q)\n`p\n`q\n"); + int main() { + // Modus ponens rule + auto mp = ds::text_to_rule("(`p -> `q)\n`p\n`q\n", 1000); - // Double negation elimination axiom - const axiom = new rule_t("((! (! `x)) -> `x)"); + // Double negation elimination axiom + auto axiom = ds::text_to_rule("((! (! `x)) -> `x)", 1000); - // Match - const result = mp.match(axiom); - if (result !== null) { - console.log(result.toString()); - // (! (! `x)) - // ---------- - // `x + // Match + std::byte buffer[1000]; + auto result = reinterpret_cast(buffer); + result->match(mp.get(), axiom.get(), buffer + 1000); + + std::cout << ds::rule_to_text(result, 1000).get() << std::endl; + + return 0; } ``` @@ -200,6 +250,22 @@ Matching unifies the first premise of a rule with a fact, producing a new rule w Renaming adds prefixes and/or suffixes to all variables in a rule. +=== "TypeScript" + + ```typescript + import { rule_t } from "atsds"; + + // Create a rule + const rule = new rule_t("`x"); + + // Rename with prefix and suffix + const spec = new rule_t("((pre_) (_suf))"); + const result = rule.rename(spec); + if (result !== null) { + console.log(result.toString()); // ----\n`pre_x_suf\n + } + ``` + === "Python" ```python @@ -214,19 +280,28 @@ Renaming adds prefixes and/or suffixes to all variables in a rule. print(result) # ----\n`pre_x_suf\n ``` -=== "TypeScript" +=== "C++" - ```typescript - import { rule_t } from "atsds"; + ```cpp + #include + #include + #include - // Create a rule - const rule = new rule_t("`x"); + int main() { + // Create a rule + auto rule = ds::text_to_rule("`x", 1000); - // Rename with prefix and suffix - const spec = new rule_t("((pre_) (_suf))"); - const result = rule.rename(spec); - if (result !== null) { - console.log(result.toString()); // ----\n`pre_x_suf\n + // Rename with prefix and suffix + auto spec = ds::text_to_rule("((pre_) (_suf))", 1000); + + // Rename the rule + std::byte buffer[1000]; + auto result = reinterpret_cast(buffer); + result->rename(rule.get(), spec.get(), buffer + 1000); + + std::cout << ds::rule_to_text(result, 1000).get() << std::endl; // ----\n`pre_x_suf\n + + return 0; } ``` @@ -234,6 +309,19 @@ Renaming adds prefixes and/or suffixes to all variables in a rule. Rules can be compared for equality. Two rules are equal if they have the same binary representation. +=== "TypeScript" + + ```typescript + import { rule_t } from "atsds"; + + const rule1 = new rule_t("(a b c)"); + const rule2 = new rule_t("(a b c)"); + const rule3 = new rule_t("(a b d)"); + + console.log(rule1.key() === rule2.key()); // true + console.log(rule1.key() === rule3.key()); // false + ``` + === "Python" ```python @@ -247,17 +335,30 @@ Rules can be compared for equality. Two rules are equal if they have the same bi print(rule1 == rule3) # False ``` -=== "TypeScript" +=== "C++" - ```typescript - import { rule_t } from "atsds"; + ```cpp + #include + #include + #include + #include - const rule1 = new rule_t("(a b c)"); - const rule2 = new rule_t("(a b c)"); - const rule3 = new rule_t("(a b d)"); + int main() { + auto rule1 = ds::text_to_rule("(a b c)", 1000); + auto rule2 = ds::text_to_rule("(a b c)", 1000); + auto rule3 = ds::text_to_rule("(a b d)", 1000); - console.log(rule1.key() === rule2.key()); // true - console.log(rule1.key() === rule3.key()); // false + bool eq12 = rule1->data_size() == rule2->data_size() && + memcmp(rule1->head(), rule2->head(), rule1->data_size()) == 0; + bool eq13 = rule1->data_size() == rule3->data_size() && + memcmp(rule1->head(), rule3->head(), rule1->data_size()) == 0; + + std::cout << std::boolalpha; + std::cout << eq12 << std::endl; // true + std::cout << eq13 << std::endl; // false + + return 0; + } ``` ## See Also diff --git a/docs/concepts/terms.md b/docs/concepts/terms.md index 4638526..89a9547 100644 --- a/docs/concepts/terms.md +++ b/docs/concepts/terms.md @@ -49,31 +49,7 @@ Lists are ordered sequences of terms enclosed in parentheses. They can contain a Lists are the primary way to build complex structures in the deductive system. -## Working with Terms - -=== "Python" - - ```python - import apyds - - # Create a variable - var = apyds.Variable("`X") - print(f"Variable name: {var.name}") # X - - # Create an item - item = apyds.Item("hello") - print(f"Item name: {item.name}") # hello - - # Create a list - lst = apyds.List("(a b c)") - print(f"List length: {len(lst)}") # 3 - print(f"First element: {lst[0]}") # a - - # Create a generic term - term = apyds.Term("(f `x)") - # Access the underlying type - inner = term.term # Returns a List - ``` +## Creating Terms === "TypeScript" @@ -99,6 +75,30 @@ Lists are the primary way to build complex structures in the deductive system. const inner = term.term(); // Returns a list_t ``` +=== "Python" + + ```python + import apyds + + # Create a variable + var = apyds.Variable("`X") + print(f"Variable name: {var.name}") # X + + # Create an item + item = apyds.Item("hello") + print(f"Item name: {item.name}") # hello + + # Create a list + lst = apyds.List("(a b c)") + print(f"List length: {len(lst)}") # 3 + print(f"First element: {lst[0]}") # a + + # Create a generic term + term = apyds.Term("(f `x)") + # Access the underlying type + inner = term.term # Returns a List + ``` + === "C++" ```cpp @@ -124,10 +124,30 @@ Lists are the primary way to build complex structures in the deductive system. } ``` -## Grounding +## Term Operations + +### Grounding Grounding substitutes variables in a term with values from a dictionary. The dictionary is a list of key-value pairs where each key is a variable and each value is its substitution. +=== "TypeScript" + + ```typescript + import { term_t } from "atsds"; + + // Create a term with a variable + const term = new term_t("`a"); + + // Create a dictionary for substitution + const dictionary = new term_t("((`a b))"); + + // Ground the term + const result = term.ground(dictionary); + if (result !== null) { + console.log(result.toString()); // b + } + ``` + === "Python" ```python @@ -145,28 +165,53 @@ Grounding substitutes variables in a term with values from a dictionary. The dic print(result) # b ``` +=== "C++" + + ```cpp + #include + #include + #include + + int main() { + // Create a term with a variable + auto term = ds::text_to_term("`a", 1000); + + // Create a dictionary for substitution + auto dictionary = ds::text_to_term("((`a b))", 1000); + + // Ground the term + std::byte buffer[1000]; + auto result = reinterpret_cast(buffer); + result->ground(term.get(), dictionary.get(), nullptr, buffer + 1000); + + std::cout << ds::term_to_text(result, 1000).get() << std::endl; // b + + return 0; + } + ``` + +### Renaming + +Renaming adds prefixes and/or suffixes to all variables in a term. This is useful for avoiding variable name collisions during unification. + === "TypeScript" ```typescript import { term_t } from "atsds"; // Create a term with a variable - const term = new term_t("`a"); + const term = new term_t("`x"); - // Create a dictionary for substitution - const dictionary = new term_t("((`a b))"); + // Create prefix and suffix specification + const spec = new term_t("((pre_) (_suf))"); - // Ground the term - const result = term.ground(dictionary); + // Rename the term + const result = term.rename(spec); if (result !== null) { - console.log(result.toString()); // b + console.log(result.toString()); // `pre_x_suf } ``` -## Renaming - -Renaming adds prefixes and/or suffixes to all variables in a term. This is useful for avoiding variable name collisions during unification. - === "Python" ```python @@ -184,21 +229,28 @@ Renaming adds prefixes and/or suffixes to all variables in a term. This is usefu print(result) # `pre_x_suf ``` -=== "TypeScript" +=== "C++" - ```typescript - import { term_t } from "atsds"; + ```cpp + #include + #include + #include - // Create a term with a variable - const term = new term_t("`x"); + int main() { + // Create a term with a variable + auto term = ds::text_to_term("`x", 1000); - // Create prefix and suffix specification - const spec = new term_t("((pre_) (_suf))"); + // Create prefix and suffix specification + auto spec = ds::text_to_term("((pre_) (_suf))", 1000); - // Rename the term - const result = term.rename(spec); - if (result !== null) { - console.log(result.toString()); // `pre_x_suf + // Rename the term + std::byte buffer[1000]; + auto result = reinterpret_cast(buffer); + result->rename(term.get(), spec.get(), buffer + 1000); + + std::cout << ds::term_to_text(result, 1000).get() << std::endl; // `pre_x_suf + + return 0; } ``` @@ -206,6 +258,18 @@ Renaming adds prefixes and/or suffixes to all variables in a term. This is usefu Operations like grounding and renaming require buffer space for intermediate results. You can control this using buffer size functions. +=== "TypeScript" + + ```typescript + import { buffer_size } from "atsds"; + + // Get current buffer size + const current = buffer_size(); + + // Set new buffer size (returns previous value) + const old = buffer_size(4096); + ``` + === "Python" ```python @@ -224,18 +288,6 @@ Operations like grounding and renaming require buffer space for intermediate res # Buffer size restored to previous value ``` -=== "TypeScript" - - ```typescript - import { buffer_size } from "atsds"; - - // Get current buffer size - const current = buffer_size(); - - // Set new buffer size (returns previous value) - const old = buffer_size(4096); - ``` - ## See Also - [Rules](rules.md) - How to create and work with inference rules diff --git a/mkdocs.yml b/mkdocs.yml index bed2405..383be40 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -47,19 +47,6 @@ nav: plugins: - search - - mkdocstrings: - default_handler: python - handlers: - python: - options: - show_source: false - show_root_heading: true - show_root_full_path: false - heading_level: 2 - members_order: source - docstring_style: google - merge_init_into_class: true - show_signature_annotations: true markdown_extensions: - pymdownx.highlight: diff --git a/pyproject.toml b/pyproject.toml index 0e9fa81..af667c5 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -38,7 +38,6 @@ dev = [ docs = [ "mkdocs~=1.6.1", "mkdocs-material~=9.6.14", - "mkdocstrings[python]~=0.29.1", ] [tool.ruff] From cc9588b7be639f7950d52749f5a293555dad6a0f Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 25 Nov 2025 13:59:37 +0000 Subject: [PATCH 6/7] Fix C++ Utility Functions docs and Python Requirements format Co-authored-by: hzhangxyz <11623447+hzhangxyz@users.noreply.github.com> --- docs/api/cpp.md | 66 +++++++++++++++++++++------- docs/getting-started/installation.md | 2 +- 2 files changed, 51 insertions(+), 17 deletions(-) diff --git a/docs/api/cpp.md b/docs/api/cpp.md index c1925e9..f59b0e3 100644 --- a/docs/api/cpp.md +++ b/docs/api/cpp.md @@ -491,32 +491,66 @@ length_t execute(const std::function& callback); Helper functions in ``. -### text_to_* Functions +### text_to_term() -Parse text into objects. Returns a unique_ptr to the created object. +Parse text into a term object. ```cpp -std::unique_ptr text_to_string(const char* text, length_t size); -std::unique_ptr text_to_variable(const char* text, length_t size); -std::unique_ptr text_to_item(const char* text, length_t size); -std::unique_ptr text_to_list(const char* text, length_t size); -std::unique_ptr text_to_term(const char* text, length_t size); -std::unique_ptr text_to_rule(const char* text, length_t size); +std::unique_ptr text_to_term(const char* text, length_t length); ``` -### *_to_text Functions +**Parameters:** + +- `text`: The text representation of the term +- `length`: Maximum size for the resulting binary term + +**Returns:** A unique_ptr to the created term, or nullptr if length exceeded. + +### term_to_text() + +Convert a term object to text. + +```cpp +std::unique_ptr term_to_text(term_t* term, length_t length); +``` + +**Parameters:** + +- `term`: The binary term to convert +- `length`: Maximum size for the resulting text + +**Returns:** A unique_ptr to the text, or nullptr if length exceeded. + +### text_to_rule() -Convert objects to text. Returns a unique_ptr to a char array. +Parse text into a rule object. ```cpp -std::unique_ptr string_to_text(string_t* string, length_t size); -std::unique_ptr variable_to_text(variable_t* variable, length_t size); -std::unique_ptr item_to_text(item_t* item, length_t size); -std::unique_ptr list_to_text(list_t* list, length_t size); -std::unique_ptr term_to_text(term_t* term, length_t size); -std::unique_ptr rule_to_text(rule_t* rule, length_t size); +std::unique_ptr text_to_rule(const char* text, length_t length); ``` +**Parameters:** + +- `text`: The text representation of the rule +- `length`: Maximum size for the resulting binary rule + +**Returns:** A unique_ptr to the created rule, or nullptr if length exceeded. + +### rule_to_text() + +Convert a rule object to text. + +```cpp +std::unique_ptr rule_to_text(rule_t* rule, length_t length); +``` + +**Parameters:** + +- `rule`: The binary rule to convert +- `length`: Maximum size for the resulting text + +**Returns:** A unique_ptr to the text, or nullptr if length exceeded. + --- ## Example diff --git a/docs/getting-started/installation.md b/docs/getting-started/installation.md index 4569e33..3e59aac 100644 --- a/docs/getting-started/installation.md +++ b/docs/getting-started/installation.md @@ -28,7 +28,7 @@ The Python package `apyds` wraps the C++ core via pybind11. pip install apyds ``` -**Requirements:** +### Requirements - Python 3.10-3.14 - Pre-built wheels are available for common platforms From 268d61206a5448664bc757b512e7ee8313a5b6da Mon Sep 17 00:00:00 2001 From: Hao Zhang Date: Tue, 25 Nov 2025 22:09:01 +0800 Subject: [PATCH 7/7] Remove example in api for cpp. --- docs/api/cpp.md | 48 ------------------------------------------------ 1 file changed, 48 deletions(-) diff --git a/docs/api/cpp.md b/docs/api/cpp.md index f59b0e3..eadc7be 100644 --- a/docs/api/cpp.md +++ b/docs/api/cpp.md @@ -550,51 +550,3 @@ 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. - ---- - -## Example - -```cpp -#include -#include -#include -#include -#include - -int main() { - // Create search engine - ds::search_t search(1000, 10000); - - // Add modus ponens rule - search.add("(`P -> `Q) `P `Q"); - - // Add axiom schemas - search.add("(`p -> (`q -> `p))"); - search.add("((`p -> (`q -> `r)) -> ((`p -> `q) -> (`p -> `r)))"); - search.add("(((! `p) -> (! `q)) -> (`q -> `p))"); - - // Add premise - search.add("(! (! X))"); - - // Define target - auto target = ds::text_to_rule("X", 1000); - - // Search until target is found - while (true) { - bool found = false; - search.execute([&](ds::rule_t* candidate) { - if (candidate->data_size() == target->data_size() && - memcmp(candidate->head(), target->head(), candidate->data_size()) == 0) { - printf("Found: %s", ds::rule_to_text(candidate, 1000).get()); - found = true; - return true; - } - return false; - }); - if (found) break; - } - - return 0; -} -```