[logic-ml] NII Type Theory Workshop

[Makoto Tatsuta]

		   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.
----------------------------------------------------------------------