lim+、delta+与beta步的非可置换性
人工智能
2013-09-17 v1 计算机科学中的逻辑
摘要
利用一个面向人类的(lim+)定理的形式化示例证明（即和的极限等于极限的和，该证明本身具有参考价值），我们展示了beta步与delta+步（根据Smullyan分类）的非可置换性，这种非可置换性在使用非自由化delta规则时不可见，在使用进一步自由化的delta规则（如delta++规则）时也不严重。除了以若干教学意图仔细展示(lim+)的证明搜索过程外，主要议题是解释为何在某些演算中beta步的顺序具有如此重要的实际作用。
引用
@article{arxiv.0902.3635,
title = {lim+, delta+, and Non-Permutability of beta-Steps},
author = {Claus-Peter Wirth},
journal= {arXiv preprint arXiv:0902.3635},
year = {2013}
}
备注
ii + 36 pages