コバヤシ サトシ   KOBAYASHI SATOSHI
  小林 聡
   所属   京都産業大学  情報理工学部 情報理工学科
   職種   教授
言語種別 英語
発行・発表の年月 2008
形態種別 研究論文
査読 査読あり
標題 A New Translation for Semi-classical Theories --- Backtracking without CPS
執筆形態 単著
掲載誌名 Proceedings of 9th International Symposium on Functional and Logic Programming, FLOPS 2008
掲載区分国外
総ページ数 24
著者・共著者 Satoshi Kobayashi
概要 Most research of algorithm extraction from classical proofs is based on double negation translation or its variants. From the viewpoint of Curry-Howard isomorphism, double negation translation corresponds to CPS translation. Unfortunately, CPS translation makes resulting programs very complex.

In this paper, we study a new translation for a semi-classical logic which is not based on double negation translation. Though it does not validate full classical logic, it translates Limit Computable Mathematics (LCM) into constructive mathematics.

Our translation is inspired by game semantics with backtracking rules. Using the translation, we can extract an algorithm from a proof of a proposition $A$ in LCM.
The extracted algorithm gives a recursive winning strategy for the first mover of the game defined from $A$, at least when $A$ is implication-free.
DOI 10.1007/978-3-540-78969-7
ISBN 978-3-540-78969-7
researchmap用URL https://www.springer.com/jp/book/9783540789680