詳細は以下をご覧ください。

https://www.waseda.jp/inst/wias/news/2017/07/04/4467/


----

Program:

1.  July 14 (Friday, G-Lab, 6th floor, East Building, Mita campus of Keio University):

Time: 13:00-18:00

Speakers: Andrew Arana (Université Paris 1 Panthéon-Sorbonne, IHPST), Kengo Okamoto (Tokyo Metropolitan University), Ryota Akiyoshi (Waseda University), Makoto Fujiwara (Waseda University)
The details will be announced soon at the following page:
https://abelard.flet.keio.ac.jp/jindex.php


2.  July 15 (Saturday, Meeting Room #1, 5th Floor, Bldg. 9, Waseda Campus of Waseda University)

Talk 1:
13:00-14:00
Ryoma Shinya (The University of Tokyo)
Title:
Almost every simply typed λ-term has a long β-reduction sequence 
Abstract:
It is well known that the length of a β-reduction sequence of a simply typed λ-term of order k can be huge; it is as large as k-fold exponential in the size of the λ-term in the worst case. We consider the following relevant question about quantitative properties, instead of the worst case: how many simply typed λ-terms have very long reduction sequences? We provide a partial answer to this question, by showing that asymptotically almost every simply typed λ-term of order k has a reduction sequence as long as (k − 2)-fold exponential in the term size, under the assumption that the arity of functions and the number of variables that may occur in every subterm are bounded above by a constant. The work has been motivated by quantitative analysis of the complexity of higher-order model checking.

Talk 2:
14:00-15:00
Taishi Kurahashi (National Institute of Technology, Kisarazu College)
Title:
On partial disjunction properties of theories containing PA
Abstract:
It is well-known that intuitionistic predicate logic and Heyting Arithmetic have the disjunction property (DP). For intuitionistic logic, DP seems to reflect its constructivity. In classical logic, DP plays a different role. If a theory T in classical logic has DP, then T is complete because the law of excluded middle is valid. Thus in classical logic, every \Sigma_1-definable consistent extension of Peano Arithmetic PA does not have DP by the Gödel–Rosser first incompleteness theorem. On the other hand, PA enjoys a partial disjunction property. Let \Gamma be a class of formula. We say that a theory T has the \Gamma-disjunction property (\Gamma-DP) iff for any \Gamma sentences \varphi and \psi, at least one of \varphi or \psi is provable in T whenever \varphi \lor \psi is provable in T.  It is known that PA has \Sigma_1-DP but does not have \Pi_1-DP. In this talk, we present several results concerning partial disjunction properties and other related properties of theories containing PA which is not necessarily \Sigma_1-definable.

Talk 3:
15:20-16:20
Naosuke Matsuda (Kanagawa University)
Title:
Some extensions of de Jongh's theorem
Abstract:
It is obvious that if a propositional formula A is provable in intuitionistic propositional calculus, 
then each arithmetical instance is provable in Heyting Arithmetic. 
The converse of this statement is known as de Jongh's theorem. 
In this talk, I give an introduction to de Jongh's theorem 
and introduce some extensional works.

Talk 4:
16:20-17:20
Masahiko Sato (Kyoto University)
Title:
A common notation system for lambda calculus and combinatory logic
Abstract:
We present a notation system which can be used to
faithfully represent both the terms of lambda calculus and
combinatory logic. We show the faithfullness of the
representations by observing that the representations respect the
beta and eta reduction rules. We also argue that Curry's Last
Problem (J.R.Hindley, Curry's Last Problem: Imitating
lambda-beta-reduction in Combinatory Logic) in its original form
is an ill-posed problem, and can be solved naturally by expressing
the problem in our notation system. 


---------------------------------------------------------------------

Organizers:

Ryota Akiyoshi (Waseda Institute for Advanced Study, Waseda University)

Makoto Fujiwara (Waseda Institute for Advanced Study, Waseda University)

Mitsuhiro Okada (Global Research Center for Logic and Sensibility, Keio University)

Co-host: Waseda Institute for Advanced Study (Waseda University), Global Research Center for Logic and Sensibility (Keio University)

Contact:
Ryota Akiyoshi
[email protected]