又一则Martin-Lof逻辑框架的归一化证明——具有正确元数的项强归一化
计算机科学中的逻辑
2007-05-23 v2
摘要
本文证明了Martin-Löf逻辑框架的强归一化，并提出“正确元数”这一弱于良类型的条件同样能保证强归一化。
关键词
引用
@article{arxiv.cs/0506060,
title = {Yet another normalisation proof for Martin-Lof's logical framework--Terms with correct arities are strongly normalising},
author = {Yong Luo},
journal= {arXiv preprint arXiv:cs/0506060},
year = {2007}
}
备注
19 pages