交换：命名与索引显式替换演算之间的自然桥梁
计算机科学中的逻辑
2011-02-21 v1 编程语言
摘要
本文致力于介绍lambda_rex,一个使用德布鲁因索引且具有简单记法的显式替换演算。通过与lambda_ex(一个近期提出的带有变量名的形式体系)同构,lambda_rex实现了beta归约的模拟(Sim)、beta强归一化的保持(PSN)以及元合流性(MC)等理想性质。我们的演算基于lambda_dB的一种新颖表示,使用了最初由德布鲁因设计的交换概念。除了lambda_rex,还介绍了与lambda_x和lambda_xgc同构的另外两个索引演算,展示了我们的技术在应用于设计已知命名演算的索引版本时的潜力。
引用
@article{arxiv.1102.3730,
title = {Swapping: a natural bridge between named and indexed explicit substitution calculi},
author = {Ariel Mendelzon and Alejandro Ríos and Beta Ziliani},
journal= {arXiv preprint arXiv:1102.3730},
year = {2011}
}
备注
In Proceedings HOR 2010, arXiv:1102.3465