Sixth NII Type Theory Workshop

Date: November 14, 2011, 11:00--17:00

Place: National Institute of Informatics, Room 2005 (20th floor) 場所: 国立情報学研究所 20階 2005室 (半蔵門線,都営地下鉄三田線・新宿線 神保町駅または東西線 竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/introduce/access1-j.shtml)

Program:

11:00--11:30 Takayuki Koai (National Institute of Informatics) Title: Verification of Substitution Theorem Using HOL

11:30--12:00 Mauricio Hernandes (The Graduate University for Advanced Studies) Title: Game theory from a logician perspective

12:00--13:40 Lunch Break

13:40--14:10 Takanori Hida (Kyoto University) Title: A computational interpretation of the axiom of determinacy

14:10--14:40 Makoto Tatsuta (National Institute of Informatics) Title: Non-Commutative Infinitary Peano Arithmetic

14:40--15:00 Tea Break

15:00--16:00 Neil D. Jones (University of Copenhagen) Title: Termination Analysis of the Untyped lambda-Calculus

16:00--17:00 Stefano Berardi (Torino University) Title: A Topology over a set of Knowledge States and a Fixed Point Problem

Abstracts: ---------------------------------------------------------------------- Takayuki Koai (National Institute of Informatics) Title: Verification of Substitution Theorem Using HOL

Abstract: Substitution Theorem is a new theorem in untyped lambda calculus, which was proved in 2006. This theorem states that for a given lambda term and given free variables in it, the term becomes weakly normalizing when we substitute arbitrary weakly normalizing terms for these free variables, if the term becomes weakly normalizing when we substitute a single arbitrary weakly normalizing term for these free variables. This paper formalizes and verifies this theorem by using higher-order theorem prover HOL. A control path, which is the key notion in the proof, explicitly uses names of bound variables in lambda terms, and it is defined only for lambda terms without bound variables renaming. The lambda terms without bound variable renaming are formalized by using the HOL package based on contextual alpha-equivalence. The verification uses 10119 lines of HOL code and 326 lemmas. This is a joint work with Makoto Tatsuta. ---------------------------------------------------------------------- Mauricio Hernandes (The Graduate University for Advanced Studies) Title: Game theory from a logician perspective

Abstract: I intend in this talk to introduce a few concepts in game theory like Nash Equilibrium and Backward-Induction, and then express those ideas with some modal logic. ---------------------------------------------------------------------- Takanori Hida (Kyoto University) Title: A computational interpretation of the axiom of determinacy

Abstract: Axiom of determinacy(AD) is a central topic in descriptive set theory and there are a number of research on this axiom. In this talk, we approach to the computational content of negative translation of AD using realizability interpretation due to Berardi, Bezem and Coquand (1998). ---------------------------------------------------------------------- Makoto Tatsuta (National Institute of Informatics) Title: Non-Commutative Infinitary Peano Arithmetic

Abstract: Does there exist any sequent calculus such that it is a subclassical logic and it becomes classical logic when the exchange rules are added? The first contribution of this paper is answering this question for infinitary Peano arithmetic. This paper defines infinitary Peano arithmetic with non-commutative sequents, called non-commutative infinitary Peano arithmetic, so that the system becomes equivalent to Peano arithmetic with the omega-rule if the the exchange rule is added to this system. This system is unique among other non-commutative systems, since all the logical connectives have standard meaning and specifically the commutativity for conjunction and disjunction is derivable. This paper shows that the provability in non-commutative infinitary Peano arithmetic is equivalent to Heyting arithmetic with the recursive omega rule and the law of excluded middle for Sigma-0-1 formulas. Thus, non-commutative infinitary Peano arithmetic is shown to be a subclassical logic. The cut elimination theorem in this system is also proved. The second contribution of this paper is introducing infinitary Peano arithmetic having antecedent-grouping and no right exchange rules. The first contribution of this paper is achieved through this system. This system is obtained from the positive fragment of infinitary Peano arithmetic without the exchange rules by extending it from a positive fragment to a full system, preserving its 1-backtracking game semantics. This paper shows that this system is equivalent to both non-commutative infinitary Peano arithmetic, and Heyting arithmetic with the recursive omega rule and the Sigma-0-1 excluded middle. This is a joint work with Stefano Berardi and was presented at CSL 2011. ---------------------------------------------------------------------- Neil D. Jones (University of Copenhagen) Title: Termination Analysis of the Untyped lambda-Calculus

Abstract: An algorithm is developed that, given an untyped lambda-expression, can certify that its call-by-value evaluation will terminate. It works by an extension of the ``size-change principle'' earlier applied to first-order programs. The algorithm is sound (and proven so) but not complete: some lambda-expressions may in fact terminate under call-by- value evaluation, but not be recognised as terminating. The intensional power of size-change termination is reasonably high: It certifies as terminating all primitive recursive programs, and many interesting and useful general recursive algorithms including programs with mutual recursion and parameter exchanges, and Colson's ``minimum'' algorithm. Further, the approach allows free use of the Y combinator, and so can identify as terminating a substantial subset of PCF. (joint work with Nina Bohr; in Logical Methods in Computer Science, 2008, Issue 1) ---------------------------------------------------------------------- Stefano Berardi (Torino University) Title: A Topology over a set of Knowledge States and a Fixed Point Problem

Abstract: We give an abstract formulation of the termination problem for realizer of Heyting Arithmetic plus various subsystem of classical logic. This termination problem is expressed as the existence of a fixed point for a class of continuous maps in a suitable topology. ----------------------------------------------------------------------