京都大学数理解析研究所の佐藤です。
2月9日11:00から、東京大学のMarc Bagnol氏に 以下の講演をしていただくことになりましたので、 ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 11:00-12:00, 9 Feb, 2017 Place: Rm 478, Research Building 2, Main Campus, Kyoto University 京都大学 本部構内 総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34) http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物)
Speaker: Marc Bagnol (JSPS Postdoctoral Fellow, University of Tokyo)
Title: Multiplicative-Additive Proof Equivalence is Logspace-complete
Abstract: Given a logic presented in a sequent calculus, a natural question is that of equivalence of proofs: to determine whether two given proofs are equated by any denotational semantics, i.e. any categorical interpretation of the logic compatible with its cut-elimination procedure. This notion can usually be captured syntactically by a set of rule permutations.
Very generally, proofnets can be defined as combinatorial objects which provide canonical representatives of equivalence classes of proofs. In particular, the existence of proof nets for a logic provides a solution to the equivalence problem of this logic. In certain fragments of linear logic, it is possible to give a notion of proofnet with good computational properties, making it a suitable representation of proofs for studying the cut-elimination procedure, among other things.
It has recently been proved that there cannot be such a notion of proofnets for the multiplicative (with units) fragment of linear logic, due to the equivalence problem for this logic being Pspace-complete.
We will investigate the multiplicative-additive (without unit) fragment of linear logic and see it is closely related to binary decision trees: we can build a representation of proofs based on binary decision trees, reducing proof equivalence to decision tree equivalence. We will see as a consequence that the proof equivalence problem multiplicative-additive linear logic is Logspace-complete.