Dialectica Categories for the Lambek Calculus.
Lecture Notes in Computer Science(2018)
摘要
We revisit the old work of de Paiva on the models of the Lambek Calculus in dialectica models making sure that the syntactic details that were sketchy on the first version got completed and verified. We extend the Lambek Calculus with a n modality, inspired by Yetter's work, which makes the calculus commutative. Then we add the of-course modality !, as Girard did, to re-introduce weakening and contraction for all formulas and get back the full power of intuitionistic and classical logic. We also present the categorical semantics, proved sound and complete. Finally we show the traditional properties of type systems, like subject reduction, the Church-Rosser theorem and normalization for the calculi of extended modalities, which we did not have before.
更多查看译文
关键词
Lambek calculus,Dialectica models,Categorical semantics,Type theory,Structural rules,Non-commutative,Linear logic
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络