标签：Term Rewriting

带「Term Rewriting」标签的文章。

• Egglog 快速入门（三）：复数定义与内置类型

  发布于2026年2月17日

  承接第二篇的实数定义，先纯构造定义复数，再介绍 egglog 内置的 i64、Rational、f64、Vec、Set、MultiSet 等类型，以及 function、extract、cost 等特性，并展示如何用它们实现高效复数运算。

• Egglog 快速入门（二）：从自然数到整数、有理数与实数

  发布于2026年2月15日

  承接第一篇的 Peano 自然数，逐步扩展：先引入 Neg 构造器得到整数，再定义有理数为整数对，并展示 rule、:when、relation、birewrite 等 egglog 特性。

• Egglog 快速入门（一）：用等价饱和定义自然数运算

  发布于2026年2月13日

  以 Peano 自然数的加法与乘法为例，介绍 egglog 语言：datatype、constructor、rewrite、check、run-schedule 与 saturate，以及 egg 与 egglog 的关系。

• E-graphs 学习笔记：动机与 Explanations

  更新于2026年2月12日

  传统 Term Rewriting 的局限如何引出 E-graph；volvox 实战困境；egg 的 explain_equivalence、FlatExplanation 与 TreeExplanation，以及如何读懂除法化简的证明序列。