从双推出语法到带与不带指数模态的超图Lambek语法
计算机科学中的逻辑
2023-03-29 v1 形式语言与自动机理论
摘要
我们研究如何将基于双推出(DPO)方法的著名超图语法与超图Lambek演算HL上的语法(HL-语法)相联系。结果表明,DPO规则可利用类似于Kanazawa用于乘法-指数线性逻辑的方法,由HL的类型自然编码。为推广其推理,我们通过添加指数模态扩展超图Lambek演算,得到新演算HMEL0;随后证明任意DPO语法均可转换为等价的HMEL0-语法。我们还定义了合取Kleene星,其表现类似于该指数模态,并建立了类似结果。若既不向HL添加指数模态也不添加合取Kleene星,则仍可使用相同编码,并证明任意对推导长度有线性限制的DPO语法可转换为等价的HL-语法。
引用
@article{arxiv.2303.15788,
title = {From Double Pushout Grammars to Hypergraph Lambek Grammars With and Without Exponential Modality},
author = {Tikhon Pshenitsyn},
journal= {arXiv preprint arXiv:2303.15788},
year = {2023}
}
备注
In Proceedings TERMGRAPH 2022, arXiv:2303.14219