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..eadc7be --- /dev/null +++ b/docs/api/cpp.md @@ -0,0 +1,552 @@ +# C++ API Reference + +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. + +## 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_term() + +Parse text into a term object. + +```cpp +std::unique_ptr text_to_term(const char* text, length_t length); +``` + +**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() + +Parse text into a rule object. + +```cpp +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. diff --git a/docs/api/python.md b/docs/api/python.md new file mode 100644 index 0000000..ef49eb2 --- /dev/null +++ b/docs/api/python.md @@ -0,0 +1,454 @@ +# Python API Reference + +This page documents the Python API for the `apyds` package. + +```python +from apyds import ( + buffer_size, + scoped_buffer_size, + String, + Variable, + Item, + List, + Term, + Rule, + Search, +) +``` + +## buffer_size + +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 + +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 + +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 + +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 + +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 + +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 + +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 + +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/api/typescript.md b/docs/api/typescript.md new file mode 100644 index 0000000..e1a74ff --- /dev/null +++ b/docs/api/typescript.md @@ -0,0 +1,449 @@ +# TypeScript API Reference + +This page documents the TypeScript API for the `atsds` package. The documentation is generated from the TypeScript source code. + +```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))"); +const result = a.ground(dict); +if (result !== null) { + console.log(result.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))"); +const result = term.rename(spec); +if (result !== null) { + console.log(result.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)"); +const result = mp.match(pq); +if (result !== null) { + console.log(result.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..a6e837d --- /dev/null +++ b/docs/concepts/rules.md @@ -0,0 +1,367 @@ +# 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 + +=== "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 + 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) + ``` + +=== "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. + +=== "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 + 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 + ``` + +=== "C++" + + ```cpp + #include + #include + #include + + int main() { + // Create a rule with variables + auto rule = ds::text_to_rule("`a", 1000); + + // Create a dictionary + auto dictionary = ds::text_to_rule("((`a b))", 1000); + + // 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; + } + ``` + +### Matching + +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 + 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 + ``` + +=== "C++" + + ```cpp + #include + #include + #include + + int main() { + // Modus ponens rule + auto mp = ds::text_to_rule("(`p -> `q)\n`p\n`q\n", 1000); + + // Double negation elimination axiom + auto axiom = ds::text_to_rule("((! (! `x)) -> `x)", 1000); + + // 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; + } + ``` + +### Renaming + +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 + 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 + ``` + +=== "C++" + + ```cpp + #include + #include + #include + + int main() { + // Create a rule + auto rule = ds::text_to_rule("`x", 1000); + + // 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; + } + ``` + +## Rule Comparison + +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 + 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 + ``` + +=== "C++" + + ```cpp + #include + #include + #include + #include + + 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); + + 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 + +- [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..75fd747 --- /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): + nonlocal 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..89a9547 --- /dev/null +++ b/docs/concepts/terms.md @@ -0,0 +1,294 @@ +# 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. + +## Creating Terms + +=== "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 + ``` + +=== "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 + #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; + } + ``` + +## 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 + 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 + ``` + +=== "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("`x"); + + // Create prefix and suffix specification + const spec = new term_t("((pre_) (_suf))"); + + // Rename the term + const result = term.rename(spec); + if (result !== null) { + console.log(result.toString()); // `pre_x_suf + } + ``` + +=== "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 + ``` + +=== "C++" + + ```cpp + #include + #include + #include + + int main() { + // Create a term with a variable + auto term = ds::text_to_term("`x", 1000); + + // Create prefix and suffix specification + auto spec = ds::text_to_term("((pre_) (_suf))", 1000); + + // 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; + } + ``` + +## Buffer Size + +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 + 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 + ``` + +## 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..829acaf --- /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): + nonlocal 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..3e59aac --- /dev/null +++ b/docs/getting-started/installation.md @@ -0,0 +1,136 @@ +# Installation + +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 + +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]" +``` + +## C++ + +The C++ library is the core implementation. Both Python and TypeScript bindings are built on top of it. + +### Prerequisites + +- C++20 compatible compiler +- 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 + +=== "TypeScript" + + ```typescript + import { term_t } from "atsds"; + + const term = new term_t("(hello world)"); + console.log(term.toString()); + ``` + +=== "Python" + + ```python + import apyds + print(apyds.__version__) + + # Create a simple term + term = apyds.Term("(hello world)") + print(term) + ``` + +=== "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..3f612c1 --- /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): + nonlocal 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..37a111e --- /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 │ +├────────────────────┬────────────────────┬──────────────────┤ +│ TypeScript (atsds) │ Python (apyds) │ C++ Direct │ +│ via WebAssembly │ via pybind11 │ │ +├────────────────────┴────────────────────┴──────────────────┤ +│ 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..383be40 --- /dev/null +++ b/mkdocs.yml @@ -0,0 +1,71 @@ +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: + - TypeScript API: api/typescript.md + - Python API: api/python.md + - C++ API: api/cpp.md + - Examples: + - examples/index.md + +plugins: + - search + +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..af667c5 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -35,6 +35,10 @@ dev = [ "pytest~=9.0.1", "pytest-cov~=7.0.0", ] +docs = [ + "mkdocs~=1.6.1", + "mkdocs-material~=9.6.14", +] [tool.ruff] line-length = 120