局部局部推理：面向全地面存储的BI超前束
计算机科学中的逻辑
2020-03-12 v1
摘要
对动态内存分配建模与推理是理论计算机科学中成熟的研究方向之一，其尤以在语义、推理和证明理论中 notorious 挑战的来源而著称。我们利用近期关于全地面存储（full ground store）的范畴语义进展（以全地面存储单子表述），构建相应程序上的高阶逻辑语义。我们的主要结果是构造了一个（直觉主义）BI超前束（BI-hyperdoctrine），它可被视为基于局部存储的高阶逻辑的语义核心。尽管我们广泛使用了已有的通用工具，仍须对若干原则性改动以实现所需构造：原单子作用于全堆（以禁用悬空指针），而我们的版本涉及偏堆（堆片）以支持使用分离合取的复合推理。我们构造的另一显著特征是，与现有通用方法不同，我们的BI代数并非直接源于内部范畴偏交换幺半群。
引用
@article{arxiv.2003.05386,
title = {Local Local Reasoning: A BI-Hyperdoctrine for Full Ground Store},
author = {Miriam Polzer and Sergey Goncharov},
journal= {arXiv preprint arXiv:2003.05386},
year = {2020}
}
备注
version with appendix