Center of Mathematics of the University of Minho

Funder

Organizational Unit

Publications

The Russell-Prawitz embedding and the atomization of universal instantiation

Publication . Espírito Santo, José; Ferreira, Gilda

Given the recent interest in the fragment of system F where universal instantiation is restricted to atomic formulas, a fragment nowadays named system Fat, we study directly in system F new conversions whose purpose is to enforce that restriction. We show some benefits of these new atomization conversions: (1) They help achieving strict simulation of proof reduction by means of the Russell-Prawitz embedding of IPC into system F; (2) They are not stronger than a certain “dinaturality” conversion known to generate a consistent equality of proofs; (3) They provide the bridge between the Russell-Prawitz embedding and another translation, due to the authors, of IPC directly into system Fat; (4) They give means for explaining why the Russell-Prawitz translation achieves strict simulation whereas the translation into Fat does not.

2020Journal article

Open access

Topological aspects of incompressible flows

Publication . Bessa, Mário; Torres, Maria Joana; Varandas, Paulo

In this article we approach some of the basic questions in topological dynamics, concerning periodic points, transitivity, the shadowing and the gluing orbit properties, in the context of C0 incompressible flows generated by Lipschitz vector fields. We prove that a C0-generic incompressible and fixed-point free flow satisfies the periodic shadowing property, it is transitive and has a dense set of periodic points in the non- wandering set. In particular, a C0-generic fixed-point free incompressible flow satisfies the reparametrized gluing orbit property. We also prove that C0-generic incompressible flows satisfy the general density theorem and the weak shadowing property, moreover these are transitive.

2021Journal article

Restricted access

Expansiveness and hyperbolicity in convex billiards

Publication . Bessa, Mário; Dias, João Lopes; Torres, Maria Joana

We say that a convex planar billiard table B is C2-stably expansive on a fixed open subset U of the phase space if its billiard map f_B is expansive on the maximal invariant set Λ_{B,U}, and this property holds under C2-perturbations of the billiard table. In this note we prove for such billiards that the closure of the set of periodic points of f_B in Λ_{B,U} is uniformly hyperbolic. In addition, we show that this property also holds for a generic choice among billiards which are expansive.

2021Journal article

Open access

How to avoid the commuting conversions of IPC

Publication . Espírito Santo, José; Ferreira, Gilda

Since the observation in 2006 that it is possible to embed IPC into the atomic polymorphic λ-calculus (a predicative fragment of system F with universal instantiations restricted to atomic formulas) different such embeddings appeared in the literature. All of them comprise the Russell-Prawitz translation of formulas, but have different strategies for the translation of proofs. Although these embeddings preserve proof identity, all fail in delivering preservation of reduction steps. In fact, they translate the commuting conversions of IPC to β-equality, or to other kinds of reduction or equality generated by new principles added to system F. The cause for this is the generation of redexes by the translation itself. In this paper, we present an embedding of IPC into atomic system F, still based on the same translation of formulas, but which maps commuting conversions to syntactic identity, while simulating the other kinds of reduction steps present in IPC by βη-reduction. In this sense the translation achieves a truly commuting-conversion-free image of IPC in atomic system F.

2025-04-07Journal article

Open access