作为AGI“思维语言”基础的反射式元图重写

MeTTa（Meta Type Talk）是为OpenCog Hyperon AGI系统创建的一种新型编程语言。它被设计为一种元语言，具有用于处理符号、接地、变量、类型、替换和模式匹配的最基础且通用的机制。其原语可用于创建新的类型系统及相关的DSL。非正式地说，MeTTa是Hyperon最低层次的“思维语言”——即用于学习更特定知识表示的算法所运行的元语言，且这些算法本身也可用该语言表示。在此我们解释如何将一个MeTTa语言形式化为一个元图重写规则系统，鉴于Hyperon的核心组件是一个分布式元图知识存储（Atomspace），该方法自然契合Hyperon框架。构成MeTTa程序的元图重写规则本身也可表示为元图，从而为MeTTa的反射与自修改代码提供了自然模型。考虑那些计算其他MeTTa程序执行轨迹之间等价性的MeTTa程序，使我们能够利用同伦类型论对MeTTa执行轨迹空间建模。考虑MeTTa程序在MeTTa程序执行轨迹间映射、而这些程序又在MeTTa程序执行轨迹间映射……的极限情形，我们发现一个给定的MeTTa代码库可被有效建模为无穷群胚（infinity-groupoid），而所有MeTTa代码库的空间则为一个(∞,1)-拓扑斯（topos）。该拓扑斯基本上等同于此前在离散物理背景下由超图重写规则导出的所谓“Ruliad”。将MeTTa形式化为元图重写规则，也可为在MeTTa解释器中构建高效的模式匹配与等价推理方法的实现提供有用框架。