除了感叹号操作符的 <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。
• 模型结构。其名称通过将文件名转换为驼峰式命名法生成。例如，对于 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表中所有行(x, y_0)和(y_1, z)，使得y_0 = y_1，然后将行(x, z)添加到Le。最终，Le表将包含我们找到的所有新行(x, z)，这意味着我们已经达到不动点，可以停止：现在谓词le是传递的。

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

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

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

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

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;
    }
  }
}