diff --git a/.vitepress/config.mts b/.vitepress/config.mts index 095e134..4bbf873 100644 --- a/.vitepress/config.mts +++ b/.vitepress/config.mts @@ -1,5 +1,5 @@ -import { defineConfig } from "vitepress"; import path from "node:path"; +import { defineConfig } from "vitepress"; // https://vitepress.dev/reference/site-config export default defineConfig({ @@ -8,57 +8,119 @@ export default defineConfig({ description: "A deductive system for logical inference, implemented in C++ with bindings for Python and TypeScript/JavaScript", srcDir: "docs", - themeConfig: { - // https://vitepress.dev/reference/default-theme-config - nav: [ - { text: "Home", link: "/" }, - { text: "Getting Started", link: "/getting-started/installation" }, - { text: "Core Concepts", link: "/concepts/terms" }, - { text: "API Reference", link: "/api/typescript" }, - { text: "Support Packages", link: "/support-packages/bnf" }, - { text: "Examples", link: "/examples/basic" }, - ], - sidebar: [ - { - text: "Getting Started", - items: [ - { text: "Installation", link: "/getting-started/installation" }, - { text: "Quick Start", link: "/getting-started/quickstart" }, + locales: { + en: { + label: "English", + lang: "en", + link: "/en/", + themeConfig: { + nav: [ + { text: "Home", link: "/en/" }, + { text: "Getting Started", link: "/en/getting-started/installation" }, + { text: "Core Concepts", link: "/en/concepts/terms" }, + { text: "API Reference", link: "/en/api/typescript" }, + { text: "Support Packages", link: "/en/support-packages/bnf" }, + { text: "Examples", link: "/en/examples/basic" }, ], - }, - { - text: "Core Concepts", - items: [ - { text: "Terms", link: "/concepts/terms" }, - { text: "Rules", link: "/concepts/rules" }, - { text: "Search Engine", link: "/concepts/search" }, - ], - }, - { - text: "API Reference", - items: [ - { text: "TypeScript API", link: "/api/typescript" }, - { text: "Python API", link: "/api/python" }, - { text: "C++ API", link: "/api/cpp" }, + sidebar: [ + { + text: "Getting Started", + items: [ + { text: "Installation", link: "/en/getting-started/installation" }, + { text: "Quick Start", link: "/en/getting-started/quickstart" }, + ], + }, + { + text: "Core Concepts", + items: [ + { text: "Terms", link: "/en/concepts/terms" }, + { text: "Rules", link: "/en/concepts/rules" }, + { text: "Search Engine", link: "/en/concepts/search" }, + ], + }, + { + text: "API Reference", + items: [ + { text: "TypeScript API", link: "/en/api/typescript" }, + { text: "Python API", link: "/en/api/python" }, + { text: "C++ API", link: "/en/api/cpp" }, + ], + }, + { + text: "Support Packages", + items: [ + { text: "BNF", link: "/en/support-packages/bnf" }, + { text: "E-Graph", link: "/en/support-packages/egg" }, + ], + }, + { + text: "Examples", + items: [ + { text: "Basic Examples", link: "/en/examples/basic" }, + { text: "Sudoku", link: "/en/examples/sudoku" }, + ], + }, ], }, - { - text: "Support Packages", - items: [ - { text: "BNF", link: "/support-packages/bnf" }, - { text: "E-Graph", link: "/support-packages/egg" }, + }, + zh: { + label: "简体中文", + lang: "zh", + link: "/zh/", + themeConfig: { + nav: [ + { text: "首页", link: "/zh/" }, + { text: "快速开始", link: "/zh/getting-started/installation" }, + { text: "核心概念", link: "/zh/concepts/terms" }, + { text: "API 参考", link: "/zh/api/typescript" }, + { text: "支持包", link: "/zh/support-packages/bnf" }, + { text: "示例", link: "/zh/examples/basic" }, ], - }, - { - text: "Examples", - items: [ - { text: "Basis Examples", link: "/examples/basic" }, - { text: "Sudoku", link: "/examples/sudoku" }, + sidebar: [ + { + text: "快速开始", + items: [ + { text: "安装", link: "/zh/getting-started/installation" }, + { text: "快速上手", link: "/zh/getting-started/quickstart" }, + ], + }, + { + text: "核心概念", + items: [ + { text: "Term", link: "/zh/concepts/terms" }, + { text: "Rule", link: "/zh/concepts/rules" }, + { text: "搜索引擎", link: "/zh/concepts/search" }, + ], + }, + { + text: "API 参考", + items: [ + { text: "TypeScript API", link: "/zh/api/typescript" }, + { text: "Python API", link: "/zh/api/python" }, + { text: "C++ API", link: "/zh/api/cpp" }, + ], + }, + { + text: "支持包", + items: [ + { text: "BNF", link: "/zh/support-packages/bnf" }, + { text: "E-Graph", link: "/zh/support-packages/egg" }, + ], + }, + { + text: "示例", + items: [ + { text: "基础示例", link: "/zh/examples/basic" }, + { text: "数独", link: "/zh/examples/sudoku" }, + ], + }, ], }, - ], + }, + }, + themeConfig: { search: { provider: "local" }, socialLinks: [{ icon: "github", link: "https://github.com/USTC-KnowledgeComputingLab/ds" }], }, diff --git a/docs/api/cpp.md b/docs/en/api/cpp.md similarity index 100% rename from docs/api/cpp.md rename to docs/en/api/cpp.md diff --git a/docs/api/python.md b/docs/en/api/python.md similarity index 100% rename from docs/api/python.md rename to docs/en/api/python.md diff --git a/docs/api/typescript.md b/docs/en/api/typescript.md similarity index 100% rename from docs/api/typescript.md rename to docs/en/api/typescript.md diff --git a/docs/concepts/rules.md b/docs/en/concepts/rules.md similarity index 100% rename from docs/concepts/rules.md rename to docs/en/concepts/rules.md diff --git a/docs/concepts/search.md b/docs/en/concepts/search.md similarity index 100% rename from docs/concepts/search.md rename to docs/en/concepts/search.md diff --git a/docs/concepts/terms.md b/docs/en/concepts/terms.md similarity index 100% rename from docs/concepts/terms.md rename to docs/en/concepts/terms.md diff --git a/docs/examples/basic.md b/docs/en/examples/basic.md similarity index 100% rename from docs/examples/basic.md rename to docs/en/examples/basic.md diff --git a/docs/examples/sudoku.md b/docs/en/examples/sudoku.md similarity index 94% rename from docs/examples/sudoku.md rename to docs/en/examples/sudoku.md index 526d72e..bccfee1 100644 --- a/docs/examples/sudoku.md +++ b/docs/en/examples/sudoku.md @@ -13,7 +13,7 @@ The Sudoku solver encodes Sudoku rules as logical inference rules in the DS syst ## Interactive Demo diff --git a/docs/getting-started/installation.md b/docs/en/getting-started/installation.md similarity index 100% rename from docs/getting-started/installation.md rename to docs/en/getting-started/installation.md diff --git a/docs/getting-started/quickstart.md b/docs/en/getting-started/quickstart.md similarity index 100% rename from docs/getting-started/quickstart.md rename to docs/en/getting-started/quickstart.md diff --git a/docs/en/index.md b/docs/en/index.md new file mode 100644 index 0000000..54fedbc --- /dev/null +++ b/docs/en/index.md @@ -0,0 +1,70 @@ +--- +layout: home + +hero: + name: "DS" + text: "A Deductive System" + tagline: A deductive system for logical inference, implemented in C++ with bindings for Python and TypeScript/JavaScript + actions: + - theme: brand + text: Quick Start + link: /en/getting-started/quickstart + - theme: alt + text: View on GitHub + link: https://github.com/USTC-KnowledgeComputingLab/ds + +features: + - title: Multi-Language Support + details: Seamlessly use the same deductive system in C++, Python, or TypeScript/JavaScript. + - title: WebAssembly Performance + details: Run high-performance deductive system in the browser or Node.js via Emscripten. + - title: Rich Logical Terms + details: Comprehensive support for variables, items, and nested lists. + - title: Rule-Based Inference + details: Flexible framework for defining rules and facts to perform complex logical deduction. + - title: Unification Engine + details: Powerful built-in mechanisms for term unification and rule matching. + - title: Automated Search + details: Built-in search engine for iterative inference. +--- + +## Supported Languages + +::: code-group +```typescript [TypeScript] +import { Term } from "atsds"; + +const term = new Term("(hello world)"); +console.log(term.toString()); +// Output: (hello world) +``` +```python [Python] +import apyds + +term = apyds.Term("(hello world)") +print(term) # (hello world) +``` +```cpp [C++] +#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; +} +``` +::: + +## 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/typescript.md)** - Complete API documentation +- **[Examples](examples/basic.md)** - Working code examples + +## License + +This project is licensed under the GNU General Public License v3.0 or later. diff --git a/docs/support-packages/bnf.md b/docs/en/support-packages/bnf.md similarity index 100% rename from docs/support-packages/bnf.md rename to docs/en/support-packages/bnf.md diff --git a/docs/support-packages/egg.md b/docs/en/support-packages/egg.md similarity index 100% rename from docs/support-packages/egg.md rename to docs/en/support-packages/egg.md diff --git a/docs/index.md b/docs/index.md index 84e42ce..d955b11 100644 --- a/docs/index.md +++ b/docs/index.md @@ -1,70 +1,19 @@ --- layout: home - -hero: - name: "DS" - text: "A Deductive System" - tagline: A deductive system for logical inference, implemented in C++ with bindings for Python and TypeScript/JavaScript - actions: - - theme: brand - text: Quick Start - link: /getting-started/quickstart - - theme: alt - text: View on GitHub - link: https://github.com/USTC-KnowledgeComputingLab/ds - -features: - - title: Multi-Language Support - details: Seamlessly use the same deductive system in C++, Python, or TypeScript/JavaScript. - - title: WebAssembly Performance - details: Run high-performance deductive system in the browser or Node.js via Emscripten. - - title: Rich Logical Terms - details: Comprehensive support for variables, items, and nested lists. - - title: Rule-Based Inference - details: Flexible framework for defining rules and facts to perform complex logical deduction. - - title: Unification Engine - details: Powerful built-in mechanisms for term unification and rule matching. - - title: Automated Search - details: Built-in search engine for iterative inference. --- -## Supported Languages - -::: code-group -```typescript [TypeScript] -import { Term } from "atsds"; - -const term = new Term("(hello world)"); -console.log(term.toString()); -// Output: (hello world) -``` -```python [Python] -import apyds - -term = apyds.Term("(hello world)") -print(term) # (hello world) -``` -```cpp [C++] -#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; -} -``` -::: - -## 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/typescript.md)** - Complete API documentation -- **[Examples](examples/basic.md)** - Working code examples - -## License - -This project is licensed under the GNU General Public License v3.0 or later. \ No newline at end of file + diff --git a/docs/zh/api/cpp.md b/docs/zh/api/cpp.md new file mode 100644 index 0000000..81589fa --- /dev/null +++ b/docs/zh/api/cpp.md @@ -0,0 +1,622 @@ +# C++ API 参考 + +本页记录了 DS 库的 C++ API。文档由 C++ 源代码生成。 + +所有类和函数都在 `ds` 命名空间中。 + +## 头文件 + +```cpp +#include // 所有基本类型 +#include // 搜索引擎 +#include // 辅助函数 +``` + +--- + +## string_t + +字符串处理类。定义在 `` 中。 + +### 方法 + +#### data_size() + +获取字符串数据的大小（以字节为单位）。 + +```cpp +length_t data_size(); +``` + +#### head() + +获取指向第一个字节的指针。 + +```cpp +std::byte* head(); +``` + +#### tail() + +获取指向最后一个字节之后的指针。 + +```cpp +std::byte* tail(); +``` + +#### print() + +将字符串输出到缓冲区。 + +```cpp +char* print(char* buffer, char* check_tail = nullptr); +``` + +#### scan() + +从缓冲区读取字符串。 + +```cpp +const char* scan(const char* buffer, std::byte* check_tail = nullptr); +``` + +--- + +## variable_t + +逻辑 Variable 类。定义在 `` 中。 + +Variable 表示可以与其他 Term 进行合一的占位符。 + +### 方法 + +#### name() + +获取 Variable 的名称（不带反引号前缀）。 + +```cpp +string_t* name(); +``` + +#### data_size() + +获取 Variable 数据的大小（以字节为单位）。 + +```cpp +length_t data_size(); +``` + +#### head() / tail() + +获取指向数据边界的指针。 + +```cpp +std::byte* head(); +std::byte* tail(); +``` + +#### print() / scan() + +输入/输出操作。 + +```cpp +char* print(char* buffer, char* check_tail = nullptr); +const char* scan(const char* buffer, std::byte* check_tail = nullptr); +``` + +--- + +## item_t + +Item（常量/函子）类。定义在 `` 中。 + +Item 表示原子值或函数符号。 + +### 方法 + +#### name() + +获取 Item 的名称。 + +```cpp +string_t* name(); +``` + +#### data_size() + +获取 Item 数据的大小（以字节为单位）。 + +```cpp +length_t data_size(); +``` + +#### head() / tail() + +获取指向数据边界的指针。 + +```cpp +std::byte* head(); +std::byte* tail(); +``` + +#### print() / scan() + +输入/输出操作。 + +```cpp +char* print(char* buffer, char* check_tail = nullptr); +const char* scan(const char* buffer, std::byte* check_tail = nullptr); +``` + +--- + +## list_t + +List 类。定义在 `` 中。 + +List 包含 Term 的有序序列。 + +### 方法 + +#### length() + +获取 List 中的元素数量。 + +```cpp +length_t length(); +``` + +#### getitem() + +通过索引获取元素。 + +```cpp +term_t* getitem(length_t index); +``` + +#### data_size() + +获取 List 数据的大小（以字节为单位）。 + +```cpp +length_t data_size(); +``` + +#### head() / tail() + +获取指向数据边界的指针。 + +```cpp +std::byte* head(); +std::byte* tail(); +``` + +#### print() / scan() + +输入/输出操作。 + +```cpp +char* print(char* buffer, char* check_tail = nullptr); +const char* scan(const char* buffer, std::byte* check_tail = nullptr); +``` + +--- + +## term_t + +通用 Term 类。定义在 `` 中。 + +一个 Term 可以是 Variable、Item 或 List。 + +### 枚举：term_type_t + +```cpp +enum class term_type_t : min_uint_t { + null = 0, + variable = 1, + item = 2, + list = 3 +}; +``` + +### 方法 + +#### get_type() + +获取此 Term 的类型。 + +```cpp +term_type_t get_type(); +``` + +#### is_null() + +检查 Term 是否为 null。 + +```cpp +bool is_null(); +``` + +#### variable() / item() / list() + +获取作为特定类型的底层值。如果 Term 不是该类型，则返回 nullptr。 + +```cpp +variable_t* variable(); +item_t* item(); +list_t* list(); +``` + +#### set_type() / set_null() / set_variable() / set_item() / set_list() + +设置 Term 类型。 + +```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() + +获取 Term 数据的大小（以字节为单位）。 + +```cpp +length_t data_size(); +``` + +#### head() / tail() + +获取指向数据边界的指针。 + +```cpp +std::byte* head(); +std::byte* tail(); +``` + +#### print() / scan() + +输入/输出操作。 + +```cpp +char* print(char* buffer, char* check_tail = nullptr); +const char* scan(const char* buffer, std::byte* check_tail = nullptr); +``` + +#### ground() + +使用字典将此 Term 具体化 (Ground)，替换 Variable。 + +```cpp +term_t* ground(term_t* term, term_t* dictionary, const char* scope, + std::byte* check_tail = nullptr); +``` + +#### match() + +将两个 Term 进行合一并生成合一字典。 + +```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() + +通过添加前缀和后缀重命名 Variable。 + +```cpp +term_t* rename(term_t* term, term_t* prefix_and_suffix, + std::byte* check_tail = nullptr); +``` + +--- + +## rule_t + +逻辑 Rule 类。定义在 `` 中。 + +一条 Rule 由前提和结论组成。 + +### 方法 + +#### conclusion() + +获取 Rule 的结论。 + +```cpp +term_t* conclusion(); +``` + +#### only_conclusion() + +仅当没有前提时获取结论。否则返回 nullptr。 + +```cpp +term_t* only_conclusion(); +``` + +#### premises() + +通过索引获取前提。 + +```cpp +term_t* premises(length_t index); +``` + +#### premises_count() + +获取前提的数量。 + +```cpp +length_t premises_count(); +``` + +#### valid() + +检查 Rule 是否有效。 + +```cpp +bool valid(); +``` + +#### data_size() + +获取 Rule 数据的大小（以字节为单位）。 + +```cpp +length_t data_size(); +``` + +#### head() / tail() + +获取指向数据边界的指针。 + +```cpp +std::byte* head(); +std::byte* tail(); +``` + +#### print() / scan() + +输入/输出操作。 + +```cpp +char* print(char* buffer, char* check_tail = nullptr); +const char* scan(const char* buffer, std::byte* check_tail = nullptr); +``` + +#### ground() + +使用字典将此 Rule 具体化 (Ground)。 + +```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() + +将此 Rule 与事实进行匹配。 + +```cpp +rule_t* match(rule_t* rule_1, rule_t* rule_2, + std::byte* check_tail = nullptr); +``` + +#### rename() + +重命名此 Rule 中的 Variable。 + +```cpp +rule_t* rename(rule_t* rule, rule_t* prefix_and_suffix, + std::byte* check_tail = nullptr); +``` + +--- + +## search_t + +搜索引擎类。定义在 `` 中。 + +管理知识库并执行逻辑推理。 + +### 构造函数 + +```cpp +search_t(length_t limit_size, length_t buffer_size); +``` + +**参数：** + +- `limit_size`：每个存储的 Rule/事实的最大大小 +- `buffer_size`：操作的内部缓冲区大小 + +### 方法 + +#### set_limit_size() + +设置最大 Rule/事实大小。 + +```cpp +void set_limit_size(length_t limit_size); +``` + +#### set_buffer_size() + +设置内部缓冲区大小。 + +```cpp +void set_buffer_size(length_t buffer_size); +``` + +#### reset() + +清除所有 Rule 和事实。 + +```cpp +void reset(); +``` + +#### add() + +从文本添加 Rule 或事实。 + +```cpp +bool add(std::string_view text); +``` + +#### execute() + +执行一轮推理。 + +```cpp +length_t execute(const std::function& callback); +``` + +**参数：** + +- `callback`：对每个新推理调用的函数。返回 false 继续，返回 true 停止。 + +**返回值：** 生成的新推理数量。 + +--- + +## 辅助函数 + +`` 中的辅助函数。 + +### text_to_term() + +将文本解析为 Term 对象。 + +```cpp +std::unique_ptr text_to_term(const char* text, length_t length); +``` + +**参数：** + +- `text`：Term 的文本表示 +- `length`：生成的二进制 Term 的最大大小 + +**返回值：** 指向创建的 Term 的 unique_ptr，如果超过长度则返回 nullptr。 + +### term_to_text() + +将 Term 对象转换为文本。 + +```cpp +std::unique_ptr term_to_text(term_t* term, length_t length); +``` + +**参数：** + +- `term`：要转换的二进制 Term +- `length`：生成的文本的最大大小 + +**返回值：** 指向文本的 unique_ptr，如果超过长度则返回 nullptr。 + +### text_to_rule() + +将文本解析为 Rule 对象。 + +```cpp +std::unique_ptr text_to_rule(const char* text, length_t length); +``` + +**参数：** + +- `text`：Rule 的文本表示 +- `length`：生成的二进制 Rule 的最大大小 + +**返回值：** 指向创建的 Rule 的 unique_ptr，如果超过长度则返回 nullptr。 + +### rule_to_text() + +将 Rule 对象转换为文本。 + +```cpp +std::unique_ptr rule_to_text(rule_t* rule, length_t length); +``` + +**参数：** + +- `rule`：要转换的二进制 Rule +- `length`：生成的文本的最大大小 + +**返回值：** 指向文本的 unique_ptr，如果超过长度则返回 nullptr。 + +--- + +## 完整示例 + +这是一个演示 C++ API 的完整示例： + +```cpp +#include +#include +#include +#include +#include + +int main() { + const int buffer_size = 1000; + + // Create terms using utility functions + auto term = ds::text_to_term("(f `x `y)", buffer_size); + + std::cout << "Term: " << ds::term_to_text(term.get(), buffer_size).get() << std::endl; + + // Work with rules + auto fact = ds::text_to_rule("(parent john mary)", buffer_size); + auto rule = ds::text_to_rule("(father `X `Y)\n----------\n(parent `X `Y)\n", buffer_size); + + std::cout << "\nFact:\n" << ds::rule_to_text(fact.get(), buffer_size).get(); + std::cout << "Rule premises: " << rule->premises_count() << std::endl; + std::cout << "Rule conclusion: " << ds::term_to_text(rule->conclusion(), buffer_size).get() << std::endl; + + // Search engine + ds::search_t search(1000, 10000); + + // Add rules and facts + search.add("p q"); // p implies q + search.add("q r"); // q implies r + search.add("p"); // fact: p + + std::cout << "\nRunning inference:" << std::endl; + + // Execute search + auto target = ds::text_to_rule("r", buffer_size); + bool found = false; + + while (!found) { + auto count = search.execute([&](ds::rule_t* candidate) { + std::cout << " Derived: " << ds::rule_to_text(candidate, buffer_size).get(); + + // Check if this is our target + if (candidate->data_size() == target->data_size() && + memcmp(candidate->head(), target->head(), candidate->data_size()) == 0) { + found = true; + return true; // Stop + } + return false; // Continue + }); + + if (count == 0) { + std::cout << " (no more inferences)" << std::endl; + break; + } + } + + if (found) { + std::cout << "Target found!" << std::endl; + } + + return 0; +} +``` diff --git a/docs/zh/api/python.md b/docs/zh/api/python.md new file mode 100644 index 0000000..6ef902a --- /dev/null +++ b/docs/zh/api/python.md @@ -0,0 +1,547 @@ +# Python API 参考 + +本页记录了 `apyds` 包的 Python API。 + +```python +from apyds import ( + buffer_size, + scoped_buffer_size, + String, + Variable, + Item, + List, + Term, + Rule, + Search, +) +``` + +## buffer_size + +获取当前缓冲区大小，或设置新的缓冲区大小并返回之前的值。 + +```python +def buffer_size(size: int = 0) -> int +``` + +**参数：** + +- `size` (可选)：要设置的新缓冲区大小。如果为 0（默认值），则返回当前大小而不进行修改。 + +**返回值：** 之前的缓冲区大小值。 + +**示例：** + +```python +current_size = buffer_size() # Get current size +old_size = buffer_size(2048) # Set new size, returns old size +``` + +--- + + +## scoped_buffer_size + +用于临时更改缓冲区大小的上下文管理器。 + +```python +@contextmanager +def scoped_buffer_size(size: int = 0) +``` + +**参数：** + +- `size`：要设置的临时缓冲区大小。 + +**示例：** + +```python +with scoped_buffer_size(4096): + # Operations here use buffer size of 4096 + pass +# Buffer size is restored to previous value +``` + +--- + + +## String + +演绎系统字符串的包装类。 + +### 构造函数 + +```python +def __init__(self, value: String | str | bytes, size: int | None = None) +``` + +**参数：** + +- `value`：初始值（字符串、bytes 或另一个 String） +- `size` (可选)：内部存储的缓冲区容量 + +### 方法 + +#### __str__() + +将值转换为字符串表示形式。 + +```python +def __str__(self) -> str +``` + +#### data() + +获取值的二进制表示形式。 + +```python +def data(self) -> bytes +``` + +#### size() + +获取数据的大小（以字节为单位）。 + +```python +def size(self) -> int +``` + +**示例：** + +```python +str1 = String("hello") +str2 = String(str1.data()) # From binary +print(str1) # "hello" +``` + +--- + + +## Variable + +演绎系统中逻辑 Variable 的包装类。 + +### 构造函数 + +```python +def __init__(self, value: Variable | str | bytes, size: int | None = None) +``` + +**参数：** + +- `value`：初始值（以反引号开头的字符串、bytes 或另一个 Variable） +- `size` (可选)：内部存储的缓冲区容量 + +### 属性 + +#### name + +获取此 Variable 的名称（不带反引号前缀）。 + +```python +@property +def name(self) -> String +``` + +**示例：** + +```python +var1 = Variable("`X") +print(var1.name) # "X" +print(var1) # "`X" +``` + +--- + + +## Item + +演绎系统中 Item（常量/函子）的包装类。 + +### 构造函数 + +```python +def __init__(self, value: Item | str | bytes, size: int | None = None) +``` + +### 属性 + +#### name + +获取此 Item 的名称。 + +```python +@property +def name(self) -> String +``` + +**示例：** + +```python +item = Item("atom") +print(item.name) # "atom" +``` + +--- + + +## List + +演绎系统中 List 的包装类。 + +### 构造函数 + +```python +def __init__(self, value: List | str | bytes, size: int | None = None) +``` + +### 方法 + +#### __len__() + +获取 List 中的元素数量。 + +```python +def __len__(self) -> int +``` + +#### __getitem__() + +通过索引获取 List 中的元素。 + +```python +def __getitem__(self, index: int) -> Term +``` + +**示例：** + +```python +lst = List("(a b c)") +print(len(lst)) # 3 +print(lst[0]) # "a" +``` + +--- + + +## Term + +演绎系统中逻辑 Term 的包装类。一个 Term 可以是 Variable、Item 或 List。 + +### 构造函数 + +```python +def __init__(self, value: Term | str | bytes, size: int | None = None) +``` + +### 属性 + +#### term + +提取底层 Term 并将其作为具体类型返回。 + +```python +@property +def term(self) -> Variable | Item | List +``` + +### 方法 + +#### ground() + +使用字典将此 Term 具体化 (Ground)，用值替换 Variable。 + +```python +def ground(self, other: Term, scope: str | None = None) -> Term | None +``` + +**参数：** + +- `other`：表示字典的 Term（对列表） +- `scope` (可选)：用于 Variable 作用域的字符串 + +**返回值：** 具体化后的 Term，如果失败则返回 None。 + +**示例：** + +```python +a = Term("`a") +dict = Term("((`a b))") +result = a.ground(dict) +if result is not None: + print(result) # "b" +``` + +#### __matmul__() / match + +将两个 Term 进行合一，并返回合一结果作为字典。 + +```python +def __matmul__(self, other: Term) -> Term | None +``` + +**参数：** + +- `other`：要与此 Term 匹配的 Term + +**返回值：** 表示合一字典（元组列表）的 Term，如果匹配失败则返回 None。 + +**示例：** + +```python +a = Term("`a") +b = Term("b") +result = a @ b +if result is not None: + print(result) # "((1 2 `a b))" +``` + +#### rename() + +通过添加前缀和后缀重命名此 Term 中的所有 Variable。 + +```python +def rename(self, prefix_and_suffix: Term) -> Term | None +``` + +**参数：** + +- `prefix_and_suffix`: 格式为 `((prefix) (suffix))` 的 Term + +**返回值：** 重命名后的 Term，如果重命名失败则返回 None。 + +**示例：** + +```python +term = Term("`x") +spec = Term("((pre_) (_suf))") +result = term.rename(spec) +if result is not None: + print(result) # "`pre_x_suf" +``` + +--- + + +## Rule + +演绎系统中逻辑 Rule 的包装类。 + +### 构造函数 + +```python +def __init__(self, value: Rule | str | bytes, size: int | None = None) +``` + +### 属性 + +#### conclusion + +获取 Rule 的结论。 + +```python +@property +def conclusion(self) -> Term +``` + +### 方法 + +#### __len__() + +获取 Rule 中的前提数量。 + +```python +def __len__(self) -> int +``` + +#### __getitem__() + +通过索引获取前提 Term。 + +```python +def __getitem__(self, index: int) -> Term +``` + +#### ground() + +使用字典将此 Rule 具体化 (Ground)。 + +```python +def ground(self, other: Rule, scope: str | None = None) -> Rule | None +``` + +#### __matmul__() / match + +使用合一将此 Rule 与另一个 Rule 匹配。 + +```python +def __matmul__(self, other: Rule) -> Rule | None +``` + +**参数：** + +- `other`：要匹配的 Rule（必须是没有前提的事实） + +**返回值：** 匹配后的 Rule，如果匹配失败则返回 None。 + +**示例：** + +```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() + +重命名此 Rule 中的所有 Variable。 + +```python +def rename(self, prefix_and_suffix: Rule) -> Rule | None +``` + +--- + + +## Search + +演绎系统的搜索引擎。 + +### 构造函数 + +```python +def __init__(self, limit_size: int = 1000, buffer_size: int = 10000) +``` + +**参数：** + +- `limit_size` (可选)：用于存储 Rule/事实的缓冲区大小（默认值：1000） +- `buffer_size` (可选)：用于内部操作的缓冲区大小（默认值：10000） + +### 方法 + +#### set_limit_size() + +设置存储最终对象的缓冲区大小。 + +```python +def set_limit_size(self, limit_size: int) -> None +``` + +#### set_buffer_size() + +设置内部操作的缓冲区大小。 + +```python +def set_buffer_size(self, buffer_size: int) -> None +``` + +#### reset() + +重置搜索引擎，清除所有 Rule 和事实。 + +```python +def reset(self) -> None +``` + +#### add() + +向知识库添加 Rule 或事实。 + +```python +def add(self, text: str) -> bool +``` + +**返回值：** 如果添加成功则返回 True，否则返回 False。 + +#### execute() + +执行搜索引擎，并为每个推导出的 Rule 调用回调。 + +```python +def execute(self, callback: Callable[[Rule], bool]) -> int +``` + +**参数：** + +- `callback`：对每个候选 Rule 调用的函数。返回 False 继续，返回 True 停止。 + +**返回值：** 处理的 Rule 数量。 + +**示例：** + +```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) +``` + +--- + + +## 完整示例 + +这是一个演示大多数 API 的完整示例： + +```python +import apyds + +# Configure buffer size for operations +apyds.buffer_size(2048) + +# Create terms +var = apyds.Variable("`X") +item = apyds.Item("hello") +lst = apyds.List("(a b c)") +term = apyds.Term("(f `x `y)") + +print(f"Variable: {var}, name: {var.name}") +print(f"Item: {item}, name: {item.name}") +print(f"List: {lst}, length: {len(lst)}") +print(f"Term: {term}, type: {type(term.term)}") + +# Work with rules +fact = apyds.Rule("(parent john mary)") +rule = apyds.Rule("(father `X `Y)\n----------\n(parent `X `Y)\n") + +print(f"\nFact: {fact}") +print(f"Rule premises: {len(rule)}, conclusion: {rule.conclusion}") + +# Grounding +term_a = apyds.Term("`a") +dictionary = apyds.Term("((`a hello))") +grounded = term_a // dictionary +print(f"\nGrounding `a with ((` hello)): {grounded}") + +# Matching +mp = apyds.Rule("(`p -> `q)\n`p\n`q\n") +axiom = apyds.Rule("((A) -> B)") +matched = mp @ axiom +print(f"\nMatching modus ponens with (A -> B):\n{matched}") + +# Search engine +search = apyds.Search(1000, 10000) +search.add("p q") # p implies q +search.add("q r") # q implies r +search.add("p") # fact: p + +print("\nRunning inference:") +for i in range(3): + count = search.execute(lambda r: print(f" Derived: {r}") or False) + if count == 0: + break + +# Using context manager for buffer size +with apyds.scoped_buffer_size(4096): + big_term = apyds.Term("(a b c d e f g h i j)") + print(f"\nBig term: {big_term}") +``` \ No newline at end of file diff --git a/docs/zh/api/typescript.md b/docs/zh/api/typescript.md new file mode 100644 index 0000000..40965bb --- /dev/null +++ b/docs/zh/api/typescript.md @@ -0,0 +1,553 @@ +# TypeScript API 参考 + +本页记录了 `atsds` 包的 TypeScript API。文档由 TypeScript 源代码生成。 + +```typescript +import { + buffer_size, + String_, + Variable, + Item, + List, + Term, + Rule, + Search +} from "atsds"; +``` + +## buffer_size + +获取当前缓冲区大小，或设置新的缓冲区大小并返回之前的值。 + +```typescript +function buffer_size(size?: number): number; +``` + +**参数：** + +- `size` (可选)：要设置的新缓冲区大小。如果为 0 或省略，则返回当前大小而不进行修改。 + +**返回值：** 之前的缓冲区大小值。 + +**示例：** + +```typescript +const currentSize = buffer_size(); // Get current size +const oldSize = buffer_size(2048); // Set new size, returns old size +``` + +--- + +## String_ + +演绎系统字符串的包装类。 + +### 构造函数 + +```typescript +constructor(value: string | Buffer | String_, size?: number) +``` + +**参数：** + +- `value`：初始值（字符串、Buffer 或另一个 String_） +- `size` (可选)：内部存储的缓冲区容量 + +### 方法 + +#### toString() + +将值转换为字符串表示形式。 + +```typescript +topString(): string +``` + +#### data() + +获取值的二进制表示形式。 + +```typescript +data(): Buffer +``` + +#### size() + +获取数据的大小（以字节为单位）。 + +```typescript +size(): number +``` + +#### copy() + +创建此实例的深拷贝。 + +```typescript +copy(): String_ +``` + +#### key() + +获取用于相等性比较的键表示形式。 + +```typescript +key(): string +``` + +**示例：** + +```typescript +const str1 = new String_("hello"); +const str2 = new String_(str1.data()); +console.log(str1.toString()); // "hello" +``` + +--- + +## Variable + +演绎系统中逻辑 Variable 的包装类。 + +### 构造函数 + +```typescript +constructor(value: string | Buffer | Variable, size?: number) +``` + +**参数：** + +- `value`：初始值（以反引号开头的字符串、Buffer 或另一个 Variable） +- `size` (可选)：内部存储的缓冲区容量 + +### 方法 + +继承自 `String_` 的所有方法，加上： + +#### name() + +获取此 Variable 的名称（不带反引号前缀）。 + +```typescript +name(): String_ +``` + +**示例：** + +```typescript +const var1 = new Variable("`X"); +console.log(var1.name().toString()); // "X" +console.log(var1.toString()); // "`X" +``` + +--- + +## Item + +演绎系统中 Item（常量/函子）的包装类。 + +### 构造函数 + +```typescript +constructor(value: string | Buffer | Item, size?: number) +``` + +### 方法 + +继承自 `String_` 的所有方法，加上： + +#### name() + +获取此 Item 的名称。 + +```typescript +name(): String_ +``` + +**示例：** + +```typescript +const item = new Item("atom"); +console.log(item.name().toString()); // "atom" +``` + +--- + +## List + +演绎系统中 List 的包装类。 + +### 构造函数 + +```typescript +constructor(value: string | Buffer | List, size?: number) +``` + +### 方法 + +继承自 `String_` 的所有方法，加上： + +#### length() + +获取 List 中的元素数量。 + +```typescript +length(): number +``` + +#### getitem() + +通过索引获取 List 中的元素。 + +```typescript +getitem(index: number): Term +``` + +**示例：** + +```typescript +const list = new List("(a b c)"); +console.log(list.length()); // 3 +console.log(list.getitem(0).toString()); // "a" +``` + +--- + +## Term + +演绎系统中逻辑 Term 的包装类。一个 Term 可以是 Variable、Item 或 List。 + +### 构造函数 + +```typescript +constructor(value: string | Buffer | Term, size?: number) +``` + +### 方法 + +继承自 `String_` 的所有方法，加上： + +#### term() + +提取底层 Term 并将其作为具体类型返回。 + +```typescript +term(): Variable | Item | List +``` + +#### ground() + +使用字典将此 Term 具体化 (Ground)，用值替换 Variable。 + +```typescript +ground(other: Term, scope?: string): Term | null +``` + +**参数：** + +- `other`：表示字典的 Term（对列表） +- `scope` (可选)：用于 Variable 作用域的字符串 + +**返回值：** 具体化后的 Term，如果失败则返回 null。 + +**示例：** + +```typescript +const a = new Term("`a"); +const dict = new Term("((`a b))"); +const result = a.ground(dict); +if (result !== null) { + console.log(result.toString()); // "b" +} +``` + +#### match() + +将两个 Term 进行合一，并返回合一结果作为字典。 + +```typescript +match(other: Term): Term | null +``` + +**参数：** + +- `other`：要与此 Term 匹配的 Term + +**返回值：** 表示合一字典（元组列表）的 Term，如果匹配失败则返回 null。 + +**示例：** + +```typescript +const a = new Term("`a"); +const b = new Term("b"); +const result = a.match(b); +if (result !== null) { + console.log(result.toString()); // "((1 2 `a b))" +} +``` + +#### rename() + +通过添加前缀和后缀重命名此 Term 中的所有 Variable。 + +```typescript +rename(prefix_and_suffix: Term): Term | null +``` + +**参数：** + +- `prefix_and_suffix`：格式为 `((prefix) (suffix))` 的 Term + +**返回值：** 重命名后的 Term，如果重命名失败则返回 null。 + +**示例：** + +```typescript +const term = new Term("`x"); +const spec = new Term("((pre_) (_suf))"); +const result = term.rename(spec); +if (result !== null) { + console.log(result.toString()); // "`pre_x_suf" +} +``` + +--- + +## Rule + +演绎系统中逻辑 Rule 的包装类。 + +### 构造函数 + +```typescript +constructor(value: string | Buffer | Rule, size?: number) +``` + +### 方法 + +继承自 `String_` 的所有方法，加上： + +#### length() + +获取 Rule 中的前提数量。 + +```typescript +length(): number +``` + +#### getitem() + +通过索引获取前提 Term。 + +```typescript +getitem(index: number): Term +``` + +#### conclusion() + +获取 Rule 的结论。 + +```typescript +conclusion(): Term +``` + +#### ground() + +使用字典将此 Rule 具体化 (Ground)。 + +```typescript +ground(other: Rule, scope?: string): Rule | null +``` + +#### match() + +使用合一将此 Rule 与另一个 Rule 匹配。 + +```typescript +match(other: Rule): Rule | null +``` + +**参数：** + +- `other`：要匹配的 Rule（必须是没有前提的事实） + +**返回值：** 匹配后的 Rule，如果匹配失败则返回 null。 + +**示例：** + +```typescript +const mp = new Rule("(`p -> `q)\n`p\n`q\n"); +const pq = new Rule("((! (! `x)) -> `x)"); +const result = mp.match(pq); +if (result !== null) { + console.log(result.toString()); + // "(! (! `x))\n----------\n`x\n" +} +``` + +#### rename() + +重命名此 Rule 中的所有 Variable。 + +```typescript +rename(prefix_and_suffix: Rule): Rule | null +``` + +--- + +## Search + +演绎系统的搜索引擎。 + +### 构造函数 + +```typescript +constructor(limit_size?: number, buffer_size?: number) +``` + +**参数：** + +- `limit_size` (可选)：用于存储 Rule/事实的缓冲区大小（默认值：1000） +- `buffer_size` (可选)：用于内部操作的缓冲区大小（默认值：10000） + +### 方法 + +#### set_limit_size() + +设置存储最终对象的缓冲区大小。 + +```typescript +set_limit_size(limit_size: number): void +``` + +#### set_buffer_size() + +设置内部操作的缓冲区大小。 + +```typescript +set_buffer_size(buffer_size: number): void +``` + +#### reset() + +重置搜索引擎，清除所有 Rule 和事实。 + +```typescript +reset(): void +``` + +#### add() + +向知识库添加 Rule 或事实。 + +```typescript +add(text: string): boolean +``` + +**返回值：** 如果添加成功则返回 true，否则返回 false。 + +#### execute() + +执行搜索引擎，并为每个推导出的 Rule 调用回调。 + +```typescript +execute(callback: (candidate: Rule) => boolean): number +``` + +**参数：** + +- `callback`：对每个候选 Rule 调用的函数。返回 false 继续，返回 true 停止。 + +**返回值：** 处理的 Rule 数量。 + +**示例：** + +```typescript +const search = new Search(1000, 10000); +search.add("p q"); // p implies q +search.add("q r"); // q implies r +search.add("p"); // fact: p + +search.execute((candidate) => { + console.log(candidate.toString()); + return false; // Continue searching +}); +``` + +--- + +## 完整示例 + +这是一个演示大多数 TypeScript API 的完整示例： + +```typescript +import { + buffer_size, + String_, + Variable, + Item, + List, + Term, + Rule, + Search +} from "atsds"; + +// Configure buffer size +buffer_size(2048); + +// Create terms +const varX = new Variable("`X"); +const item = new Item("hello"); +const lst = new List("(a b c)"); +const term = new Term("(f `x `y)"); + +console.log(`Variable: ${varX.toString()}, name: ${varX.name().toString()}`); +console.log(`Item: ${item.toString()}, name: ${item.name().toString()}`); +console.log(`List: ${lst.toString()}, length: ${lst.length()}`); +console.log(`Term: ${term.toString()}`); + +// Work with rules +const fact = new Rule("(parent john mary)"); +const rule = new Rule("(father `X `Y)\n----------\n(parent `X `Y)\n"); + +console.log(`\nFact: ${fact.toString()}`); +console.log(`Rule premises: ${rule.length()}, conclusion: ${rule.conclusion().toString()}`); + +// Grounding +const termA = new Term("`a"); +const dictionary = new Term("((`a hello))"); +const grounded = termA.ground(dictionary); +if (grounded) { + console.log(`\nGrounding + with (( +)): ${grounded.toString()}`); +} + +// Matching +const mp = new Rule("(`p -> `q)\n`p\n`q\n"); +const axiom = new Rule("((A) -> B)"); +const matched = mp.match(axiom); +if (matched) { + console.log(`\nMatching modus ponens with (A -> B):\n${matched.toString()}`); +} + +// Search engine +const search = new Search(1000, 10000); +search.add("p q"); // p implies q +search.add("q r"); // q implies r +search.add("p"); // fact: p + +console.log("\nRunning inference:"); +for (let i = 0; i < 3; i++) { + const count = search.execute((r) => { + console.log(` Derived: ${r.toString()}`); + return false; + }); + if (count === 0) break; +} + +// Copying and comparison +const rule1 = new Rule("(a b c)"); +const rule2 = rule1.copy(); +console.log(`\nRule comparison: ${rule1.key() === rule2.key()}`); // true +``` diff --git a/docs/zh/concepts/rules.md b/docs/zh/concepts/rules.md new file mode 100644 index 0000000..996632b --- /dev/null +++ b/docs/zh/concepts/rules.md @@ -0,0 +1,360 @@ +# Rule + +Rule 是 DS 中表示逻辑推理的核心机制。本页解释了 Rule 的工作原理以及如何使用它们。 + +## Rule 结构 + +一条 Rule 由以下部分组成： + +- **前提**：零个或多个条件（横线上方） +- **结论**：当所有前提都满足时的结果（横线下方） + +### 文本表示 + +Rule 的前提和结论由破折号分隔（至少四个破折号）： + +``` +premise1 +premise2 +---------- +conclusion +``` + +**事实 (Fact)** 是没有前提的 Rule： + +``` +(parent john mary) +``` + +或者显式表示为： + +``` +---------- +(parent john mary) +``` + +::: tip Rule 格式详情 +- 前提之间用换行符分隔 +- 分隔线必须包含至少 4 个破折号 (`----`) 在前提和结论之间 +- 前提和结论周围的空白会被修剪 +- 没有前提的 Rule 是事实 + +::: +### 紧凑 Rule 格式 + +对于有多个前提的 Rule，可以使用单行空格分隔的 Term： + +``` +(`P -> `Q) `P `Q +``` + +这等价于： + +``` +(`P -> `Q) +`P +---------- +`Q +``` + +最后一个 Term 是结论，之前的所有 Term 都是前提。 + +### 示例 + +**肯定前件 (Modus Ponens)** (如果 P 蕴含 Q 且 P 为真，则 Q 为真)： + +``` +(`P -> `Q) +`P +---------- +`Q +``` + +**家庭关系** (如果 X 是 Y 的父亲，则 X 是 Y 的父母)： + +``` +(father `X `Y) +---------- +(parent `X `Y) +``` + +## 创建 Rule + +::: code-group +```typescript [TypeScript] +import { Rule } from "atsds"; + +// Create a fact +const fact = new Rule("(parent john mary)"); + +// Create a rule with premises +const rule = new Rule("(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) +``` +```cpp [C++] +#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 操作 + +### Grounding + +Grounding 将 Rule 中的 Variable 替换为字典中的值。 + +::: code-group +```typescript [TypeScript] +import { Rule } from "atsds"; + +// Create a rule with variables +const rule = new Rule("`a"); + +// Create a dictionary +const dictionary = new Rule("((`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 +``` +```cpp [C++] +#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 将 Rule 的第一个前提与一个事实合一，产生一个少了一个前提的新 Rule。 + +::: code-group +```typescript [TypeScript] +import { Rule } from "atsds"; + +// Modus ponens rule +const mp = new Rule("(`p -> `q)\n`p\n`q\n"); + +// Double negation elimination axiom +const axiom = new Rule("((! (! `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 +``` +```cpp [C++] +#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 为 Rule 中的所有 Variable 添加前缀和/或后缀。 + +::: code-group +```typescript [TypeScript] +import { Rule } from "atsds"; + +// Create a rule +const rule = new Rule("`x"); + +// Rename with prefix and suffix +const spec = new Rule("((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 +``` +```cpp [C++] +#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 比较 + +Rule 可以比较是否相等。如果两条 Rule 具有相同的二进制表示，则它们是相等的。 + +::: code-group +```typescript [TypeScript] +import { Rule } from "atsds"; + +const rule1 = new Rule("(a b c)"); +const rule2 = new Rule("(a b c)"); +const rule3 = new Rule("(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 +``` +```cpp [C++] +#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; +} +``` +::: + +``` \ No newline at end of file diff --git a/docs/zh/concepts/search.md b/docs/zh/concepts/search.md new file mode 100644 index 0000000..2bdf12b --- /dev/null +++ b/docs/zh/concepts/search.md @@ -0,0 +1,268 @@ +# 搜索引擎 + +搜索引擎是 DS 中的核心推理机制。它管理 Rule 和事实的知识库，并通过将 Rule 与事实进行匹配来执行逻辑推理。 + +## 概览 + +搜索引擎： + +1. 维护 Rule 和事实的集合 +2. 迭代地应用 Rule 以生成新的事实 +3. 通过回调通知您每个新推理 +4. 自动防止重复推理 + +::: tip 工作原理 +搜索引擎使用前向链 (forward-chaining) 推理方法： + +1. 当您调用 `execute()` 时，引擎尝试将每个 Rule 的第一个前提与现有事实进行匹配 +2. 找到匹配项时，Rule 中的 Variable 被替换，并创建一个新 Rule（前提少一个） +3. 如果新 Rule 没有前提，它将成为一个新的事实 +4. 对每个新派生的 Rule 调用回调 +5. 自动过滤掉重复的 Rule + +::: +## 创建搜索引擎 + +::: code-group +```typescript [TypeScript] +import { Search } from "atsds"; + +// Create with default sizes +const search = new Search(); + +// Create with custom sizes +const search2 = new Search(1000, 10000); +``` +```python [Python] +import apyds + +# Create with default sizes +search = apyds.Search() + +# Create with custom sizes +search = apyds.Search(limit_size=1000, buffer_size=10000) +``` +```cpp [C++] +#include + +// Create search engine +ds::search_t search(1000, 10000); +``` +::: + +### 参数 + +- **limit_size**：每个存储的 Rule/事实的最大大小（字节）（默认值：1000）。大于此大小的 Rule 或事实将被拒绝。 +- **buffer_size**：中间操作的内部缓冲区大小（默认值：10000）。如果您处理复杂的 Rule，请增加此值。 + +## 添加 Rule 和事实 + +使用 `add()` 方法将 Rule 和事实添加到知识库中。 + +::: code-group +```typescript [TypeScript] +import { Search } from "atsds"; + +const search = new 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"); +``` +```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") +``` +```cpp [C++] +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"); +``` +::: + +## 执行搜索 + +`execute()` 方法执行一轮推理。它将所有 Rule 与所有事实进行匹配，并生成新的结论。 + +::: code-group +```typescript [TypeScript] +import { Search } from "atsds"; + +const search = new Search(); +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`); +``` +```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") +``` +```cpp [C++] +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); +``` +::: + +### 回调函数 + +回调接收每个新推断出的 Rule，并且应该返回： + +- `False` (Python) / `false` (TypeScript/C++): 继续搜索 +- `True` (Python) / `true` (TypeScript/C++): 停止搜索 + +## 搜索目标 + +要搜索直到找到特定目标： + +::: code-group +```typescript [TypeScript] +import { Rule, Search } from "atsds"; + +const search = new Search(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("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; +} +``` +```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 +``` +::: + +## 配置方法 + +### 设置 Limit Size + +控制每个存储的 Rule/事实的最大大小： + +::: code-group +```typescript [TypeScript] +search.set_limit_size(2000); +``` +```python [Python] +search.set_limit_size(2000) +``` +```cpp [C++] +search.set_limit_size(2000); +``` +::: + +### 设置 Buffer Size + +控制操作的内部缓冲区大小： + +::: code-group +```typescript [TypeScript] +search.set_buffer_size(20000); +``` +```python [Python] +search.set_buffer_size(20000) +``` +```cpp [C++] +search.set_buffer_size(20000); +``` +::: + +### 重置 + +清除所有 Rule 和事实： + +::: code-group +```typescript [TypeScript] +search.reset(); +``` +```python [Python] +search.reset() +``` +```cpp [C++] +search.reset(); +``` +::: + +## 性能考虑 + +1. **Buffer Size**：更大的缓冲区允许更复杂的中间结果，但占用更多内存 +2. **Limit Size**：限制最大 Rule/事实的复杂度 - 太小可能会拒绝有效的 Rule +3. **迭代执行**：循环调用 `execute()` 以继续推理直到收敛 +4. **提前终止**：从回调返回 `true` 以在找到目标后立即停止 +5. **去重**：引擎自动对事实进行去重，避免冗余计算 diff --git a/docs/zh/concepts/terms.md b/docs/zh/concepts/terms.md new file mode 100644 index 0000000..28b9d43 --- /dev/null +++ b/docs/zh/concepts/terms.md @@ -0,0 +1,348 @@ +# Term + +Term 是演绎系统的基本构建块。本页解释了不同类型的 Term 以及如何使用它们。 + +## Term 类型 + +演绎系统支持三种基本类型的 Term： + +### Variable + +Variable 是占位符，可以在推理过程中与其他 Term 进行合一。它们以反引号 (`` ` ``) 为前缀。 + +``` +`X +`variable_name +`P +`Q +``` + +Variable 用于在 Rule 中表示任何可以在合一期间匹配的 Term。在推理过程中，Variable 可以通过合一绑定到特定的 Term。 + +::: tip Variable 命名 +Variable 名称可以包含除反引号、空格和括号之外的任何字符。按照惯例，单个大写字母如 `` `X``, `` `P``, `` `Q`` 常用于简单的逻辑，而描述性名称如 `` `person`` 或 `` `result`` 则用于提高复杂 Rule 的可读性。 + +::: +### Item + +Item 表示常量或函子。它们是没有特殊前缀的原子值。 + +``` +hello +atom +father +! +-> +``` + +Item 可以表示： + +- **常量**：原子值，如 `john`, `mary`, `42` +- **函子**：组合其他 Term 的符号，如 `father`, `->`, `!` +- **操作符**：用于逻辑表达式的特殊符号，如表示蕴含的 `->` 或表示否定的 `!` + +::: tip Item 字符 +Item 可以包含除反引号、空格和括号之外的任何字符。特殊符号如 `->`, `!`, `<-`, `&&`, `||` 常被用作逻辑操作符。 + +::: +### List + +List 是圆括号中 Term 的有序序列。它们可以包含 Variable、Item 和嵌套 List 的任何组合。 + +``` +(a b c) +(father john mary) +(-> P Q) +(! (! X)) +``` + +List 是在演绎系统中构建复杂结构的主要方式。它们可以表示： + +- **关系**：`(father john mary)` - "John 是 Mary 的父亲" +- **逻辑表达式**：`(P -> Q)` - "P 蕴含 Q" +- **嵌套结构**：`(! (! X))` - "非非 X" (双重否定) +- **数据集合**：`(1 2 3 4 5)` - 数字列表 + +::: tip List 嵌套 +List 可以嵌套到任意深度： +``` +((a b) (c d) (e f)) +(if (> `x 0) (positive `x) (non-positive `x)) +``` + +::: +## 创建 Term + +::: code-group +```typescript [TypeScript] +import { Variable, Item, List, Term } from "atsds"; + +// Create a variable +const var1 = new Variable("`X"); +console.log(`Variable name: ${var1.name().toString()}`); // X + +// Create an item +const item = new Item("hello"); +console.log(`Item name: ${item.name().toString()}`); // hello + +// Create a list +const lst = new List("(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("(f `x)"); +// Access the underlying type +const inner = term.term(); // Returns a List +``` +```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 +``` +```cpp [C++] +#include +#include +#include + +int main() { + // Create a generic term + auto term = ds::text_to_term("(f `x)", 1000); + // Access the underlying type + auto list = term->list(); + auto item = list->term(0)->item(); + auto variable = list->term(1)->variable(); + return 0; +} +``` +::: + +## Term 操作 + +### Grounding + +Grounding 将 Term 中的 Variable 替换为字典中的值。字典是一个键值对列表，其中每个键是一个 Variable，每个值是它的替换项。 + +::: code-group +```typescript [TypeScript] +import { Term } from "atsds"; + +// Create a term with a variable +const term = new Term("`a"); + +// Create a dictionary for substitution +const dictionary = new Term("((`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 +``` +```cpp [C++] +#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; +} +``` +::: + +### Matching + +Matching 将两个 Term 进行合一，并返回一个 Variable 绑定字典。该字典包含使两个 Term 相等所需的替换。 + +::: code-group +```typescript [TypeScript] +import { Term } from "atsds"; + +// Match a variable with a value +const a = new Term("`a"); +const b = new Term("value"); + +const result = a.match(b); +if (result !== null) { + console.log(result.toString()); // ((1 2 `a value)) +} + +// Match complex terms +const term1 = new Term("(f b a)"); +const term2 = new Term("(f `x a)"); + +const dict = term1.match(term2); +if (dict !== null) { + console.log(dict.toString()); // ((2 1 `x b)) +} +``` +```python [Python] +import apyds + +# Match a variable with a value +a = apyds.Term("`a") +b = apyds.Term("value") + +result = a @ b # Uses @ operator +print(result) # ((1 2 `a value)) + +# Match complex terms +term1 = apyds.Term("(f b a)") +term2 = apyds.Term("(f `x a)") + +dict_result = term1 @ term2 +print(dict_result) # ((2 1 `x b)) +``` +```cpp [C++] +#include +#include +#include + +int main() { + // Match a variable with a value + auto a = ds::text_to_term("`a", 1000); + auto b = ds::text_to_term("value", 1000); + + // Match the terms + std::byte buffer[1000]; + auto result = reinterpret_cast(buffer); + result->match(a.get(), b.get(), "1", "2", buffer + 1000); + + std::cout << ds::term_to_text(result, 1000).get() << std::endl; // ((1 2 `a value)) + + return 0; +} +``` +::: + +### Renaming + +Renaming 为 Term 中的所有 Variable 添加前缀和/或后缀。这对于避免合一过程中的 Variable 名称冲突非常有用。 + +::: code-group +```typescript [TypeScript] +import { Term } from "atsds"; + +// Create a term with a variable +const term = new Term("`x"); + +// Create prefix and suffix specification +const spec = new Term("((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 +``` +```cpp [C++] +#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; +} +``` +::: + +## 缓冲区大小 + +Grounding 和 Renaming 等操作在 TypeScript/Javascript 和 Python 中需要缓冲区空间来存储中间结果。您可以使用缓冲区大小函数来控制它。 + +::: code-group +```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 +``` +::: diff --git a/docs/zh/examples/basic.md b/docs/zh/examples/basic.md new file mode 100644 index 0000000..9ee92d5 --- /dev/null +++ b/docs/zh/examples/basic.md @@ -0,0 +1,160 @@ +# 基础示例 + +本节包含演示各种语言中使用 DS 演绎系统的示例。 + +## 命题逻辑推理 + +这个经典示例演示了使用命题逻辑公理进行的双重否定消除： + +- **肯定前件 (Modus Ponens)**：如果 P 蕴含 Q，且 P 为真，则 Q 为真 +- **公理 1**：P → (Q → P) +- **公理 2**：(P → (Q → R)) → ((P → Q) → (P → R)) +- **公理 3**：(¬P → ¬Q) → (Q → P) + +给定前提 ¬¬X (X 的双重否定)，我们可以推导出 X。 + +::: code-group +```typescript [TypeScript] +import { Rule, Search } from "atsds"; + +// Create a search engine +const search = new 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) +const target = new Rule("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; +} +``` +```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 +``` +```cpp [C++] +#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; +} +``` +::: + +## 运行示例 + +示例文件位于仓库的 `examples/` 目录下： + +- `examples/main.py` - Python 示例 +- `examples/main.mjs` - TypeScript 示例 +- `examples/main.cc` - C++ 示例 + +### TypeScript + +```bash +npm install atsds +node examples/main.mjs +``` + +### Python + +```bash +pip install apyds +python examples/main.py +``` + +### C++ + +```bash +cmake -B build +cmake --build build +./build/main +``` diff --git a/docs/zh/examples/sudoku.md b/docs/zh/examples/sudoku.md new file mode 100644 index 0000000..690cf27 --- /dev/null +++ b/docs/zh/examples/sudoku.md @@ -0,0 +1,21 @@ +# 数独 + +这个示例演示了一个由 DS 演绎系统驱动的**数独求解器**。求解器使用逻辑 Rule 基于标准数独约束来推导单元格的值： + +- **行约束**：每一行必须恰好包含一次数字 1-9 +- **列约束**：每一列必须恰好包含一次数字 1-9 +- **宫约束**：每个 3×3 宫必须恰好包含一次数字 1-9 + +## 工作原理 + +数独求解器将数独规则编码为 DS 系统中的逻辑推理 Rule。当您点击“Solve”时，搜索引擎会迭代应用这些 Rule 来推导新的单元格值，直到谜题完成。您也可以点击“Update”来执行单次推理迭代，并在日志中观察逐步求解过程。 + +## 交互式演示 + + + + + + diff --git a/docs/zh/getting-started/installation.md b/docs/zh/getting-started/installation.md new file mode 100644 index 0000000..05026bb --- /dev/null +++ b/docs/zh/getting-started/installation.md @@ -0,0 +1,199 @@ +# 安装 + +DS 可以为 TypeScript/JavaScript、Python 安装，或直接作为 C++ 库使用。 + +## TypeScript/JavaScript + +TypeScript/JavaScript 包 `atsds` 通过 WebAssembly 封装了 C++ 核心。 + +```bash +npm install atsds +``` + +该包包含： + +- WebAssembly 二进制文件 (`.wasm`) +- TypeScript 类型定义 (`.d.mts`) +- ES 模块支持 + +### 要求 + +- Node.js 20+ 或支持 WebAssembly 的现代浏览器 + +### 浏览器用法 + +该包适用于支持 WebAssembly 的浏览器： + +```html + +``` + +## Python + +Python 包 `apyds` 通过 pybind11 封装了 C++ 核心。 + +```bash +pip install apyds +``` + +### 要求 + +- Python 3.11-3.14 +- 已为常见平台（Linux, macOS, Windows）提供预编译的 Wheel 包 + +### 虚拟环境（推荐） + +推荐使用虚拟环境： + +```bash +python -m venv venv +source venv/bin/activate # On Windows: venv\Scripts\activate +pip install apyds +``` + +### 开发安装 + +要从源码安装并包含开发依赖： + +```bash +git clone https://github.com/USTC-KnowledgeComputingLab/ds.git +cd ds +uv sync --extra dev +``` + +## C++ + +C++ 库是核心实现。Python 和 TypeScript 绑定都建立在其之上。 + +### 先决条件 + +- 兼容 C++20 的编译器 (GCC 10+, Clang 10+, MSVC 2019+) +- CMake 3.30+ + +### 使用 vcpkg + +克隆仓库并使用覆盖端口 (overlay port)： + +```bash +git clone https://github.com/USTC-KnowledgeComputingLab/ds.git +vcpkg install ds --overlay-ports=./ds/ports +``` + +添加到你的 `vcpkg.json`： + +```json +{ + "dependencies": ["ds"] +} +``` + +在你的 CMakeLists.txt 中： + +```cmake +find_package(ds CONFIG REQUIRED) +target_link_libraries(your_target PRIVATE ds::ds) +``` + +### 从源码构建 + +```bash +git clone https://github.com/USTC-KnowledgeComputingLab/ds.git +cd ds +cmake -B build +cmake --build build +``` + +### 在你的项目中使用 + +在你的 C++ 项目中包含 `include/ds/` 下的头文件： + +```cpp +#include +#include +``` + +链接构建生成的 `ds` 静态库。 + +## 构建所有组件 + +要从源码构建所有语言绑定： + +### TypeScript/JavaScript (需要 Emscripten) + +```bash +# Install Emscripten SDK first +# https://emscripten.org/docs/getting_started/downloads.html + +npm install +npm run build +``` + +### Python + +```bash +uv sync --extra dev +``` + +### C++ + +```bash +cmake -B build +cmake --build build +``` + +## 运行测试 + +安装后，你可以通过运行测试来验证一切正常： + +### TypeScript/JavaScript 测试 + +```bash +npm test +``` + +### Python 测试 + +```bash +uv run pytest +``` + +### C++ 测试 + +```bash +cd build +ctest +``` + +## 验证安装 + +::: code-group +```typescript [TypeScript] +import { Term } from "atsds"; + +const term = new Term("(hello world)"); +console.log(term.toString()); +// Output: (hello world) +``` +```python [Python] +import apyds + +term = apyds.Term("(hello world)") +print(term) # (hello world) +``` +```cpp [C++] +#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/zh/getting-started/quickstart.md b/docs/zh/getting-started/quickstart.md new file mode 100644 index 0000000..48d711f --- /dev/null +++ b/docs/zh/getting-started/quickstart.md @@ -0,0 +1,216 @@ +# 快速开始 + +本指南将帮助您使用偏好的语言开始使用 DS。 + +## 创建 Term + +Term 是演绎系统的基本构建块。一个 Term 可以是： + +- **Variable**：以反引号为前缀，例如 `` `X``, `` `P`` +- **Item**：常量或函子，例如 `a`, `father`, `!` +- **List**：圆括号中的有序序列，例如 `(a b c)` + +::: code-group +```typescript [TypeScript] +import { Variable, Item, List, Term } from "atsds"; + +// Create different types of terms +const var1 = new Variable("`X"); +const item = new Item("hello"); +const lst = new List("(a b c)"); +const term = new Term("(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) +``` +```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) +``` +```cpp [C++] +#include +#include +#include + +int main() { + auto term = ds::text_to_term("(f `x a)", 1000); + std::cout << "Term: " << ds::term_to_text(term.get(), 1000).get() << std::endl; + return 0; +} +``` +::: + +## 创建 Rule + +Rule 表示逻辑推理步骤。一条 Rule 包含前提（条件）和结论。 + +::: code-group +```typescript [TypeScript] +import { Rule } from "atsds"; + +// A fact (rule with no premises) +const fact = new Rule("(parent john mary)"); +console.log(`Fact: ${fact.toString()}`); + +// A rule with premises +const rule = new Rule("(father `X `Y)\n----------\n(parent `X `Y)\n"); +console.log(`Rule premises: ${rule.length()}`); +console.log(`Rule conclusion: ${rule.conclusion().toString()}`); +``` +```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}") +``` +```cpp [C++] +#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 << "Rule premises: " << rule->premises_count() << std::endl; + std::cout << "Rule conclusion: " << ds::term_to_text(fact->conclusion(), 1000).get() << std::endl; + return 0; +} +``` +::: + +## 使用搜索引擎 + +搜索引擎通过将 Rule 与事实进行匹配来执行逻辑推理。 + +::: code-group +```typescript [TypeScript] +import { Rule, Search } from "atsds"; + +// Create search engine +const search = new 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 +const target = new Rule("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; +} +``` +```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 +``` +```cpp [C++] +#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; +} +``` +::: diff --git a/docs/zh/index.md b/docs/zh/index.md new file mode 100644 index 0000000..417dfa7 --- /dev/null +++ b/docs/zh/index.md @@ -0,0 +1,70 @@ +--- +layout: home + +hero: + name: "DS" + text: "一个演绎系统" + tagline: 一个用于逻辑推理的演绎系统，使用 C++ 实现，并提供 Python 和 TypeScript/JavaScript 的绑定 + actions: + - theme: brand + text: 快速开始 + link: /zh/getting-started/quickstart + - theme: alt + text: 在 GitHub 上查看 + link: https://github.com/USTC-KnowledgeComputingLab/ds + +features: + - title: 多语言支持 + details: 在 C++、Python 或 TypeScript/JavaScript 中无缝使用同一个演绎系统。 + - title: WebAssembly 性能 + details: 通过 Emscripten 在浏览器或 Node.js 中运行高性能演绎系统。 + - title: 丰富的逻辑 Term + details: 对 Variable、Item 和嵌套 List 的全面支持。 + - title: 基于 Rule 的推理 + details: 用于定义 Rule 和事实以执行复杂逻辑推演的灵活框架。 + - title: 合一引擎 + details: 强大的内置机制，用于 Term 合一和 Rule 匹配。 + - title: 自动搜索 + details: 内置搜索引擎，用于迭代推理。 +--- + +## 支持的语言 + +::: code-group +```typescript [TypeScript] +import { Term } from "atsds"; + +const term = new Term("(hello world)"); +console.log(term.toString()); +// Output: (hello world) +``` +```python [Python] +import apyds + +term = apyds.Term("(hello world)") +print(term) # (hello world) +``` +```cpp [C++] +#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; +} +``` +::: + +## 快速链接 + +- **[安装](getting-started/installation.md)** - 为您偏好的语言安装 DS +- **[快速开始](getting-started/quickstart.md)** - 在几分钟内启动并运行 +- **[核心概念](concepts/terms.md)** - 了解 Term、Rule 和推理 +- **[API 参考](api/typescript.md)** - 完整的 API 文档 +- **[示例](examples/basic.md)** - 可运行的代码示例 + +## 许可证 + +本项目采用 GNU 通用公共许可证 v3.0 或更高版本授权。 diff --git a/docs/zh/support-packages/bnf.md b/docs/zh/support-packages/bnf.md new file mode 100644 index 0000000..4eae40e --- /dev/null +++ b/docs/zh/support-packages/bnf.md @@ -0,0 +1,117 @@ +# BNF 支持包 + +BNF 支持包提供了 DS 两种语法格式之间的双向转换： + +- **Ds**：DS 内部使用的 S-表达式（类 Lisp）语法 +- **Dsp**：传统的、带有中缀操作符的人类可读语法 + +该包允许您使用更自然、更数学化的符号编写逻辑 Rule，并将其转换为 DS 内部格式，反之亦然。 + +## 安装 + +::: code-group +```bash [TypeScript] +npm install atsds-bnf +``` +```bash [Python] +pip install apyds-bnf +``` +::: + + 需要 Python 3.11-3.14。 + +## 用法 + +::: code-group +```javascript [TypeScript] +import { parse, unparse } from "atsds-bnf"; + +// Parse: Convert from readable Dsp to DS format +const dsp_input = "a, b => c"; +const ds_output = parse(dsp_input); +console.log(ds_output); +// Output: +// a +// b +// ---- +// c + +// Unparse: Convert from DS format to readable Dsp +const ds_input = "a\nb\n----\nc\n"; +const dsp_output = unparse(ds_input); +console.log(dsp_output); +// Output: a, b => c +``` +```python [Python] +from apyds_bnf import parse, unparse + +# Parse: Convert from readable Dsp to DS format +dsp_input = "a, b => c" +ds_output = parse(dsp_input) +print(ds_output) +# Output: +# a +# b +# ---- +# c + +# Unparse: Convert from DS format to readable Dsp +ds_input = "a\nb\n----\nc\n" +dsp_output = unparse(ds_input) +print(dsp_output) +# Output: a, b => c +``` +::: + +## 语法格式 + +### Ds 格式 (内部) + +Ds 格式使用 S-表达式（类 Lisp 语法）来表示逻辑 Rule： + +``` +premise1 +premise2 +---------- +conclusion +``` + +对于结构化 Term： + +- 函数：`(function f a b)` +- 下标：`(subscript a i j)` +- 二元操作符：`(binary + a b)` +- 一元操作符：`(unary ~ a)` + +### Dsp 格式 (人类可读) + +Dsp 格式使用传统的数学符号： + +``` +premise1, premise2 => conclusion +``` + +对于结构化 Term： + +- 函数：`f(a, b)` +- 下标：`a[i, j]` +- 二元操作符：`(a + b)` (带括号) +- 一元操作符：`(~ a)` (带括号) + +### 语法比较 + +| 描述 | Dsp 格式 | Ds 格式 | +|-------------|------------|-----------| +| 简单 Rule | `a, b => c` | `a\nb\n----\nc\n` | +| 公理 | `a` | `----\na\n` | +| 函数调用 | `f(a, b) => c` | `(function f a b)\n----------------\nc\n` | +| 下标 | `a[i, j] => b` | `(subscript a i j)\n-----------------\nb\n` | +| 二元操作符 | `(a + b) => c` | `(binary + a b)\n--------------\nc\n` | +| 一元操作符 | `~ a => b` | `(unary ~ a)\n-----------\nb\n` | +| 复杂表达式 | `((a + b) * c), d[i] => f(g, h)` | `(binary * (binary + a b) c)\n(subscript d i)\n---------------------------\n(function f g h)\n` | + +## 包信息 + +- **Python 包**: [apyds-bnf](https://pypi.org/project/apyds-bnf/) +- **npm 包**: [atsds-bnf](https://www.npmjs.com/package/atsds-bnf) +- **源代码**: [GitHub - bnf 目录](https://github.com/USTC-KnowledgeComputingLab/ds/tree/main/bnf) diff --git a/docs/zh/support-packages/egg.md b/docs/zh/support-packages/egg.md new file mode 100644 index 0000000..856300b --- /dev/null +++ b/docs/zh/support-packages/egg.md @@ -0,0 +1,187 @@ +# E-Graph 支持包 + +E-Graph 支持包为 DS 演绎系统提供了 Term 等价类的有效管理和操作。 + +E-Graph (等价图) 是一种数据结构，可以有效地表示 Term 的等价类，并自动维护同余闭包。该实现遵循 egg 风格的方法，具有延迟重建功能以获得最佳性能。灵感来自 [egg 库](https://egraphs-good.github.io/)。 + +## 安装 + +::: code-group +```bash [TypeScript] +npm install atsds-egg +``` +```bash [Python] +pip install apyds-egg +``` +::: + + 需要 Python 3.11-3.14。 + +## 用法 + +::: code-group +```typescript [TypeScript] +import { Term } from "atsds"; +import { EGraph } from "atsds-egg"; + +// Create an E-Graph +const eg = new EGraph(); + +// Add terms to the E-Graph +const a = eg.add(new Term("a")); +const b = eg.add(new Term("b")); +const x = eg.add(new Term("x")); + +// Add compound terms +const ax = eg.add(new Term("(+ a x)")); +const bx = eg.add(new Term("(+ b x)")); + +// Initially, (+ a x) and (+ b x) are in different E-classes +if (eg.find(ax) === eg.find(bx)) throw new Error("Should be different"); + +// Merge a and b +eg.merge(a, b); + +// Rebuild to restore congruence +eg.rebuild(); + +// Now (+ a x) and (+ b x) are in the same E-class +if (eg.find(ax) !== eg.find(bx)) throw new Error("Should be same"); +``` +```python [Python] +import apyds +from apyds_egg import EGraph + +# Create an E-Graph +eg = EGraph() + +# Add terms to the E-Graph +a = eg.add(apyds.Term("a")) +b = eg.add(apyds.Term("b")) +x = eg.add(apyds.Term("x")) + +# Add compound terms +ax = eg.add(apyds.Term("(+ a x)")) +bx = eg.add(apyds.Term("(+ b x)")) + +# Initially, (+ a x) and (+ b x) are in different E-classes +assert eg.find(ax) != eg.find(bx) + +# Merge a and b +eg.merge(a, b) + +# Rebuild to restore congruence +eg.rebuild() + +# Now (+ a x) and (+ b x) are in the same E-class +assert eg.find(ax) == eg.find(bx) +``` +::: + +### 同余闭包 (Congruence Closure) + +E-Graph 自动维护同余闭包。当两个 E-Class 合并时，`rebuild()` 方法确保所有同余 Term 保持在同一个 E-Class 中。 + +::: code-group +```typescript [TypeScript] +import { Term } from "atsds"; +import { EGraph } from "atsds-egg"; + +const eg = new EGraph(); + +// Add terms with nested structure +const fa = eg.add(new Term("(f a)")); +const fb = eg.add(new Term("(f b)")); +const gfa = eg.add(new Term("(g (f a))")); +const gfb = eg.add(new Term("(g (f b))")); + +// Merge a and b +const a = eg.add(new Term("a")); +const b = eg.add(new Term("b")); +eg.merge(a, b); + +// Rebuild propagates equivalence +eg.rebuild(); + +// Now all derived terms are equivalent +if (eg.find(fa) !== eg.find(fb)) throw new Error("fa != fb"); +if (eg.find(gfa) !== eg.find(gfb)) throw new Error("gfa != gfb"); +``` +```python [Python] +eg = EGraph() + +# Add terms with nested structure +fa = eg.add(apyds.Term("(f a)")) +fb = eg.add(apyds.Term("(f b)")) +gfa = eg.add(apyds.Term("(g (f a))")) +gfb = eg.add(apyds.Term("(g (f b))")) + +# Merge a and b +a = eg.add(apyds.Term("a")) +b = eg.add(apyds.Term("b")) +eg.merge(a, b) + +# Rebuild propagates equivalence +eg.rebuild() + +# Now all derived terms are equivalent +assert eg.find(fa) == eg.find(fb) +assert eg.find(gfa) == eg.find(gfb) +``` +::: + +## 核心概念 + +### E-Graph 结构 + +E-Graph 由几个关键组件组成： + +- **E-Node**：表示具有操作符和子节点的 Term +- **E-Class**：E-Node 的等价类 +- **Hash-consing**：通过将相同的节点映射到同一个 E-Class 来确保 E-Node 的唯一性 +- **并查集 (Union-Find)**：管理 E-Class 的等价关系 +- **Parents**：跟踪哪些 Term 依赖于每个 E-Class +- **Worklist**：管理延迟的同余重建 + +### 延迟重建 (Deferred Rebuilding) + +该实现使用 egg 风格的延迟重建： + +1. **Merge**：合并两个 E-Class 并添加到 Worklist +2. **Rebuild**：处理 Worklist 以恢复同余 +3. **Repair**：重新规范化父节点并合并同余节点 + +这种方法通过批量处理同余更新，提供了比立即重建更好的性能。 + +### 添加 Term + +Term 被转换为 E-Node 并添加到 E-Graph 中： + +- **Item（常量/函子）和 Variable**：原子 Term 如 `a`, `b`，或以反引号为前缀的 variable 如 `x`，表示为没有子节点的 E-Node +- **List**：复合 Term 如 `(+ a b)` 表示为操作符为 `"()"` 且每个列表元素都有子节点的 E-Node + +Hash-consing 机制确保相同的 E-Node 共享相同的 E-Class ID。 + +## API 参考 + +### TypeScript (atsds-egg) + +- `new EGraph()`: 创建一个新的 E-Graph +- `add(term: atsds.Term): EClassId`: 向 E-Graph 添加一个 Term +- `merge(a: EClassId, b: EClassId): EClassId`: 合并两个 E-Class +- `rebuild(): void`: 恢复同余闭包 +- `find(eclass: EClassId): EClassId`: 查找规范的 E-Class 代表 + +### Python (apyds-egg) + +- `EGraph()`: 创建一个新的 E-Graph +- `add(term: apyds.Term) -> EClassId`: 向 E-Graph 添加一个 Term +- `merge(a: EClassId, b: EClassId) -> EClassId`: 合并两个 E-Class +- `rebuild() -> None`: 恢复同余闭包 +- `find(eclass: EClassId) -> EClassId`: 查找规范的 E-Class 代表 + +## 包信息 + +- **Python 包**: [apyds-egg](https://pypi.org/project/apyds-egg/) +- **npm 包**: [atsds-egg](https://www.npmjs.com/package/atsds-egg) +- **源代码**: [GitHub - egg 目录](https://github.com/USTC-KnowledgeComputingLab/ds/tree/main/egg)