## Research team

• Guillermo Incatasciato
• Martín Moroni
• Mauricio Tellechea (Assistant Professor)
• Pablo Ventura
• Gonzalo Zigarán

## Recent journal articles

1. X. Caicedo, M. Campercholi, K. A. Kearnes, P. Sánchez Terraf, Á. Szendrei, and D. Vaggione, “Every minimal dual discriminator variety is minimal as a quasivariety,” Algebra universalis 82 (2) p. 36 (2021).

Let $\dagger$ denote the following property of a variety $\mathcal{V}$: \emph{Every subquasivariety of $\mathcal{V}$ is a variety}. In this paper, we prove that every idempotent dual discriminator variety has property $\dagger$ . Property $\dagger$ need not hold for nonidempotent dual discriminator varieties, but $\dagger$ does hold for \emph{minimal} nonidempotent dual discriminator varieties. Combining the results for the idempotent and nonidempotent cases, we obtain that every minimal dual discriminator variety is minimal as a quasivariety

@article{minimal-dual-quasi,
author = {Caicedo, Xavier and Campercholi, Miguel and Kearnes, Keith A. and S{\'a}nchez Terraf, Pedro and Szendrei, {\'A}gnes and Vaggione, Diego},
year = 2021,
title = {Every minimal dual discriminator variety is minimal as a quasivariety},
journal = {Algebra universalis},
month = {Apr},
day = 29,
volume = 82,
number = 2,
pages = 36,
abstract = {Let $\dagger$ denote the following property of a variety $\mathcal{V}$: \emph{Every subquasivariety of $\mathcal{V}$ is a variety}. In this paper, we prove that every idempotent dual discriminator variety has property $\dagger$ . Property $\dagger$ need not hold for nonidempotent dual discriminator varieties, but $\dagger$ does hold for \emph{minimal} nonidempotent dual discriminator varieties. Combining the results for the idempotent and nonidempotent cases, we obtain that every minimal dual discriminator variety is minimal as a quasivariety},
issn = {1420-8911},
doi = {10.1007/s00012-021-00715-8},
url = {https://doi.org/10.1007/s00012-021-00715-8}
}

2. J. Pachl and P. Sánchez Terraf, “Semipullbacks of labelled Markov processes,” Logical Methods in Computer Science 17 (2) (2021).
[ Abstract | BibTeX ]

A \emph{labelled Markov process (LMP)} consists of a measurable space $S$ together with an indexed family of Markov kernels from $S$ to itself. This structure has been used to model probabilistic computations in Computer Science, and one of the main problems in the area is to define and decide whether two LMP $S$ and $S’$ “behave the same”. There are two natural categorical definitions of sameness of behavior: $S$ and $S’$ are \emph{bisimilar} if there exist an LMP $T$ and measure preserving maps forming a diagram of the shape $S\leftarrow T \rightarrow{S’}$; and they are \emph{behaviorally equivalent} if there exist some $U$ and maps forming a dual diagram $S\rightarrow U \leftarrow{S’}$. These two notions differ for general measurable spaces but Edalat proved that they coincide for analytic Borel spaces, showing that from every diagram $S\rightarrow U \leftarrow{S’}$ one can obtain a bisimilarity diagram as above. Moreover, the resulting square of measure preserving maps is commutative (a \emph{semipullback}). In this paper, we extend Edalat’s result to measurable spaces $S$ isomorphic to a universally measurable subset of a Polish space with the trace of the Borel $\sigma$-algebra, using a version of Strassen’s theorem on common extensions of finitely additive measures.

@article{2017arXiv170602801P,
author = {Pachl, Jan and S{\'a}nchez Terraf, Pedro},
title = {Semipullbacks of labelled {M}arkov processes},
journal = {Logical Methods in Computer Science},
volume = 17,
number = 2,
year = 2021,
month = apr,
archiveprefix = {arXiv},
eprint = {1706.02801},
primaryclass = {math.PR},
keywords = {Mathematics - Probability, Computer Science - Logic in Computer Science, 28A35, 28A60, 68Q85, F.4.1, F.1.2},
adsnote = {Provided by the SAO/NASA Astrophysics Data System},
abstract = {A \emph{labelled Markov process (LMP)} consists of a measurable
space $S$ together with an indexed family of Markov kernels from $S$
to itself. This structure has been used to model probabilistic
computations in Computer Science, and one of the main problems in
the area is to define and decide whether two LMP $S$ and $S'$ behave
the same''. There are two natural categorical definitions of
sameness of behavior: $S$ and $S'$ are \emph{bisimilar}
if there exist an LMP $T$ and measure preserving maps
forming a diagram of the shape
$S\leftarrow T \rightarrow{S'}$; and they
are \emph{behaviorally equivalent}
if there exist some $U$ and maps forming a dual diagram
$S\rightarrow U \leftarrow{S'}$.
These two notions differ for general measurable spaces but Edalat
proved that they coincide for analytic Borel spaces, showing that
from every
diagram $S\rightarrow U \leftarrow{S'}$ one can obtain a
bisimilarity diagram as above. Moreover, the resulting square of
measure preserving maps is commutative (a \emph{semipullback}).
In this paper, we extend Edalat's result to measurable spaces $S$
isomorphic to a universally measurable subset of
a Polish space with the trace of the Borel $\sigma$-algebra, using a
version of Strassen's theorem on
common extensions of finitely additive measures.}
}

3. M. Campercholi, M. Tellechea, and P. Ventura, “Deciding Quantifier-free Definability in Finite Algebraic Structures,” Electronic Notes in Theoretical Computer Science 348: 23-41 (2020). 14th International Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2019).

This work deals with the definability problem by quantifier-free first-order formulas over a finite algebraic structure. We show the problem to be coNP-complete and present a decision algorithm based on a semantical characterization of definable relations as those preserved by isomorphisms of substructures. Our approach also includes the design of an algorithm that computes the isomorphism type of a tuple in a finite algebraic structure. Proofs of soundness and completeness of the algorithms are presented, as well as empirical tests assessing their performances.

@article{CAMPERCHOLI202023,
title = {Deciding Quantifier-free Definability in Finite Algebraic Structures},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {348},
pages = {23 - 41},
year = {2020},
note = {14th International Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2019)},
issn = {1571-0661},
doi = {https://doi.org/10.1016/j.entcs.2020.02.003},
url = {http://www.sciencedirect.com/science/article/pii/S1571066120300037},
author = {Miguel Campercholi and Mauricio Tellechea and Pablo Ventura},
keywords = {Definability, logic, decision algorithm, complexity},
abstract = {This work deals with the definability problem by quantifier-free first-order formulas over a finite algebraic structure. We show the problem to be coNP-complete and present a decision algorithm based on a semantical characterization of definable relations as those preserved by isomorphisms of substructures. Our approach also includes the design of an algorithm that computes the isomorphism type of a tuple in a finite algebraic structure. Proofs of soundness and completeness of the algorithms are presented, as well as empirical tests assessing their performances.}
}

4. M. S. Moroni and P. Sánchez Terraf, “The Zhou Ordinal of Labelled Markov Processes over Separable Spaces,” arXiv e-prints 2005.03630 (2020). Accepted for publication at the Review of Symbolic Logic.
[ Abstract | BibTeX ]

There exist two notions of equivalence of behavior between states of a Labelled Markov Process (LMP): state bisimilarity and event bisimilarity. The first one can be considered as an appropriate generalization to continuous spaces of Larsen and Skou’s probabilistic bisimilarity, while the second one is characterized by a natural logic. C. Zhou expressed state bisimilarity as the greatest fixed point of an operator $\mathcal{O}$, and thus introduced an ordinal measure of the discrepancy between it and event bisimilarity. We call this ordinal the “Zhou ordinal” of $\mathbb{S}$, $\mathfrak{Z}(\mathbb{S})$. When $\mathfrak{Z}(\mathbb{S})=0$, $\mathbb{S}$ satisfies the Hennessy-Milner property. The second author proved the existence of an LMP $\mathbb{S}$ with $\mathfrak{Z}(\mathbb{S}) \geq 1$ and Zhou showed that there are LMPs having an infinite Zhou ordinal. In this paper we show that there are LMPs $\mathbb{S}$ over separable metrizable spaces having arbitrary large countable $\mathfrak{Z}(\mathbb{S})$ and that it is consistent with the axioms of $\mathit{ZFC}$ that there is such a process with an uncountable Zhou ordinal.

@article{moroni2020zhou,
title = {The {Z}hou Ordinal of Labelled {M}arkov Processes over Separable Spaces},
author = {Moroni, Martín Santiago and S\'anchez Terraf, Pedro},
journal = {arXiv e-prints},
month = may,
year = 2020,
eprint = {2005.03630},
volume = {2005.03630},
archiveprefix = {arXiv},
primaryclass = {cs.LO},
note = {Accepted for publication at the Review of Symbolic Logic},
abstract = {There exist two notions of equivalence of behavior between states of a
Labelled Markov Process (LMP): state bisimilarity and event bisimilarity. The
first one can be considered as an appropriate generalization to continuous
spaces of Larsen and Skou's probabilistic bisimilarity, while the second one is
characterized by a natural logic. C. Zhou expressed state bisimilarity as the
greatest fixed point of an operator $\mathcal{O}$, and thus introduced an
ordinal measure of the discrepancy between it and event bisimilarity. We call
this ordinal the "Zhou ordinal" of $\mathbb{S}$, $\mathfrak{Z}(\mathbb{S})$.
When $\mathfrak{Z}(\mathbb{S})=0$, $\mathbb{S}$ satisfies the Hennessy-Milner
property. The second author proved the existence of an LMP $\mathbb{S}$ with
$\mathfrak{Z}(\mathbb{S}) \geq 1$ and Zhou showed that there are LMPs having an
infinite Zhou ordinal. In this paper we show that there are LMPs $\mathbb{S}$
over separable metrizable spaces having arbitrary large countable
$\mathfrak{Z}(\mathbb{S})$ and that it is consistent with the axioms of
$\mathit{ZFC}$ that there is such a process with an uncountable Zhou ordinal.}
}

## Recent conference papers

1. E. Gunther, M. Pagano, and P. Sánchez Terraf, “Formalization of Forcing in Isabelle/ZF,” in Automated Reasoning. 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II, 2020, p. 221–235.
[ Abstract | BibTeX ]

We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of $\mathit{ZFC}$, we construct a proper generic extension and show that the latter also satisfies $\mathit{ZFC}$. In doing so, we remodularized Paulson’s ZF-Constructibility library.

@inproceedings{2020arXiv200109715G,
author = {Gunther, Emmanuel and Pagano, Miguel and S{\'a}nchez Terraf, Pedro},
title = {{Formalization of Forcing in Isabelle/ZF}},
isbn = {978-3-662-45488-6},
booktitle = {Automated Reasoning. 10th International Joint Conference, IJCAR 2020, Paris, France, July 1--4, 2020, Proceedings, Part II},
volume = 12167,
series = {Lecture Notes in Artificial Intelligence},
editor = {Peltier, Nicolas and Sofronie-Stokkermans, Viorica},
publisher = {Springer International Publishing},
doi = {10.1007/978-3-030-51054-1},
pages = {221--235},
journal = {arXiv e-prints},
keywords = {Computer Science - Logic in Computer Science, Mathematics - Logic, 03B35 (Primary) 03E40, 03B70, 68T15 (Secondary), F.4.1},
year = 2020,
eid = {arXiv:2001.09715},
archiveprefix = {arXiv},
eprint = {2001.09715},
primaryclass = {cs.LO},
abstract = {We formalize the theory of forcing in the set theory framework of
Isabelle/ZF. Under the assumption of the existence of a countable
transitive model of $\mathit{ZFC}$, we construct a proper generic extension and show
that the latter also satisfies $\mathit{ZFC}$. In doing so, we remodularized
Paulson's ZF-Constructibility library.},
adsnote = {Provided by the SAO/NASA Astrophysics Data System}
}

2. E. Gunther, M. Pagano, and P. Sánchez Terraf, “First steps towards a formalization of Forcing,” Electronic Notes in Theoretical Computer Science 344: 119-136 (2019). The proceedings of LSFA 2018, the 13th Workshop on Logical and Semantic Frameworks with Applications (LSFA’18).

We lay the ground for an Isabelle/ZF formalization of Cohen’s technique of \emph{forcing}. We formalize the definition of forcing notions as preorders with top, dense subsets, and generic filters. We formalize a version of the principle of Dependent Choices and using it we prove the Rasiowa-Sikorski lemma on the existence of generic filters. Given a transitive set $M$, we define its generic extension $M[G]$, the canonical names for elements of $M$, and finally show that if $M$ satisfies the axiom of pairing, then $M[G]$ also does.

@article{2018arXiv180705174G,
author = {Gunther, Emmanuel and Pagano, Miguel and S{\'a}nchez Terraf, Pedro},
title = {{First steps towards a formalization of Forcing}},
journal = {Electronic Notes in Theoretical Computer Science},
archiveprefix = {arXiv},
eprint = {1807.05174},
primaryclass = {cs.LO},
keywords = {Computer Science - Logic in Computer Science, 03B35 (Primary) 03E40, 03B70, 68T15 (Secondary), F.4.1},
month = jul,
adsnote = {Provided by the SAO/NASA Astrophysics Data System},
abstract = {We lay the ground for an Isabelle/ZF formalization of Cohen's
technique of \emph{forcing}. We formalize the definition of forcing notions as
preorders with top, dense subsets, and generic filters. We formalize
a version of the principle of Dependent Choices and using it
we prove the Rasiowa-Sikorski lemma on the existence of generic filters.
Given a transitive set $M$, we define its generic extension $M[G]$,
the canonical names for elements of $M$, and finally show that if $M$
satisfies the axiom of pairing, then $M[G]$ also does.},
volume = {344},
pages = {119 - 136},
year = {2019},
issn = {1571-0661},
doi = {10.1016/j.entcs.2019.07.008},
url = {http://www.sciencedirect.com/science/article/pii/S157106611930026X},
note = {The proceedings of LSFA 2018, the 13th Workshop on Logical and Semantic Frameworks with Applications (LSFA’18)}
}