Forcing as a Program Transformation
Résumé
This paper is a study of the forcing translation through the proofs as programs correspondence in classical logic, following the methodology introduced by Krivine. For that, we introduce an extension of (classical) higher-order arithmetic suited to express the forcing translation, called PAw+. We present the proof system of PAw+ (based on Curry-style proof terms with call/cc) as well as the corresponding classical realizability semantics. Then, given a poset of conditions (represented in PAw+ as an upwards closed subset of a fixed meet semi-lattice), we define the forcing translation A -> (p forces A) (where A ranges over propositions) and show that the corresponding transformation of proofs is induced by a simple program transformation t -> t* defined on raw proof-terms (i.e. independently from the derivation). From an analysis of the computational behavior of transformed programs, we show how to avoid the cost of the transformation by introducing an extension of Krivine's abstract machine devoted to the execution of proofs constructed by forcing. We show that this machine induces new classical realizability models and present the corresponding adequacy results.