Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
A New Translation for Semi-classical Theories — Backtracking without CPS
| |
|
A New Translation for Semi-classical Theories — Backtracking without CPS
Satoshi Kobayashi1 
| (1) |
Dept. of Computer Science, Kyoto Sangyo University, Kamigamo Motoyama, Kita-ku, Kyoto, Japan |
Abstract
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.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|