除了感叹号操作符的 <var> := ... 形式外，在 then 语句中不得引入额外的变量。每个出现在规则 then 语句中的术语都必须等于出现在早期 if 语句中的术语。绕过此限制的唯一方法是添加形式为 then <tm>!; 的语句。之后的 then 语句原子可以自由使用 <tm>。

例如，考虑以下关于半格理论的无效和有效规则

// Invalid: Cannot infer type of x.
rule {
    if x = x;
    then x = x;
}
// Valid (but nonsensical):
rule {
    if x: El;
    then x = x;
}

// Invalid: x and y are not introduced in an `if` statement.
rule {
    then meet(x, y)!;
}
// Valid:
rule {
    if x: El;
    if y: El;
    then meet(x, y)!;
}

// Invalid: meet(x, y) is not equal to a term occurring earlier.
rule {
    if le(z, x);
    if le(z, y);
    then le(z, meet(x, y));
}
// Valid: Assert that meet(x, y) exists in a then statement.
rule {
    if le(z, x);
    if le(z, y);
    then meet(x, y)!
    then le(z, meet(x, y));
}
// Valid: Suppose that meet(x, y) exists in if statement.
rule {
    if le(z, x);
    if le(z, y);
    if meet(x, y)!;
    then le(z, meet(x, y));
}

// Invalid: Both Meet(x, y) and Meet(y, x) do not occur earlier.
rule {
    if x: El;
    if y: El;
    then meet(x, y);
    then meet(y, x);
}

// Valid: the term on the left-hand side of the equation is introduced
// in an if statement.
rule {
    if meet(x, y)!;
    then meet(x, y);
    then meet(y, x);
}

// Valid: the term on the right-hand side of the equation is introduced
// earlier in a then statement.
rule {
    if x: El;
    if y: El;
    then meet(x, y)!;
    then meet(y, x) = meet(x, y);
}

// Invalid: meet(x, y) is not equal to a term that occurs earlier.
rule {
    if u = meet(x, meet(y, z))!;
    then meet(meet(x, y), z) = u;
}

// Valid: All of u, Meet(x, y) and z are introduced in an if statement.
rule {
    if u = meet(x, meet(y, z))!;
    if meet(x, y)!;
    then u = meet(meet(x, y), z);
}

生成的 Rust 接口

Eqlog 将每个 .eqlog 转换为一个 .rs 文件。Rust 文件必须在 src 目录内的一个模块中声明（例如 lib.rs 或 main.rs），使用 eqlog_runtime::eqlog_mod! 宏。

Eqlog 生成带文档的 Rust 代码。要构建和查看此文档，请运行

cargo doc --document-private-items --open

生成的 Rust 模块的公共 API 由以下符号组成

• 对于每个 Eqlog 类型，都有一个 Rust 类型 <TypeName>，用于表示该类型的元素 ID。
• 模型结构。其名称通过将文件名转换为 Upper Camel Case 而得。例如，对于 semi_group.eqlog，这将变成 SemiGroup。

模型结构具有以下成员函数

• fn new() -> Self
  创建一个空模型结构。
• fn close(&mut self)
  关闭模型下的所有规则。
• pub fn close_until(&mut self, condition:impl Fn(&Self) -> bool) -> bool
  关闭模型下的所有规则，直到满足条件。如果模型可以在所有规则下关闭，但条件仍然不成立，则返回 false。
• 对于每个类型
  • fn new_<sort_name>(&mut self) -> <TypeName>
    将一个新元素添加到模型结构中。
  • fn equate_<sort_name>(&mut self, lhs: <TypeName>, rhs: <TypeName>)
    在模型结构中强制执行 lhs = rhs 的等价。
  • fn are_equal_<sort_name>(&self, lhs: <TypeName>, rhs: <TypeName>) -> bool
    如果 lhs 和 rhs 表示相同的元素，则返回 true。
  • fn root_<sort_name>(&self, el: <TypeName>) -> <TypeName>
    返回元素的等价类的基本/根元素。
• 对于每个谓词
  • fn <pred_name>(&self,arg_1: <Type_1>, ...,arg_n: <Type_n>)
    检查给定的参数上谓词是否成立。
  • fn iter_<pred_name>(&self) ->impl'_ + 迭代器<Item =<arity>>
    返回一个满足谓词的元组的迭代器。迭代器产生的项类型由arity确定。
  • fn insert_<pred_name>(&mut self, arg_1: <Type_1>, ..., arg_n: <Type_n>)
    确保给定的参数上谓词成立。
• 对于每个函数
  • fn <func_name>(&self,arg_1: <Type_1>, ...,arg_n: <Type_n>) -> Option<<ResultType>>
    在给定的参数上评估函数。
  • fn iter_<func_name>(&self) ->impl'_ + 迭代器<Item =<arity>>
    返回一个遍历函数图中的元组的迭代器。迭代器产生的项类型由arity确定。
  • fn define_<func_name>(&mut self, arg_1: <Type_1>, ..., arg_n: <Type_n>) -> <ResultType>
    确保函数在给定的参数上定义，如果需要则添加新元素。
  • fn insert_<func_name>(&mut self, arg_1: <Type_1>, ..., arg_n: <Type_n>, result: <ResultType>)
    将元组插入函数的图中。

例如，以下是从半格理论生成的rust模块的公共声明

