文件名称：abstract-binding-trees:抽象绑定树（抽象语法树加活页夹），作为Agda中的库
文件大小：113KB
文件格式：ZIP
更新时间：2024-06-14 22:38:34
Agda
抽象绑定树 这是一个用于抽象绑定树的Agda库，如Robert Harper的《 Practical Foundations for Programming Languages》一书的第1章所述。 抽象绑定树（ABT）是一个抽象语法树，它也知道绑定器和变量。 因此，该库还定义了ABT上的取代，并提供了有关取代的定理。 该库使用de Bruijn索引表示变量。 抽象绑定树ABT由两种节点组成： 变量：变量节点是叶子（无子代），并存储de Bruijn索引。 运算符：运算符节点被标记为运算符的种类，并且根据运算符的种类，它具有零个或多个子代。 ABT数据类型在“ 模块中定义，该参数由运算符的种类及其签名进行参数化，该运算符指定诸如每种运算符的子节点数之类的内容。 要指定运算符，请为每种类型创建一个带有一个构造函数的数据类型定义。 以lambda演算为例，将定义两种：一种用于lambd
【文件预览】：
abstract-binding-trees-master
----src()
--------Fold.agda(7KB)
--------GSubst.agda(4KB)
--------WellScoped.agda(10KB)
--------GenericSubstitution.agda(5KB)
--------MapFusion.agda(6KB)
--------OldMap.agda(15KB)
--------Map.agda(7KB)
--------experimental()
--------AbstractBindingTree.agda(6KB)
--------FoldMapFusion.agda(13KB)
--------FoldPreserve.agda(13KB)
--------MapPreserve.agda(4KB)
--------Substitution.agda(11KB)
--------Structures.agda(6KB)
--------Sig.agda(282B)
--------examples()
--------ScopedTuple.agda(7KB)
--------Renaming.agda(6KB)
--------Syntax.agda(382B)
--------Makefile(693B)
--------Var.agda(2KB)
--------ListAux.agda(1KB)
--------SubstPreserve.agda(3KB)
--------ABTPredicate.agda(3KB)
--------sub-normal-form()
--------FoldFoldFusion.agda(9KB)
----abt.agda-lib(48B)
----README.md(14KB)