qQ`Fb?QT QM *QKTmi#BHBiv h?2Q`v M/
6QmM/iBQMb Q7 Ji?2KiB+b kyR3am`m;/B *KTmb- J2BDB lMBp2`bBiv- hQFvQ- CTMX
RjĜR8 a2Ti2K#2`- kyR3
lT/i2/ QM a2Ti2K#2` N- kyR3

*QMi2Mib
R S`Q;`KK2

kk #bi`+ib
S2`KmiiBQMb Q7 i?2 BMi2;2`b BM/m+2 QMHv i?2 i`BpBH miQKQ`T?BbK Q7 i?2 hm`BM; /2;`22b
U"DQ`M EDQb@>Mbb2MV X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X*?BiBMǶb MmK#2` b  7mM+iBQM Uum GBM;V X X X X X X X X X X X X X X X X X X X X X X X X X X X X
JQMQiQMQmb #2iiBM; bi`i2;B2b BM r`T2/ +bBMQb U:2Q`;2 "`KTHBbV X X X X X X X X X X X X*QMiBMmQmb pHmiBQMb QM [mbB@SQHBb? bT+2b UJii?2r /2 "`2+?iV X X X X X X X X X X X X X X*QKTmi2`@bbBbi2/ T`QQ7b pB BMi2`pH `Bi?K2iB+, BMi`Q/m+iBQM M/ TTHB+iBQMb UhQKQvmFB
JBvDBV X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X.2+BbBQM S`Q#H2Kb BM Ji`Bt a2KB;`QmTb, H;Q`Bi?KB+ /2+B/#BHBiv M/ +QKTmiiBQMH +QK@
TH2tBiv UA;Q` SQiTQpV X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X X

j

GQ+H P`;MBx2`b,
FBiQb?B ErKm` UFrKm`!BM7XFvmb?m@mX+XDTVE2Mb?B JBv#2 U`2b2`+?!F2Mb?BXKBv#2XMK2V

R

j
j
j
j
9
9

R S`Q;`KK2
h?m`b/v Rj
Ry,yyĜRk,yy 6mDBr`@ErB- EDQb@>Mbb2M
Rk,yyĜRj,jy GmM+? "`2F
Rj,jyĜRd,yy amxmFB- S2HmT2bbv- LF#vb?B@hMF@GB- JBv#2

6`B/v R9Ry,yyĜRk,yy JBxmbr- um
Rk,yyĜRj,jy GmM+? "`2F
Rj,jyĜRd,yy "`KTHBb- JBv#2- /2 "`2+?i- uQFQvK

aim`/v R8Ry,yyĜRk,yy >KKQiQ@ErKm`@wB2;H2`- JBvDB
Rk,yyĜRj,jy GmM+? "`2F
Rj,jyĜR8,jy SQiTQp- ErKm`@ai2BM#2`;@h?B2bkk #bi`+ib
S2`KmiiBQMb Q7 i?2 BMi2;2`b BM/m+2 QMHv i?2 i`BpBH miQKQ`T?BbK Q7 i?2 hm`BM;/2;`22b"DQ`M EDQb@>Mbb2M UlMBp2`bBiv Q7 >rBB i JMQV
Ab i?2`2  MQMi`BpBH miQKQ`T?BbK Q7 i?2 hm`BM; /2;`22b\ Ai Bb  KDQ` QT2M T`Q#H2K Q7 +QK@
Tmi#BHBiv i?2Q`vX Sbi `2bmHib ?p2 HBKBi2/ ?Qr MQMi`BpBH miQKQ`T?BbKb +QmH/ TQbbB#Hv #2X >2`2 r2+QMbB/2` BMbi2/ ?Qr M miQKQ`T?BbK KB;?i #2 BM/m+2/ #v  7mM+iBQM QM `2Hb- Q` 2p2M #v  7mM+iBQM
QM BMi2;2`bX q2 b?Qr i?i  T2`KmiiBQM Q7 ! +MMQi BM/m+2 Mv MQMi`BpBH miQKQ`T?BbK Q7 i?2
hm`BM; /2;`22b Q7 K2K#2`b Q7 2! - M/ BM 7+i Mv T2`KmiiBQM i?i BM/m+2b i?2 i`BpBH miQKQ`T?BbK
Kmbi #2 +QKTmi#H2X  KBM B/2 Q7 i?2 T`QQ7 Bb iQ +QMbB/2` i?2 K2K#2`b Q7 2! iQ #2 T`Q##BHBiB2bM/ mb2 biiBbiB+b, 7`QK `M/QK Qmi+QK2b 7`QK  /Bbi`B#miBQM r2 +M +QKTmi2 i?i /Bbi`B#miBQM- #mi
MQi Km+? KQ`2X AM i?2 b2+QM/ T`i Q7 i?2 iHF- r2 Mbr2`  [m2biBQM Q7 a+?r2#2` 7`QK kyRj #v;BpBM; M 2tTHB+Bi 2tKTH2 Bb ;Bp2M Q7  +QmMi#H2 ;`QmT i?i Bb MQi BbQKQ`T?B+ iQ i?2 miQKQ`T?BbK;`QmT Q7 i?2 hm`BM; /2;`22b Aut(DT )X h?Bb Bb Q#iBM2/ #v b?QrBM; i?i Aut(DT ) ?b  T`2b2MiiBQM
`2+m`bBp2 BM EH22M2Ƕb OX q2 HbQ b?Qr i?i Aut(DT ) Bb  bm#;`QmT Q7  019 @T`2b2Mi#H2 ;`QmTX*?BiBMǶb MmK#2` b  7mM+iBQM
um GBM; ULMDBM; lMBp2`bBivV
#bi`+i, h"