struct El;
struct Semilattice;
impl Semilattice {
  fn new() -> Self;
  fn close(&mut self);
  fn close_until(&mut self, condition: impl Fn(&Self) -> bool) -> bool;

  fn new_el(&mut self) -> El;
  fn equate_el(&mut self, lhs: El, rhs: El);
  fn are_equal_el(&self, lhs: El, rhs: El) -> bool;
  fn root_el(&self, el: El) -> El;

  fn le(&self, arg0: El, arg1: El) -> bool;
  fn iter_le(&self) -> impl '_ + Iterator<Item = (El, El)>;
  fn insert_le(&mut self, arg0: El, arg1: El);

  fn meet(&self, arg0: El, arg1: El) -> Option<El>;
  fn iter_meet(&self) -> impl '_ + Iterator<Item = (El, El, El)>;
  fn define_meet(&mut self, arg0: El, arg1: El) -> El;
  fn insert_meet(&mut self, arg0: El, arg1: El, result: El);
}

数据模型和算法

标准Datalog功能

eqlog生成的理论模型结构可以看作是内存中的SQL数据库，其模式由类型、谓词和函数声明给出。给定类型的元素是简单的整数ID，模型结构维护每个类型的有效ID列表。每个谓词 p 都表示为一个表，其行是谓词成立的元素的元组。函数表示为图。例如，如果 f 是一个单参数函数，那么 f 的内部表将由以下形式的行组成：(x, f(x))。

close 函数重复枚举规则中的if语句的所有匹配，并将规则中then语句对应的数据附加到模型中。最终，达到一个不动点（除非理论包含非满射规则，见下文），算法停止。例如，对于传递性公理

rule {
    if le(x, y);
    if le(y, z);
    then le(x, z);
}

close 函数枚举 Le 表中所有满足 y_0 = y_1 的 (x, y_0) 和 (y_1, z) 行，然后将行 (x, z) 添加到 Le。最终，Le 表将已经包含我们找到的所有新行 (x, z)，这意味着我们已经达到不动点，可以停止：现在 le 谓词是传递的。

if语句实例的枚举称为SQL术语中的（内部）连接。SQL数据库使用索引加速内部连接，eqlog自动选择并维护索引以加快eqlog文件中列出的规则所需的连接。在每次迭代中，不需要枚举在上一迭代中已枚举的if语句。这种优化称为半朴素评估，eqlog再次使用它来加速 close 函数。

等式

除了之前讨论的标准日志功能外，eqlog还支持在then语句中的等式。一个例子是偏序的反对称公理。

rule {
    if le(x, y);
    if le(y, x);
    then x = y;
}

在then语句中的等式的另一个来源是函数的隐式功能公理：对于函数f，如果我们发现图f中同时存在(x_1, ..., x_n, y)和(x1, , ..., x_n, z)，那么我们必须推导出y = z。如果我们用g_f表示f的图，那么隐式功能公理可以表述如下。

rule {
    if g_f(x_1, ..., x_n, y);
    if g_f(x_1, ..., x_n, z);
    then y = z;
}

然而，需要注意的是，在eqlog文件中不能直接引用函数的图。

为了处理导出的等式，eqlog模型结构为每种类型维护并查集数据结构。当在调用close过程中推导出等式x = y时，eqlog会合并x和y的等价类。

为了加快匹配if语句时所需连接的计算，eqlog为每个表维护索引。然而，只有当元素id可以直接比较相等而不是咨询并查集数据结构时，这些索引才能使用。因此，eqlog维护一个不变性，即所有谓词和函数图表只包含规范类型元素，即只有id是相应并查集数据结构的根节点的元素。

当eqlog将某个元素x的等价类合并到元素y的等价类中时，这个不变性暂时被违反。为了恢复这个不变性，eqlog会从包含x的表中删除所有行，用新的根idy替换x，然后再次插入行。为了加快这个过程，eqlog为每个根id维护一个列表，该列表包含所有出现根id的行。

非全射规则和非终止

回想一下，eqlog规则需要是全射的，除非使用感叹号操作符!：then语句中的每个元素都必须等于if语句中的某个元素。在全射规则下关闭模型结构不会增加模型中元素的数量，这保证了close函数最终会终止。

如果有非全射规则，则这并不保证。考虑以下eqlog理论，该理论形式化自然数

type N;
zero: N;
succ: N -> N;

rule {
    then Zero()!;
}
rule {
    if n: N;
    then Succ(n)!;
}

关闭空模型结构首先将元素zero添加到模型中，然后是元素succ(zero)，然后是succ(succ(zero))等等。然而，非全射规则的存在并不一定意味着close函数必须无限期运行。例如，半格理论包含非全射规则

rule {
    if x: El;
    if y : El;
    then meet(x, y)!;
}

// Match `if` statements in a rule and change the model such that the
// corresponding `then` statements holds. Returns true if the model was
// changed, i.e. if new facts were concluded.
fn adjoin_conclusions(ax: Axiom) -> bool {
  ...
}

fn close() {
  loop {
    loop {
      let model_changed = surjective_rules.iter().any(adjoin_conclusion);
      if !model_changed {
        break;
      }
    }

    let model_changed = non_surjective_rules.iter().any(adjoin_conclusion);
    if !model_changed {
      break;
    }
  }
}