非结合Lambek演算经典扩展的聚焦与相模型
计算机科学中的逻辑
2011-06-03 v1
摘要
Lambek的非结合句法演算（NL）以其资源敏感性著称：通常的结构规则——弱化、收缩、交换乃至结合性——均被舍弃。近来，已有一些保守扩展方案被提出，以消除NL对单结论矢列式的直觉主义偏向：De Groote和Lamarche的经典非结合Lambek演算（CNL），以及Moortgat及其合作者的Lambek-Grishin演算（LG）。我们为上述方案证明了Andreoli的聚焦性质：这是一个关于无Cut矢列式推导的规范化结果，能在很大程度上识别出那些仅因平凡规则排列而不同的推导。为此，我们从一个“统一”的矢列式表示出发，通过添加结构规则从LG导出CNL。规范化证明通过构造句法相模型来完成，其中每个“真值”都有一个聚焦证明，类似于Okada以及Herbelin和Lee的工作。
引用
@article{arxiv.1106.0399,
title = {Focalization and phase models for classical extensions of non-associative Lambek calculus},
author = {Arno Bastenhof},
journal= {arXiv preprint arXiv:1106.0399},
year = {2011}
}
备注
To be submitted