JQMQiQMQmb #2iiBM; bi`i2;B2b BM r`T2/ +bBMQb:2Q`;2 "`KTHBb U*?BM2b2 +/2Kv Q7 a+B2M+2bV
amTTQb2 i?i vQm FMQr i?2 +bBMQ `QmH2ii2 Bb `B;;2/ M/ i?2`2 Bb M BK#HM+2 Q7 `2/f#H+F Qmi@
+QK2b- i H2bi BM i?2 HBKBiX h?2M i?2`2 Bb  bi`i2;v r?B+? QMHv #2ib QM `2/ Q` QMHv #2ib QM #H+Fr?B+? ;m`Mi22b vQm mM#QmM/2/ T`Q}iX JQ`2 ;2M2`HHv- bmTTQb2 i?i vQm ?p2 i?2 `2bi`B+iBQM i?ivQm +MMQi #2i i?2 /QHH`b vQm 2`M #v #2iiBM; QM `2/- iQ #2i QM #H+F M/ pB+2@p2`bX AM i?2 bK2
+bBMQ i?2`2 Bb  bm++2bb7mH bi`i2;v Q7 i?Bb FBM/- r?B+? /Q2b MQi /2T2M/ QM r?2`2 i?2 #Bb Bb U`2/
Q` #H+FV Q` 2p2M i?2 /2;`22 Q7 i?2 #Bb UB2 ?Qr 7` 7`QK Rfk 2+? Qmi+QK2 7`2[m2M+v +M ;2i BM i?2
HBKBiVXaQK2iBK2b +bBMQb `2 `B;;2/ BM KQ`2 bm#iH2 rvb- r?BH2 biBb7vBM; HH +QKKQMHv mb2/ Hrb Q7 H`;2
MmK#2`b HBF2 i?2 `2HiBp2 7`2[m2M+v HBKBi Q7 2+? Qmi+QK2 i2M/BM; iQ RfkX h?2M `2 i?2`2 bBKTH2rBMMBM; bi`i2;B2b\ q2 bim/v i?Bb [m2biBQM 7`QK M H;Q`Bi?KB+ T2`bT2+iBp2- r?B+? Bb  Mim`H
TT`Q+? bBM+2 Bi Bb `2bQM#H2 iQ 2tT2+i i?i  bi`i2;v Bb T`Q;`KK#H2 BM  +QKTmi2`X q2 b?Qr
i?i BM i?2 +b2 Q7 T`Q;`KK#H2 bi`i2;B2b i?2 Mbr2` Bb TQbBiBp2 r?BH2 BM i?2 +b2 Q7 +QmMi#H2
KBtim`2b Q7 T`Q;`KK#H2 bi`i2;B2b i?2 Mbr2` Bb M2;iBp2X
h?Bb iHF Bb #b2/ QM i?2 7QHHQrBM; DQBMi rQ`F rBi? 6M; LM M/ M/v G2rBb@Sv2,?iiTb,ff`tBpXQ`;fT/7fR3ydXy9ej8XT/7*QMiBMmQmb pHmiBQMb QM [mbB@SQHBb? bT+2b
Jii?2r /2 "`2+?i UEvQiQ lMBp2`bBivVjZmbB@SQHBb? bT+2b `2  +Hbb Q7 +QmMi#Hv #b2/ iQTQHQ;B+H bT+2b r?B+? ;2M2`HBx2 #Qi? SQHBb?
bT+2b Ur?B+? `2 BKTQ`iMi BM MHvbBb M/ K2bm`2 i?2Q`vV M/ !@+QMiBMmQmb /QKBMb Ur?B+? `2
BKTQ`iMi BM i?2Q`2iB+H +QKTmi2` b+B2M+2 M/ H;2#`VX  pHmiBQM Bb  T`iB+mH` FBM/ Q7 KTTBM;
7`QK i?2 QT2M bm#b2ib Q7  iQTQHQ;B+H bT+2 iQ i?2 `2H MmK#2`b- r?B+? b?`2b KMv T`QT2`iB2b Q7 
K2bm`2X
AM i?Bb iHF- r2 rBHH ;Bp2  #`B27 BMi`Q/m+iBQM iQ [mbB@SQHBb? bT+2b M/ T`2b2Mi bQK2 #bB+ `2@
bmHib +QM+2`MBM; +QMiBMmQmb pHmiBQMb QM [mbB@SQHBb? bT+2bX 1p2`v "Q`2H K2bm`2 `2bi`B+ib iQ 
+QMiBMmQmb pHmiBQM- M/ +QMp2`b2Hv 2p2`v UHQ+HHv }MBi2V +QMiBMmQmb pHmiBQM QM  [mbB@SQHBb?
bT+2 2ti2M/b UmMB[m2HvV iQ  "Q`2H K2bm`2X 6m`i?2`KQ`2- i?2 bT+2 Q7 +QMiBMmQmb pHmiBQMb QM [mbB@SQHBb? bT+2 Bb ;BM  [mbB@SQHBb? bT+2 r?2M ;Bp2M i?2 r2F iQTQHQ;vX*QKTmi2`@bbBbi2/ T`QQ7b pB BMi2`pH `Bi?K2iB+, BMi`Q/m+iBQM M/ TTHB+iBQMb
hQKQvmFB JBvDB UJ2BDB lMBp2`bBivV
AM i?Bb iHF- +QKTmi2`@bbBbi2/ T`QQ7b mbBM; ~QiBM;@TQBMi `Bi?K2iB+ `2 /Bb+mbb2/ 7`QK  pB2rTQBMi
Q7 TTHB2/ MHvbBbX  #bB+ bi`i2;v Q7 i?2 T`QQ7 Bb iQ p2`B7v i?2 2tBbi2M+2 Q7 i?2 i`m2 bQHmiBQM
M2` M TT`QtBKi2 bQHmiBQM r?B+? Bb +QKTmi2/ #v  mbmH MmK2`B+H K2i?Q/X AMi2`pH `Bi?K2iB+
THvb  7mM/K2MiH `QH2 BM i?2 p2`B}+iBQM K2i?Q/X Ai `2im`Mb M BMi2`pH r?B+? 2M+HQb2b i?2 i`m2
pHm2 Q7 `Bi?K2iB+ QT2`iBQM- iFBM; HH i?2 `QmM/BM; 2``Q`b BMiQ ++QmMiX PM2 +M mb2 +QKTmi2`
iQ i2bi r?2i?2`  bm{+B2Mi +QM/BiBQM Q7 bQK2 }t2/@TQBMi i?2Q`2K Bb biBb}2/X am+? p2`B}+iBQM
K2i?Q/b `2 TTHB2/ iQ KMv T`Q#H2Kb `BbBM; BM /vMKB+H bvbi2Kb- T`iBH /Bz2`2MiBH 2[miBQMb+QKTmiiBQMH ;2QK2i`v- 2i+X h?Bb iHF +QMbBbib Q7 irQ T`ibX AM S`i R-  #`B27 Qp2`pB2r Q7 bim/B2b
Q7 p2`B}+iBQM K2i?Q/b #b2/ QM BMi2`pH `Bi?K2iB+ Bb T`QpB/2/- M/ bQK2 i2+?MB[m2b Q7 bQHpBM;}MBi2 /BK2MbBQMH T`Q#H2Kb `2 2tTHBM2/X 6Q` BMbiM+2- i?2 BMi2`pH L2riQM K2i?Q/ Bb  biM/`/K2i?Q/ 7Q` bQHpBM; MQMHBM2` 2[miBQMb- M/ GQ?M2`Ƕb K2i?Q/ Bb TTHB2/ iQ M BMBiBH pHm2 T`Q#H2K
Q7 Q`/BM`v /Bz2`2MiBH 2[miBQMbX AM S`i k- M TTHB+iBQM iQ  T`Q#H2K `BbBM; 7`QK Ki?2KiB+H~mB/ /vMKB+b Bb T`2b2Mi2/X aQK2 #QmM/`v pHm2 T`Q#H2K 7Q` Q`/BM`v /Bz2`2MiBH 2[miBQMb Bb
bQHp2/ pB i?2 b?QQiBM; K2i?Q/ rBi? i?2 p2`B}+iBQM K2i?Q/X.2+BbBQM S`Q#H2Kb BM Ji`Bt a2KB;`QmTb, H;Q`Bi?KB+ /2+B/#BHBiv M/ +QKTmiiBQMH+QKTH2tBiv
A;Q` SQiTQp UlMBp2`bBiv Q7 GBp2`TQQHVh?2 #bi`+ib Q7 SQiTQpǶb iHF M/ i?2 +QMi`B#mi2/ iHFb `2 //2/ 7`QK i?2 M2ti T;2X

9

Decision Problems in Matrix Semigroups:
algorithmic decidability and computational complexity
Igor Potapov ⇤A large number of naturally defined matrix problems are still unanswered despite the long history of matrix theory. Originally in Arthur Cayley’s “A Memoiron the Theory of Matrices” in 1858, the notion of a matrix arises naturally fromabbreviated notations for a set of linear equations where he also defined associated operation of multiplication, notions of determinant, inverse matrices, etc.
Nowadays questions on matrices and matrix problems emerge in much larger
context as they appear in the analysis of various digital processes, verification
problems [18], in the context of control theory questions [2]. Moreover problems
on matrix products have been associated with several long standing open problems in algebraic number theory and transcendence theory, Nash equilibria, in
the theory of joint spectral radius and its applications [9, 14, 18, 19].
Many simply formulated and elementary problems for matrices are inherently difficult to solve even in dimension two, and most of these problems become
undecidable in general starting from dimension three or four [6, 4, 7, 9, 10, 20].
Only few decidability results are known so far, see for example [1, 12, 5, 11, 13,
21, 22, 23].
Let us given a finite set of square matrices (known as a generator) which
is forming a multiplicative semigroup S. The classical computational problems
for matrix semigroups are:
• Membership (Decide whether a given matrix M belong to a semigroup S)
and two special cases such as: Identity (i.e. if M is the identity matrix)
and Mortality (i.e. if M is the zero matrix) problems• Vector reachability (Decide for a given vectors u and v whether exist amatrix M in S such that M · u = v)
• Scalar reachability (Decide for a given vectors u, v and a scalar L whether
exist a matrix M in S such that u · M · v=L)
• Freeness (Decide whether every matrix product in S is unique, i.e. whether
it is a code) and some variants of the freeness such as finite freeness problem, the recurrent matrix problem, the unique⇤ DepartmentofComputerpotapov@liverpool.ac.uk.

Science,1

UniversityofLiverpool,

Email:

• factorizability problem, vector freeness problem, vector ambiguity problems, etc.
The undecidability proofs in matrix semigroups are mainly based on various techniques and methods for embedding universal computations into matrix
products. The case of dimension two is the most intriguing since there is someevidence that if these problems are undecidable, then this cannot be proved
directly using previously known constructions. Due to a severe lack of methods
and techniques the status of decision problems for 2 ⇥ 2 matrices (like membership, vector reachability, freeness) is remaining to be a long standing open
problem not only for matrices over algebraic, complex, rational numbers but
also for integer matrices.
Recently, a new approach of translating numerical problems of 2 ⇥ 2 integer
matrices into variety of combinatorial and computational problems on words
and automata over group alphabet and studying their transformations as specificrewriting systems [11, 13] have led to a few results on decidability and complexity
for some subclasses:• The membership problem for 2 ⇥ 2 nonsingular integer matrices is decidable [23]. The algorithm relies on a translation of numerical problems on
matrices into combinatorial problems on words. It also makes use of somealgebraic properties of well-known subgroups of GL(2, Z) and various newtechniques and constructions that help to convert matrix equations into
the emptiness problem for intersection of regular languages.
• The Identity problem in SL(2, Z) is NP-complete [8, 5]. Our NP algorithm is based on various new techniques that allow us to operate withcompressed word representations of matrices without explicit exponential
expansion.
• The vector reachability problem over a finitely generated semigroup of
matrices from SL(2, Z) and the point to point reachability (over rational
numbers) for fractional linear transformations, where associated matrices
are from SL(2, Z) are decidable [21].
Similar techniques have been applied to show that the freeness problem is co-NPhard [16] as well as to study the complexity of other freeness problems such as
finite freeness problem, the recurrent matrix problem, the unique factorizability
problem, vector freeness problem, vector ambiguity problems, etc [15].
Currently we focus on decidability of matrix problems in the Special Linear
Group in dimension three, 3 ⇥ 3 matrices with determinant one. In the seminal
paper of Paterson in 1970 [20], an injective morphism from pairs of words into
3 ⇥ 3 integral matrices was used to prove the undecidability of the mortality
problem, and later led to many undecidability results of matrix problems indimension three. In [17] it was shown that there is no embedding from pairsof words into 3 ⇥ 3 integral matrices with determinant one, i.e., into SL(3, Z),
which provides strong evidence that computational problems in SL(3, Z) may be2

decidable, as all known undecidability techniques for low-dimensional matrices
are based on encoding of Turing machine computations via Post’s Correspondence Problem (PCP), which cannot be applied in SL(3, Z) following the resultsof [17]. In the case of the PCP encoding, matrix products extended by rightmultiplication correspond to a Turing machine simulation, and the only known
proof alternatives rely on recursively enumerable sets and Hilbert’s Tenth Problem, but provide undecidability for matrix equations of very high dimensions.
[3].

References[1] László Babai, Robert Beals, Jin-yi Cai, Gábor Ivanyos, and Eugene M. Luks.
Multiplicative equations over commuting matrices. In Proceedings of the Seventh Annual ACM-SIAM Symposium on Discrete Algorithms, SODA ’96,
pages 498–507, Philadelphia, PA, USA, 1996. Society for Industrial and Applied Mathematics.
[2] Vincent D. Blondel, John N. Tsitsiklis. A survey of computational complexity results in systems and control. Automatica 36(9): 1249-1274 (2000)[3] Paul Bell, Vesa Halava, Tero Harju, Juhani Karhumki, Igor Potapov: Matrix
Equations and Hilbert’s Tenth Problem. IJAC 18(8): 1231-1241 (2008)[4] Paul C. Bell, Mika Hirvensalo, and Igor Potapov. Mortality for 2x2 matrices
is NP-hard. In Branislav Rovan, Vladimiro Sassone, and Peter Widmayer,
editors, Mathematical Foundations of Computer Science 2012, volume 7464
of Lecture Notes in Computer Science, pages 148–159. Springer Berlin Heidelberg, 2012.
[5] Paul C. Bell, Mika Hirvensalo, and Igor Potapov. The Identity Problem for Matrix Semigroups in SL2(Z) is NP-complete. In Proceedings of
the Twenty-Eighth Annual ACM-SIAM Symposium on Discrete Algorithms,
SODA 2017, Barcelona, Spain, Hotel Porta Fira, January 16-19, pages 187206, 2017.
[6] Paul Bell and Igor Potapov. On undecidability bounds for matrix decision
problems. Theoretical Computer Science, 391(1-2):3–13, 2008.
[7] Paul C. Bell and Igor Potapov. On the undecidability of the identity correspondence problem and its applications for word and matrix semigroups.
Int. J. Found. Comput. Sci., 21(6):963–978, 2010.
[8] Paul C. Bell and Igor Potapov. On the computational complexity of matrix
semigroup problems. Fundam. Inf., 116(1-4):1–13, January 2012.
[9] Vincent D. Blondel, Emmanuel Jeandel, Pascal Koiran, and Natacha Portier.
Decidable and undecidable problems about quantum automata. SIAM J.
Comput., 34(6):1464–1473, June 2005.
3

[10] Julien Cassaigne, Vesa Halava, Tero Harju, and François Nicolas. Tighter
undecidability bounds for matrix mortality, zero-in-the-corner problems, andmore. CoRR, abs/1404.0644, 2014.
[11] Christian Cho↵rut and Juhani Karhumaki. Some decision problems on
integer matrices. RAIRO-Theor. Inf. Appl., 39(1):125–131, 2005.
[12] Esther Galby, Joël Ouaknine, and James Worrell. On Matrix Powering in Low Dimensions. In Ernst W. Mayr and Nicolas Ollinger, editors,
32nd International Symposium on Theoretical Aspects of Computer Science(STACS 2015), volume 30 of Leibniz International Proceedings in Informatics (LIPIcs), pages 329–340, Dagstuhl, Germany, 2015. Schloss Dagstuhl–
Leibniz-Zentrum fuer Informatik.
[13] Yuri Gurevich and Paul Schupp. Membership problem for the modulargroup. SIAM J. Comput., 37(2):425–459, May 2007.
[14] Raphael Jungers. The Joint Spectral Radius. Theory and Applications,Lecture Notes in Control and Information Sciences, Springer, 146pp, 2009[15] Sang-Ki Ko, and Igor Potapov Vector Ambiguity and Freeness Problems inSL(2,Z), Theory and Applications of Models of Computation: 14th Annual
Conference, TAMC 2017, Bern, Switzerland, April 20-22, 2017, Proceedings,
2017, LNCS Springer, 373–388.
[16] Sang-Ki Ko, and Igor Potapov. Matrix Semigroup Freeness Problems inSL(2,Z). SOFSEM 2017: Theory and Practice of Computer Science: 43rd
International Conference on Current Trends in Theory and Practice of Computer Science, 2017, LNCS Springer, 268–279.
[17] Sang-Ki Ko, Reino Niskanen, Igor Potapov: On the Identity Problem for
the Special Linear Group and the Heisenberg Group. ICALP 2018: 132:1132:15[18] Joël Ouaknine, João Sousa Pinto, and James Worrell. On termination of
integer linear loops. In Proceedings of the Twenty-Sixth Annual ACM-SIAM
Symposium on Discrete Algorithms, SODA ’15, pages 957–969. SIAM, 2015.
[19] Joël Ouaknine and James Worrell. On the positivity problem for simple
linear recurrence sequences,. In Automata, Languages, and Programming 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July
8-11, 2014, Proceedings, Part II, pages 318–329, 2014.
[20] M. S. Paterson. Unsolvability in 3x3 matrices. Studies in Applied Mathematics, 49(1):pp.105–107, 1970.
[21] Igor Potapov and Pavel Semukhin. Vector reachability problem in SL(2,Z). MFCS 2016. 84:1-84:14, LIPICS, 20164

[22] Igor Potapov, Pavel Semukhin: Membership Problem in GL(2, Z) Extended
by Singular Matrices. MFCS 2017: 44:1-44:13[23] Igor Potapov and Pavel Semukhin. Decidability of the membership problem
for 2 x 2 integer matrices. In Proceedings of the Twenty-Eighth Annual ACMSIAM Symposium on Discrete Algorithms, SODA 2017, Barcelona, Spain,
Hotel Porta Fira, January 16-19, pages 170–186, 2017.

5

Bar induction and bar recursion with respect tocontinuity on Baire space
Makoto Fujiwara
Waseda Institute for Advanced Study, Waseda University

Bar induction is originally discussed by L. E. J. Brouwer under the nameof “bar theorem” in his intuitionistic mathematics but first formalized by
S. C. Kleene probably in late 1950’s. On the other hand, in his posthumously published paper [1], C. Spector introduced a principle so-called “barrecursion” and gave a consistency proof of classical analysis by extending K.
Gödel’s consistency proof of Peano arithmetic by using the so-called Dialectica interpretation. As already mentioned in [1], bar recursion is an analogueof bar induction in the sense that bar recursion is a principle of definition
and bar induction is a corresponding principle of proof. In particular, bar
induction of type N (namely, formalized Brouwer’s bar theorem) is briefly
compared with bar recursion in an intuitionistic setting (namely, in the presence of continuity principle) in [1, Section 6 with footnote 5 and 6 written
by G. Kreisel]. However, the exact relation between them from the purely
constructive point of view is still unknown.
In this talk, we systematically study the relation between several formsof bar induction of type N and bar recursion for continuous functions of type
NN → N, which is classically valid while bar recursion in general is not so.
Among other things, we show that the existence of bar recursor for continuous functions with continuous modulus of type NN → N is derived from thedecidable bar induction of type N over the extensional versions of intuitionistic arithmetic in all finite types with the axiom scheme of countable choice.
In addition, the converse is also the case over that system augmented withthe characteristic principles of the Dialectica interpretation.
This is a joint work with Tatsuji Kawai (Japan Advanced Institute of
Science and Technology).

References[1] C. Spector, Provably recursive functionals of analysis: a consistency
proof of analysis by an extension of principles in current intuitionistic mathematics. In F. D. E. Dekker, editor, Recursive Function Theory: Proceedings of Symposia in Pure Mathematics, volume 5, pp. 1–27.
American Mathematical Society, Providence, Rhode Island, 1962.
1

Independent distributions on amulti-branching AND-OR tree of height 2(a joint work with Mika Shigemizu and Koki Usami)

Toshio Suzuki∗aa Tokyo Metropolitan University, Japan

We investigate an AND-OR tree T of height h and a probability distribution d on the truth assignments to the leaves. The cost denotes the expected
number of leaves probed during the comuptation. If an algorithm is a minimizer of the cost among all algorithms being considerd then it is called an
optimal algorithm (with respect to d). The following is a known result.
- (Tarsi,J.ACM, 1983) If d is an independent and identical distribution(IID) such that the probability of a leaf having value 0 ̸= 0, 1 then (under acertain assumptions) there exists an optimal algorithm that is depth-first.
Depth-first algorithms have an advantage that they are compatible withinduction on subtrees. We investigate the case where d is an independent
distribution (ID) and the probability depends on each leaf. The following
are known results.
- (S.,2018) If h ≥ 3 then Tarsi-type result does not hold.
- (S.,2018) If T is complete binary and h = 2 then Tarsi-type result holds.
We ask whether Tarsi-type result holds in the case of h = 2. Here, a childnode of the root is either an OR-gate or a leaf: The number of child nodesof an internal node is arbitrary, and depends on an internal node.
- (Main result) If h = 2 then Tarsi-type result holds.
Our strategy of the proof is to reduce the problem to the case of directionalalgorithms. We discuss why our proof does not apply to height 3 trees.

References[1] Mika Shigemizu, Toshio Suzuki and Koki Usami. Independent distributions on a multi-branching AND-OR tree of height 2. Preprint,
arXiv:1804.06601[cs.DS] (2018).
[2] Toshio Suzuki. Non-Depth-First Search against an Independent Distribution on a Balanced AND-OR Tree. To appear in: Inform. Process.
Lett., 139 (2018) 13–17.
∗

E-mail: toshio-suzuki@tmu.ac.jp Partially supported by JSPS KAKENHI 16K05255.

Reverse mathematics of the �nite downwards closed
subsets of Nk ordered by inclusion
Florian Pelupessy
The following was conjectured by Hatzikiriakou and Simpson in Remark 6.2 in [1].
De�nition 1 We order k-tuples coordinatewise.
Theorem 2 RCA0 proves that the following are equivalent:!

1. ! ! is well founded,
2. For every k: the �nite downwards closed subsets of Nk , ordered by inclusion, are a well partial
order.
We con�rm that this is the case, also with RCA⇤ as base theory.
0

References[1] K. Hatzikiriakou and S. G. Simpson, Reverse mathematics, Young diagrams, and the ascending chain condition,
Journal of Symbolic Logic 82 (2017): 576-589.
[2] F. Pelupessy, Reverse mathematics of the �nite downwards closed subsets of Nk ordered by inclusion and adjacentRamsey for �xed dimension, Mathematical Logic Quarterly 64: 178-182.

On one-variable modal µ-calculus
Misato Nakabayashi∗
A Joint work with Wenjuan Li†and Kazuyuki Tanaka‡
Modal µ-calculus, introduced by Kozen, is an extension of modal propositional logic by adding agreatest fixpoint operator µ and a least fixpoint operators ν. It is well suited for specifying properties oftransition systems, and closely related to tree automata and parity games.
A fundamental issue on modal µ-calculus is the strictness of alternation hierarchy of the Lµ -formulas,which are classified by their alternation depth, namely, the number of alternating blocks of µ and ν.
Roughly speaking, the class Σµ0 = Πµ0 is the class of Lµ -formulas with no fixed-point operations; Σµn+1(resp. Πµn+1 ) is the closure of Σµn and Πµn under the composition (i.e., substitution) and µ (resp. ν). A
classical result by Rabin implies that ∆µ2 (= Σµ2 ∩ Πµ2 ) is equal to the compositions of Σµ1 and Πµ1 , which
may also be represented by one-variable formulas.
In this talk, we first show the relationship between one-variable Lµ -formulas and weak alternating tree
automata. An alternating tree automaton A = (A, Q, qI , δ, Ω) with a priority function Ω : Q → {0, . . . , n}is said to be weak if δ has the following additional property:
for all q ∈ Q and a ∈ A, if q ′ occurs in δ(q, a), then Ω(q ′ ) ≤ Ω(q).
Then, we have
Theorem There is an eﬀective translation procedure between a one-variable Lµ -formula ϕ and a weakalternating tree automaton A so that for all finitely branching transition system (S, s),(S, s) |= ϕ ⇐⇒ (S, s) ∈ L(A).
Furthermore, the alternation depth of a one-variable Lµ -formula ϕ corresponds to the number ofthe priorities of the associated automaton A. Therefore, we conclude the strictness of the alternation
hierarchy of one-variable Lµ -formulas within ∆µ2 from the strictness of the hierarchy of weak alternating
tree automata first proved by Mostowski.
Next, we consider infinitely branching transition systems, or especially recursively presented transition
systems (RPTS). Bradfield [1] adapted Lubarsky’s alternation hierarchy of arithmetic µ-calculus (ΣAµ
n ,
µ
Aµ
ΠAµ
n ) to show that for Lµ -formula ϕ ∈ Σn , the denotation ||ϕ|| in any RPTS is a Σn definable set of
integers, and conversely, for any arithmetic µ-calculus formula Φ ∈ ΣAµn , there is an RPTS R and an
Lµ -formula ϕ ∈ Σµn such that ||Φ|| is definable by ϕ over R. Thus, ∆µ2 in RPTS’s corresponds to theclass of sets S of integers such that both S and its complement are definable by a Σ11 -monotone operator.
Therefore, in RPTS’s, ∆µ2 is not equal to the compositions of Σµ1 and Πµ1 , which corresponds to thecompositions of Π11 and Σ11 in integers.
Finally, we introduce the transfinite extension of the hierarchy of one-variable modal µ-calculus, andshow that it exhausts ∆µ2 in RPTS’s.

References[1] J.C. Bradfield, The modal µ-calculus hierarchy is strict. Theoret. Comput. Sci. 195 (1998), 133-153.
∗

Mathematical Institute, Tohoku University. E-mail: misato.nakabayashi@gmail.com
School of Mathematics, Nanyang Technological University. E-mail: wenjuan.li1701@gmail.com‡
Mathematical Institute, Tohoku University. E-mail: tanaka.math@tohoku.ac.jp†

 hlhP_AG PL :J1@h>1P_1hA* S_P""AGAhu L.
G:P_Ah>JA* _L.PJL1aa
E1La>A JAu"1

A rBHH ;Bp2  imiQ`BH QM ;K2@i?2Q`2iB+ T`Q##BHBiv M/ H;Q`Bi?KB+ `M/QKM2bbX
S`Q##BHBiv Bb  bi`M;2 MQiBQM- M/ Bib 7Q`KmHiBQM M/ BMi2`T`2iiBQM Bb biBHH
QM;QBM;X  Ki?2KiB+H 7Q`KmHiBQM Q7 i?2 MQiBQM Q7 T`Q##BHBiv ?b #22M ;Bp2M#v EQHKQ;Q`Qp- r?B+? r2 +HH K2bm`2@i?2Q`2iB+ T`Q##BHBiv i?2Q`vX ++Q`/BM; iQ
i?2 i?2Q`v- T`Q##BHBiv Bb bQK2i?BM; rBi? r?B+? bQK2 tBQKb ?QH/X h?2`2 `2
bQK2 Hi2`MiBp2b bm+? b i?2 i?2Q`v Q7 +QHH2+iBp2b #v pQM JBb2b M/ H;Q`Bi?KB+
T`Q##BHBiv #v aQHQKQMQzX AM #Qi? i?2Q`B2b- `M/QK b2[m2M+2b `2 2bb2MiBH MQiBQMbX
h?2 KQbi r2HH@FMQrM MQiBQM Q7 `M/QKM2bb Bb #v J`iBM@Gƺ7X M BM}MBi2 #BM`v
b2[m2M+2 Bb JG@`M/QK B7 Bi Bb  ivTB+H b2[m2M+2 M/ Bi pQB/b HH 2z2+iBp2 MmHH
b2ibX JG@`M/QKM2bb +M #2 +?`+i2`Bx2/ #v mMT`2/B+i#BHBiv- bv- `M/QK B7 Mv
2z2+iBp2 #2iiBM; bi`i2;v /Q2b MQi bm++22/ HQM; i?2 b2[m2M+2X HbQ #v BM+QK@
T`2bbB#BHBiv- `M/QK B7 2p2`v BMBiBH b2;K2Mi /Q2b MQi ?p2 b?Q`i /2b+`BTiBQMbX q2?p2 BMimBiBQM i?i `M/QK B7 ivTB+H- mMT`2/B+i#H2- Q` +QKTH2tX PM2 Q7 BMi2`2biBM;
i?BM;b #Qmi i?2 i?2Q`v Q7 `M/QKM2bb Bb i?i r2 +M Ki?2KiB+HHv T`Qp2 bm+?
i?BM;bXh?2 i?2Q`v Q7 `M/QKM2bb ?b  bi`QM; `2HiBQM rBi? +QKTmi#BHBiv i?2Q`vX*?BiBMǶb ⌦ Bb  H27i@+X2X `2H- r?B+? K2Mb Bi ?b  +QKTmi#H2 TT`QtBKiBQM 7`QK
#2HQr- M/ Bb JG@`M/QK i i?2 bK2 iBK2X aQHQpv `2/m+B#BHBiv Bb  MQiBQM iQ +QK@T`2 irQ H27i@+X2X `2Hb BM i?2 b2Mb2 Q7 TT`QtBK#BHBivX h?2 iQT 2H2K2Mi Q7 aQHQpv/2;`22b BM H27i@+X2X `2Hb Bb 2t+iHv i?2 +Hbb Q7 H27i@+X2X JG@`M/QK `2HbX h?2`2 `2KMv bii2K2Mib #Qmi i?2 `2HiBQM #2ir22M `M/QKM2bb M/ +QKTmi#BHBiv- r?B+?
QM2 +M MQi bii2 BM i?2 K2bm`2@i?2Q`2iB+ T`Q##BHBivX:K2@T`Q##BHBiv T`Q##BHBiv ?b MQi?2` BMi2`T`2iiBQM Q7 T`Q##BHBiv- M/ Bi
BMi2`+ib rBi? i?2 i?2Q`v Q7 `M/QKM2bbX amTTQb2 QM2 ~BTb  +QBM (2n + 1)@iBK2bX
h?2M- #v bvKK2i`v- i?2 2p2Mi i?i i?2 MmK#2` Q7 ?2/b Bb H`;2` i?M Q` 2[mH
iQ n + 1 ?b T`Q##BHBiv 12 X AM K2bm`2@i?2Q`2iB+ T`Q##BHBiv- i?Bb Bb #2+mb2 i?2
MmK#2` Q7 TQbbB#H2 2[mHHv@HBF2Hv Qmi+QK2b Bb 2n M/ i?2 MmK#2` Q7 i?2 /2bB`#H2
Qmi+QK2b Bb 2t+iHv  ?H7 Q7 BiX oBHH2 b?Qr2/ i?i i?2`2 Bb  #2iiBM; bi`i2;v bm+?
i?i QM2 +M /Qm#H2 i?2B` +TBiH r?2M i?2 /2bB`#H2 2p2Mi Q++m`bX h?2 QM2 b?QmH/
F22T i?2B` +TBiH MQM@M2;iBp2 HQM; Mv Qmi+QK2X h?2 `iBQ Q7 i?2 }MH +TBiHM/ i?2 BMBiBH +TBiH Bb MQi?BM; #mi ;K2@i?2Q`2iB+ T`Q##BHBivX
Mv i?2Q`2K BM K2bm`2@i?2Q`2iB+ T`Q##BHBiv b?QmH/ ?p2  ;K2@i?2Q`2iB++QmMi2`T`i T`QQ7- r?B+? `Qm;?Hv bvBM; mb2b QMHv K`iBM;H2bX _2r`BiBM; T`QQ7b
pB K`iBM;H2b KF2b Bi 2bv iQ MHvx2 +QKTmi#BHBiv Q7 K`iBM;H2bX _Qm;?Hv
bvBM;- r2 +M b2T`i2 i?2 T`QQ7 BMiQ +QKTmi#BHBiv T`i M/ T`Q##BHBiv T`iX
PM2 bm+? 2tKTH2 rBHH #2 ;Bp2M BM Kv MQi?2` iHFX
UEX JBv#2V J2BDB lMBp2`bBiv- CTM
1@KBH //`2bb, `2b2`+?!F2Mb?BXKBv#2XMK2

R

Some results of pS-reducibility(a joint work with Toshio Suzuki and Masahiro Kumabe)

YUKI MIZUSAWA∗aa Tokyo Metropolitan University, Japan

Solovay reducibility is well-known notion in theory of algorithmic randomness.We define pS-reducibility as a generalization of Solovay reducibility.
We have following results
1. Solovay reducible ⇒ pS-reducible
2. ¬ [pS-reducible ⇒ Solovay reducible]
3. pS-reducible ⇒ wtt-reducible
4. ¬ [wtt-reducible ⇒ pS-reducible]
5. pS-reducibility is standard reducibility.
We also study relationship between reducibility and continuity in analytics and have some results.

References[1] Rodney G. Downey and Denis R. Hirschfeldt. Algorithmic Randomness
and Complexity,Theory and Applications of Computability. SpringerVerlag New York,2010.

∗

E-mail: houji6@gmail.com

ERDÖS-FELLER-KOLMOGOROV-PETROWSKY LAW OF THE
ITERATED LOGARITHM
KENSHI MIYABE

A fundamental results in measure-theoretic probability is the strong law of large
numbers (SLLN) shown by Borel (1901). Let Xi be i.i.d. random variables with!n
1
Sn
P (Xi = 1) = P (Xi = −1) = . Let Sn = i=1 Xi . Then,→ 0 almost surely.
2n
A more precise version was given by Khintchine (1924). With the same assumption, we haveSn
lim sup √=1n→∞
2n ln ln nalmost surely. This is called the law of the iterated logarithm (LIL).
Further precise version was also known as the Erdös-Feller-Kolmogorov-Petrowsky
law of the iterated logarithm (EFKP-LIL). Let ψ be a positive increasing function.
Let
" ∞
ψ(λ)
I(ψ) =exp(−ψ(λ)2 /2)dλλ
1
If I(ψ) < ∞, then√Sn < nψ(n)for almost all n almost surely. If I(ψ) = ∞, then√Sn > nψ(n)for infinitely many n almost surely. We call the former the validity, and the latter
sharpness.
We restrict ψ to be computable. Notice that I(ψ) may not be computable even
if it converges, and I(ψ) can grow more slowly than any computable function. The
main claim in this talk is that computable randomness is suﬃcient to hold EFKPLIL, but Schnorr randomness is not suﬃcient. In fact, the speed of divergence orconvergence of I(ψ) exactly corresponds to the bound of the speed of divergence ofmartingales.
The known proofs of EFKP-LIL for fair-coin tossing are fairy complicated.
The EFKP-LIL also holds for Brownian motion, whose proof uses the OrnsteinUhlenbeck process and its scale function. The proof can be naturally converted
to a game-theoretic proof. Finally, we construct a computable function ψ and a
Schnorr random sequence with some properties as usual in the theory of randomness.
(K. Miyabe) Meiji University, Japan
E-mail address: research@kenshi.miyabe.name1Approaching the first-order strength of
Hindman’s theorem
Keita Yokoyama⋆
Japan Advanced Institute of Science and Technology
y-keita@jaist.ac.jp

The reverse mathematical study of Hindman’s theorem is initiated by Blass,
Hirst and Simpson [1]. They showed that Hindman’s theorem is provable from
ACA0 + , and it implies ACA0 over RCA0 . Since then, many people tried to decide
the exact strength with many diﬀerent approaches, but it is still open whether
Hindman’s theorem is equivalent to one of them or strictly in between. In thistalk, we will try to calibrate the first-order strength of HIndman’s theorem.
Hindman’s theorem is a Ramsey type theorem, and thus its first-order part canbe approximated by some density style statement as in [2, 3]. We will give acharacterization of the first-order part of Hindman’s theorem with this idea, andthen examine what is needed to prove the density style variation of Hindman’s
theorem. This is a joint work with Paul-Elliot Anglès d’Auriac.

References
1. Andreas R. Blass, Jeﬀry L. Hirst, and Stephen G. Simpson. Logical analysis of sometheorems of combinatorics and topological dynamics. In Logic and combinatorics(Arcata, Calif., 1985), volume 65 of Contemp. Math., pages 125–156. Amer. Math.
Soc., Providence, RI, 1987.
2. Andrey Bovykin and Andreas Weiermann. The strength of infinitary Ramseyan
principles can be accessed by their densities. Ann. Pure Appl. Logic, 168(9):1700–
1709, 2017.
3. Ludovic Patey and Keita Yokoyama. The proof-theoretic strength of Ramsey’s
theorem for pairs and two colors. Adv. Math., 330:1034–1070, 2018.

⋆

This work is partially supported by JSPS KAKENHI (grant numbers 16K17640 and
15H03634) and JSPS Core-to-Core Program (A. Advanced Research Networks).

On proving parameterized polynomial time computability ofcompositions of fundamental functions
Hiromichi Hamamoto, Akitoshi Kawamura, Martin Ziegler
In a standard formulation of real complexity theory [1], the complexity of realfunctions is discussed in oracle machine model and is measured in terms of therequired precision 𝑛. This notion of complexity can only be applied to functions
whose domain is compact, because the time for reading its arguments must be finite.
To differentiate more accurately the complexity of reading or outputting and thecomputing procedure itself, parametrized complexity has been recently introduced[2]. In this framework, the domain of a real function is a set of tuples of real
numbers 𝒙 and integer parameters 𝒌, for example {(𝑥, 𝑘) ∈ ℝ × ℕ | 𝑥 ∈ [−2𝑘 , 2𝑘 ]},and the complexity is measured in terms of 𝑛 and 𝒌. As an important theorem, theclosure property of parameterized polynomial time computable functions undercomposition is proved by simply connecting Turing machines computing eachsubfunction. Moreover, fundamental functions, such as addition, multiplication,
exponential and reciprocal, are proved to be parameterized polynomial timecomputable on appropriate domains.
Then as a natural interest, we want to prove parameterized polynomial timecomputability of functions, such as 𝑓(𝑥) = 1/𝑒 𝑥 , which can be expressed ascomposition of reciprocal and exponential functions. To grasp accuratelyparameterized polynomial time computability of such a function, each subfunction
and their composition must be defined more carefully.

In this talk, first I will give asound definition of composition of parameterized real functions. Then after provingsome properties and theorems about those functions, I will introduce output-sensitive
polynomial time computability in order to more accurately characterize parameterized
polynomial time computability of composition of reciprocal.

Reference[1] Ker-I Ko. Complexity Theory of Real Functions. Birkhäuser Boston, 1991.
[2] Akitoshi Kawamura, Martin Ziegler. Invitation to Real Complexity Theory:
Algorithmic Foundations to Reliable Numerics with Bit-Costs. In WAAC, 2015.

Computable analysis and computability in linear time
Akitoshi Kawamura1 , Florian Steinberg2 , and Holger Thies3
1

Kyushu University

2

INRIA

3

University of Tokyo

For many applications, such as for instance computable analysis [5], one is interested incomputing functions where input and output are not finite strings but functions themselves.
That is, computing operators of type B ! B where B denotes the Baire space of all total
functions ' : {0, 1}⇤ ! {0, 1}⇤ on finite binary strings. The accepted computational model
for such type-2 computations are oracle machines or equivalent models.
Computational complexity theory deals with how efficiently a problem can be solved interms of resources such as time and space. The computationally feasible functions are identified with those functions whose run-time can be bounded by a polynomial. For computations
at type level two the class of basic feasible functionals is widely accepted as the natural classof feasible operations [3, 2].
Instead of only considering feasibility, one is often interested in which operations canbe performed efficiently. A possible notion for efficient computation is computability inlinear time. Already in classical complexity theory, robustness of linear-time computability
under reasonable changes in the computational model is not given [1]. Nonetheless, proofsof linear-time computability are considered highly desirable in applications and there is awell-developed theory for the model of multi-tape Turing machines [4].
In this work, we put forward a complexity class of type-two linear-time. For this definition
to be meaningful, a detailed protocol for oracle interactions has to be fixed. This includes
some choices the defined class is sensible to and we carefully discuss our choices and theirimplications. We further discuss some properties and examples of linear-time and almost
linear-time computable operators and applications to computable analysis.

References[1] Gurevich, Y., and Shelah, S. Nearly linear time. In International Symposium on
Logical Foundations of Computer Science (1989), Springer, pp. 108–118.
[2] Kapron, B. M., and Cook, S. A. A new characterization of type-2 feasibility. SIAM
Journal on Computing 25, 1 (1996), 117–132.
[3] Mehlhorn, K. Polynomial and abstract subrecursive classes. In Proceedings of the sixth
annual ACM symposium on Theory of computing (1974), ACM, pp. 96–109.
[4] Regan, K. W. Machine models and linear time complexity. ACM SIGACT News 24, 3(1993), 5–15.
[5] Weihrauch, K. Computable Analysis. Springer, Berlin/Heidelberg, 2000.

1