Bindings, Mobility of Bindings, and the "generic judgments"-Quantifier: An Abstract
Bindings, Mobility of Bindings, and the "generic judgments"-Quantifier: An Abstract
复制标题
绑定、绑定的移动性和“一般判断”——量词：摘要
DOI：
10.1007/978-3-540-30124-0_4
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
D. Miller
中科院分区：
文献类型：
--
作者：
D. Miller
如果您的对象级语法（公式、程序、类型等）包含绑定器，则将这些绑定器映射到元语言中的绑定器。函数式编程和构造型理论：可用的绑定器是函数空间的绑定器。Proof Search（逻辑编程的现代更新）：可用的绑定器是类型化的λ-表达式，具有等式（因此，统一）模α，β和η转换。
“If your object-level syntax (formulas, programs, types, etc) contain binders, then map these binders to binders in the meta-language.” Functional Programming & Constructive type theories: the binder available is the one for function spaces. Proof Search (a modern update to logic programming): the binders available are typed λ-expressions with equality (and, hence, unification) modulo α, β, and η conversions.