Thursday, June 3, 2021
Gabriel Ciobanu (Alexandru Ioan Cuza University of Iași and Romanian Academy (ICS))
Choice principles and infinities for finitely supported structures
Abstract:
Finitely supported structures are related to permutation models of
Zermelo-Fraenkel set theory with atoms (ZFA) and to the theory of
nominal sets. They were originally introduced in 1930s by Fraenkel,
Lindenbaum and Mostowski to prove the independence of the axiom of choice and the other
axioms in ZFA. We use a set theory defined by the axioms of ZFA set
theory extended with an additional axiom for finite support. The
consistency (validity) of choice principles in various models of
Zermelo-Fraenkel set theory (ZF) and of ZFA (including the symmetric
models and the permutation models) was investigated deeply in the last century.
The choice axiom was proved to be independent from the axioms of ZF and
ZFA. In the new theory of finitely supported structures, we analyze the
consistency of various choice principles (and equivalent/related
results), as well as the consistency of results regarding cardinality
and infinity. We prove the inconsistency of choice principles for
finitely supported structures (i.e., their formulations with respect to
the finite support requirement are not valid).
Related to this inconsistency of choice principles, we present some
pairwise non-equivalent definitions for the notion of infinity
(difficult to imagine, we have seven forms of infinity for finitely
supported structures). We compare these forms, and present examples of
atomic sets satisfying a certain form of infinity, while they do not
satisfy others. In particular, we focus on the notion of Dedekind
infinity and on uniformly supported sets.
References:
[1] A. Alexandru, G. Ciobanu,
Foundations of Finitely Supported Structures: a set theoretical viewpoint, Springer, 2020.
Thursday, May 27, 2021
Cătălin Dima (University Paris-Est Créteil)
Rational Synthesis in the Commons with Careless and Careful Agents
Abstract:
Turn-based multi-agent games on graphs are games where the states are controlled by a single
player who decides which edge to follow. Each player has a temporal objective that he tries
to achieve, and one player is the designated `controller', whose objective captures the
desirable outcomes of the whole system. Cooperative rational synthesis is the problem of
computing a Nash equilibrium (w.r.t. the individual temporal objectives) that satisfies the
controller’s objective. In this presentation, we tackle this problem in the context where
each action has a cost or a benefit on one shared common pool energy resource.
The paper investigates the problem of synthesizing the controller such that there exists
an individually rational behavior of all the agents that satisfies the controller's objective
and does not deplete the resource. We consider two types of agents: careless and careful.
Careless agents only care for their temporal objective, while careful agents also pay attention
not to deplete the system's resource. We study the complexity of the problem of cooperative
rational synthesis with parity or Büchi objectives, careful or careless agents, and costs
encoded in binary or unary.
Based on joint work with Rodica Condurache (Alexandru Ioan Cuza University of Iași),
Youssouf Oualhadj (University Paris-Est Créteil) and
Nicolas Troquard (Free University of Bozen-Bolzano).
Thursday, May 20, 2021
Mihai Prunescu (University of Bucharest and IMAR)
Secret multiparty computation in arbitrary rings
Abstract:
Secret Multiparty Computation proves to work in every ring, not necessarily associative,
commutative or with 1. The Berlekamp-Welch algorithm and the Secret Multiparty Computation
with malicious partners prove to work in every field, including the non-commutative fields.
For commutative fields, including those of characteristic 0, I propose a method with division.
Thursday, May 13, 2021
Bruno Dinis (University of Lisbon)
Functional interpretations for nonstandard arithmetic
Abstract:
In the past few years there has been a growing interest in trying to make explicit constructive
aspects of nonstandard methods with the use of functional interpretations.
Functional interpretations are maps of formulas from the language of one theory into the
language of another theory, in such a way that provability is preserved. These interpretations
typically replace logical relations by functional relations. Functional interpretations have
many uses, such as relative consistency results, conservation results and extraction of
computational content from proofs.
After giving a short introduction to nonstandard analysis, I will present several recent
functional interpretations in the context of nonstandard arithmetic as well as some results
that come from these interpretations.
References:
[1] B. van den Berg, E. Briseid, P. Safarik,
A functional
interpretation for nonstandard arithmetic.
Ann. Pure Appl. Logic 163 (2012), no. 12, 1962-1994.
[2] B. Dinis, J. Gaspar, Intuitionistic nonstandard bounded modified realisability and functional
interpretation. Ann. Pure Appl. Logic 169 (2018), no. 5, 392-412.
[3] B. Dinis, J. Gaspar, Hardwiring t-truth in functional interpretations. In preparation.
[4] B. Dinis, É. Miquey, Realizability with stateful computations for nonstandard analysis.
29th EACSL Annual Conference on Computer Science Logic (CSL 2021), 19:1-19:23.
[5] F. Ferreira, J. Gaspar, Nonstandardness
and the bounded functional interpretation.
Ann. Pure Appl. Logic 166 (2015), no. 6, 701-712.
[6] S. Sanders, The unreasonable effectiveness of nonstandard analysis. J. Logic Comput. 30 (2020),
no. 1, 459-524.
Thursday, April 22, 2021
Gabriel Istrate
(West University of Timișoara)
Dorel Lucanu
(Alexandru Ioan Cuza University of Iași)
Gheorghe Ştefănescu (University of Bucharest)
Alexandru Dragomir (University of Bucharest)
Mircea Marin
(West University of Timișoara)
Andrei Sipoș (University of Bucharest)
Mihai Prunescu (University of Bucharest and IMAR)
Pedro Pinto
(Technische Universität Darmstadt)
Horațiu Cheval (University of Bucharest)
Horațiu Cheval (University of Bucharest)
Adriana Stancu (University of Bucharest)
Adriana Stancu (University of Bucharest)
Andrei Sipoș (University of Bucharest and IMAR)
Andrei Sipoș (University of Bucharest and IMAR)
Kernelization, Proof Complexity and Social Choice
Abstract: We display an application of the notions of kernelization and data
reduction from parameterized complexity to proof complexity:
Specifically, we show that the existence of data reduction rules for a
parameterized problem having (a). a small-length reduction chain, and
(b). small-size (extended) Frege proofs certifying the soundness of
reduction steps implies the existence of subexponential size
(extended) Frege proofs for propositional formalizations of the given
problem.
We apply our result to infer the existence of subexponential Frege and
extended Frege proofs for a variety of problems. Improving earlier
results of Aisenberg et al. (ICALP 2015), we show that propositional
formulas expressing (a stronger form of) the Kneser-Lovasz Theorem
have polynomial size Frege proofs for each constant value of the
parameter $k$. Previously only quasipolynomial bounds were known (and
only for the ordinary Kneser-Lovasz Theorem).
Another notable application of our framework is to impossibility
results in computational social choice: we show that, for any fixed
number of agents, propositional translations of the Arrow and
Gibbard-Satterthwaite impossibility theorems have subexponential size
Frege proofs.
This is joint work with Cosmin Bonchiș and Adrian Crăciun.
Thursday, April 15, 2021
(Co)Initial (Co)Algebra Semantics in Matching Logic
Abstract: Matching logic is a unifying foundational logic for defining formal programming
language semantics, which adopts a minimalist design with few primitive constructs
that are enough to express all properties within a variety of logical systems,
including FOL, separation logic, (dependent) type systems, modal
mu-logic, and more.
In this presentation, we will show how the initial algebra semantics and the
final (coinitial) coalgebra semantics are captured as theories in Matching
Logic. The presentation will be examples-based.
This is joint work with Xiaohong Chen and Grigore Roșu.
References:
[1] X. Chen, D. Lucanu, G. Roșu.
Matching logic explained.
Journal of Logical and Algebraic Methods in Programming 120 (2021), 100638.
[2] X. Chen, D. Lucanu, G. Roșu.
Initial algebra semantics in matching logic.
UIUC Technical Report (2020).
Thursday, April 8, 2021
Adaptive Virtual Organisms: A Compositional Model for Complex Hardware-software Binding
Abstract: The relation between a structure and the function it runs is of interest in
many fields, including computer science, biology (organ vs. function) and psychology (body vs. mind).
Our paper addresses this question with reference to computer science recent hardware and
software advances, particularly in areas as Robotics, Self-Adaptive Systems, IoT, CPS,
AI-Hardware, etc.
At the modelling, conceptual level our main contribution is the introduction of the concept
of ``virtual organism" (VO), to populate the intermediary level between reconfigurable hardware
agents and intelligent, adaptive software agents. A virtual organism has a structure,
resembling the hardware capabilities, and it runs low-level functions, implementing the
software requirements. The model is compositional in space (allowing the virtual organisms
to aggregate into larger organisms) and in time (allowing the virtual organisms to get
composed functionalities).
The virtual organisms studied here are in 2D (two dimensions) and their structures are described
by 2D patterns (adding time, we get a 3D model). By reconfiguration, an organism may change
its structure to another structure in the same 2D pattern. We illustrate the VO concept
with a few increasingly more complex VO’s dealing with flow management or a publisher-subscriber
mechanism for handling services. We implemented a simulator for a VO, collecting flow over
a tree-structure (TC-VO), and the quantitative results show reconfigurable structures are
better suited than fixed structures in dynamically changing environments.
Finally, we briefly show how Agapia - a structured parallel, interactive programming language
where dataflow and control flow structures can be freely mixed - may be used for getting
quick implementations for VO’s simulation.
References:
[1] C. I. Păduraru, G. Ştefănescu. Adaptive virtual organisms:
A compositional model for complex hardware-software binding. Fundamenta Informaticae
173, no. 2-3, 139-176, 2020.
Thursday, April 1, 2021
An Introduction to Protocols in Dynamic Epistemic Logic
Abstract: Dynamic epistemic logics are useful in reasoning about knowledge and acts
of learning, seen as epistemic actions. However, not all epistemic actions are allowed to
be executed in an initial epistemic model, and this is where the concept of a protocol
comes in: a protocol stipulates what epistemic actions are allowed to be performed in a
model. The aim of my presentation is to introduce the audience to two accounts of protocols
in DEL: Hoshi's [1], and Wang's [2].
References:
[1] T. Hoshi. Epistemic dynamics and protocol information. PhD thesis, Stanford, CA, USA.
AAI3364501 (2009).
[2] Y. Wang. Epistemic Modelling and Protocol Dynamics. PhD thesis, University of Amsterdam.
(2010).
Thursday, March 25, 2021
Regular matching problems for infinite trees
Abstract: We study the matching problem ``$\exists\sigma:\sigma(L)\subseteq R$?" where
$L,R$ are regular tree languages over finite ranked alphabets $X$ and $\Sigma$ respectively,
and $\sigma$ is a substitution such that $\sigma(x)$ is a set of trees in
$T(\Sigma\cup H)\setminus H$ for all $x\in X$. Here, $H$ denotes a set of holes which are
used to define a concatenation of trees. Conway studied this problem in the special case
for languages of finite words in his classical textbook ``Regular algebra and finite machines"
and showed that if $L$ and $R$ are regular, then the problem ``$\exists \sigma:\forall x\in
X:\sigma(x)\neq\emptyset\wedge\sigma(L)\subseteq R$?" is decidable. Moreover, there are only
finitely many maximal solutions, which are regular and
effectively computable. We extend Conway's results when $L,R$ are regular
languages of finite and infinite trees, and language substitution is applied
inside-out. We show that if $L\subseteq T(X)$ and $R\subseteq T(\Sigma)$ are
regular tree languages then the problem ``$\exists\sigma\forall x\in
X:\sigma(x)\neq\emptyset\wedge\sigma_{io}(L)\subseteq R$?" is decidable.
Moreover, there are only finitely many maximal solutions, which are regular and
effectively computable. The corresponding question for the outside-in extension
$\sigma_{oi}$ remains open, even in the restricted setting of finite trees. Our
main result is the decidability of ``$\exists\sigma:\sigma_{io}(L)\subseteq R$?"
if $R$ is regular and $L$ belongs to a class of tree languages closed under
intersection with regular sets. Such a special case pops up if $L$ is
context-free.
This is joint work with Carlos Camino, Volker Diekert, Besik Dundua and Géraud Sénizergues.
References:
[1] C. Camino, V. Diekert, B. Dundua, M. Marin, G. Sénizergues,
Regular matching problems for infinite trees,
arXiv:2004.09926 [cs.FL], 2021.
Thursday, March 18, 2021
A proof mining case study on the unit interval
Abstract: In 1991, Borwein and Borwein [1] proved the following: if
$L>0$, $f:[0,1] \to [0,1]$ is $L$-Lipschitz, $(x_n)$, $(t_n) \subseteq [0,1]$ are such
that for all $n$, $x_{n+1}=(1-t_n)x_n +t_nf(x_n)$ and there is a $\delta>0$ such that for
all $n$, $t_n \leq \frac{2-\delta}{L+1}$, then the sequence $(x_n)$ converges.
The relevant fact here is that the main argument used in their proof is of a kind that
hasn't been analyzed yet from the point of view of proof mining, and thus it may serve as
an illustrative new case study. We shall present our work on the proof [2], showing how to
extract a uniform and computable rate of metastability for the above family of sequences.
References:
[1] D. Borwein, J. Borwein, Fixed
point iterations for real functions. J. Math. Anal. Appl. 157, no. 1, 112-126, 1991.
[2] A. Sipoș, Rates of metastability for iterations
on the unit interval. arXiv:2008.03934 [math.CA], 2020.
Thursday, March 11, 2021
Exponential Diophantine equations over ${\mathbb Q}$
Abstract: In a previous exposition [1] we have seen that the solvability over ${\mathbb Q}$
is undecidable for systems of exponential Diophantine equations.
We now show that the solvability of individual exponential Diophantine equations is also
undecidable, and this happens as well for some narrower families of exponential Diophantine
equations.
References:
[1] M. Prunescu,
The exponential
Diophantine problem for ${\mathbb Q}$. The Journal of Symbolic Logic,
Volume 85, Issue 2, 671-672, 2020.
Thursday, March 4, 2021
Unwinding of proofs
Abstract: The unwinding of proofs program dates back to Kreisel in the fifties and
rests on the following broad question:
``What more do we know if we have proved a theorem by restricted means than if we
merely know that it is true?"
This research program has since been dubbed proof mining and has been greatly developed during the last
two decades and emerged as a new form of applied proof theory [1,2]. Through the use of proof-theoretical
tools, the proof mining program is concerned with the unveil of hidden finitary and combinatorial content
from proofs that use infinitary noneffective principles.
In this talk, we set out to give a brief introduction to the proof mining program, focusing on the following points:
We finish with a brief discussion of some recent results [5,6].
References:
[1] U. Kohlenbach. Applied Proof Theory: Proof
Interpretations and their Use in Mathematics.
Springer, 2008.
[2] U. Kohlenbach. Proof-theoretic methods
in nonlinear analysis. In M. Viana B. Sirakov, P. Ney de Souza, editor,
Proceedings of the International Congress of Mathematicians - Rio de Janeiro 2018, Vol. II:
Invited lectures, pages 61-82. World Sci. Publ., 2019
[3] F. Ferreira and P. Oliva.
Bounded functional interpretation.
Annals of Pure and Applied Logic, 135:73-112, 2005.
[4] F. Ferreira. Injecting uniformities
into Peano arithmetic.
Annals of Pure and Applied Logic, 157:122-129, 2009.
[5] B. Dinis and P. Pinto. Effective metastability
for a method of alternating resolvents. arXiv:2101.12675 [math.FA], 2021.
[6] U. Kohlenbach and P. Pinto. Quantitative
translations for viscosity approximation methods in hyperbolic spaces. arXiv:2102.03981 [math.FA], 2021.
Thursday, February 25, 2021
Formalizing Gödel's System $T$ in Lean
Abstract: In 1958, Gödel introduced his functional interpretation as a method
of reducing the consistency of first-order arithmetic to that of a quantifier-free system
of primitive recursive functionals of higher type. His work has since enabled other advances
in proof theory, notably the program of proof mining. We give a brief overview of Gödel's
system $T$ and then explore a formalization thereof as a deep embedding in the Lean proof assistant.
References:
[1] mathlib Community, The Lean Mathematical Library,
2019.
Thursday, February 18, 2021
An introduction to Lean
Abstract: Lean is a proof assistant and programming language developed by Leonardo
de Moura at Microsoft Research starting from 2013, based on dependent types and
Coquand's Calculus of Inductive Constructions. It offers typical functional programming
features, as well as a rich and extensible tactic language for writing proofs.
The standard library, mathlib [1], implements an ever-increasing number of definitions
and theorems, from basic facts about real numbers to more advanced topics like algebraic
geometry or category theory, providing a structured framework for formalizing mathematics.
We present an introduction to Lean's theory, methods of writing proofs and then look at
how concrete mathematics is done in mathlib.
References:
[1] mathlib Community, The Lean Mathematical Library,
2019.
Thursday, December 17, 2020
Formal verification of SeL4
Abstract: This presentation introduces the SeL4 system, a microkernel first designed
in Haskell, whose implementation in C has now a full formal proof of correctness. The focus
is on the methods used to abstract the C code implementation into Isabelle/HOL theorems:
syntactic translation, memory model and some abstraction levels added to refine the system
representation, this involves usage of additional tools like a C-to-Isabelle parser and
AutoCorres that will be shortly described.
References:
[1] G. Heiser, The seL4 Microkernel.
An introduction. White paper, The seL4 Foundation, 2020.
AutoCorres tutorial
Abstract: AutoCorres is a tool for abstracting C code into Isabelle/HOL (Isabelle's
specialization in Higher Order Logic). This presentation will introduce some basic proof
rules used in most of the Isabelle's theorems that will be needed to follow some introductory
exercises of using AutoCorres tool with sample C programs. The study cases cover the following
topics: proving correctness of programs with loops and proving statements about programs that
manipulate heap memory.
References:
[1] D. Greenaway, Automated proof-producing
abstraction of C code, PhD Thesis, University of New South Wales, Sidney, 2014.
Thursday, December 3, 2020
A quantitative multi-parameter mean ergodic theorem
Abstract: In [1], Avigad, Gerhardy and Towsner proof-theoretically analyzed
the classical textbook proof due to Riesz of the mean ergodic theorem for Hilbert spaces in
order to extract uniform rates of metastability. In [2], Kohlenbach and Leuștean extracted
rates from a simplified argument of Garrett Birkhoff that applies to uniformly
convex Banach spaces.
What we do here [3] is to analyze another proof of Riesz which was inspired by Birkhoff's one
and which delineates more clearly the role played by uniform convexity.
The corresponding argument has the advantage that it can be used to prove a more general mean
ergodic theorem for a finite family of commuting linear contracting operators.
References:
[1] J. Avigad, P. Gerhardy, H. Towsner, Local stability of ergodic averages. Trans. Amer. Math. Soc. 362,
no. 1, 261-288, 2010.
[2] U. Kohlenbach, L. Leuștean, A quantitative mean ergodic theorem for uniformly convex Banach spaces.
Ergodic Theory Dynam. Systems 29, 1907-1915, 2009.
[3] A. Sipoș, A quantitative multi-parameter mean ergodic theorem, arXiv:2008.03932 [math.DS], 2020.
Thursday, November 5, 2020
What proof mining is about
Abstract: Proof mining is an applied subfield of mathematical logic that aims to analyze
proofs in mainstream mathematics using tools from proof theory. This area has been largely
developed in the last couple of decades by the school of Ulrich Kohlenbach (see e.g.
his monograph [1]). Here, I attempt to gently introduce the field to the working logician,
by adapting my recent articles on The Proof Theory Blog [2,3].
References:
[1] U. Kohlenbach, Applied proof theory: Proof interpretations and their use in mathematics,
Springer Monographs in Mathematics, Springer, 2008.
[2] A. Sipoș,
What proof mining is about, Part I, The Proof Theory Blog, 2020.
[3] A. Sipoș, What
proof mining is about, Part II: Structures and metatheorems, The Proof Theory Blog, 2020.