Showing 1–5 of 5 results for author: Warren, L

First-order natural deduction in Agda

Authors: Louis Warren

Abstract: Agda is a dependently-typed functional programming language, based on an extension of intuitionistic Martin-Löf type theory. We implement first order natural deduction in Agda. We use Agda's type checker to verify the correctness of natural deduction proofs, and also prove properties of natural deduction, using Agda's proof assistant functionality. This implementation corresponds to a formalisatio… ▽ More Agda is a dependently-typed functional programming language, based on an extension of intuitionistic Martin-Löf type theory. We implement first order natural deduction in Agda. We use Agda's type checker to verify the correctness of natural deduction proofs, and also prove properties of natural deduction, using Agda's proof assistant functionality. This implementation corresponds to a formalisation of natural deduction in constructive type theory, and the proofs are verified by Agda to be correct (under the assumption that Agda itself is correct). △ Less

Submitted 8 April, 2021; originally announced April 2021.

Constructing a quasiregular analogue of $z \exp(z)$ in dimension 3

Authors: Luke Warren

Abstract: We construct a quasiregular analogue of the function $z\exp(z)$ in dimension 3, which gives the first explicit example of a quasiregular mapping of transcendental type that has exactly one zero. We then modify the construction to create a family of such quasiregular mappings and study their dynamics. From this, we also construct the first quasimeromorphic mappings with an essential singularity at… ▽ More We construct a quasiregular analogue of the function $z\exp(z)$ in dimension 3, which gives the first explicit example of a quasiregular mapping of transcendental type that has exactly one zero. We then modify the construction to create a family of such quasiregular mappings and study their dynamics. From this, we also construct the first quasimeromorphic mappings with an essential singularity at infinity where the backward orbit of infinity is non-empty and finite. △ Less

Submitted 10 July, 2019; originally announced July 2019.

Comments: 13 pages

MSC Class: 30C65 (Primary); 37F10;

On slow escaping and non-escaping points of quasimeromorphic mappings

Authors: Luke Warren

Abstract: We show that for any quasimeromorphic mapping with an essential singularity at infinity, there exist points whose iterates tend to infinity arbitrarily slowly. This extends a result by Nicks for quasiregular mappings, and Rippon and Stallard for transcendental meromorphic functions on the complex plane. We further establish a new result for the growth rate of quasiregular mappings near an essentia… ▽ More We show that for any quasimeromorphic mapping with an essential singularity at infinity, there exist points whose iterates tend to infinity arbitrarily slowly. This extends a result by Nicks for quasiregular mappings, and Rippon and Stallard for transcendental meromorphic functions on the complex plane. We further establish a new result for the growth rate of quasiregular mappings near an essential singularity, and briefly extend some results regarding the bounded orbit set and the bungee set to the quasimeromorphic setting. △ Less

Submitted 21 March, 2019; originally announced March 2019.

Comments: 35 pages

MSC Class: 37F10 (Primary); 30C65; 30D05

Journal ref: Ergod. Th. Dynam. Sys. 41 (2021) 1190-1216

The Drinker Paradox and its Dual

Authors: Louis Warren, Hannes Diener, Maarten McKubre-Jordens

Abstract: The Drinker Paradox is as follows. In every nonempty tavern, there is a person such that if that person is drinking, then everyone in the tavern is drinking. Formally, \[ \exists x \big(\varphi \rightarrow \forall y \varphi[x/y]\big) \ . \] Due to its counterintuitive nature it is called a paradox, even though it actually is a classical tautology. However, it is not minimally (or even intuit… ▽ More The Drinker Paradox is as follows. In every nonempty tavern, there is a person such that if that person is drinking, then everyone in the tavern is drinking. Formally, \[ \exists x \big(\varphi \rightarrow \forall y \varphi[x/y]\big) \ . \] Due to its counterintuitive nature it is called a paradox, even though it actually is a classical tautology. However, it is not minimally (or even intuitionistically) provable. The same can be said of its dual, which is (equivalent to) the well-known principle of \emph{independence of premise}, \[ \varphi \rightarrow \exists x ψ \ \vdash \ \exists x (\varphi \rightarrow ψ) \] where $x$ is not free in $\varphi$. In this paper we study the implications of adding these and other formula schemata to minimal logic. We show first that these principles are independent of the law of excluded middle and of each other, and second how these schemata relate to other well-known principles, such as Markov's Principle of unbounded search, providing proofs and semantic models where appropriate. △ Less

Submitted 29 November, 2018; v1 submitted 16 May, 2018; originally announced May 2018.

On the iteration of quasimeromorphic mappings

Authors: Luke Warren

Abstract: The Fatou-Julia theory for rational functions has been extended both to transcendental meromorphic functions and more recently to several different types of quasiregular mappings in higher dimensions. We extend the iterative theory to quasimeromorphic mappings with an essential singularity at infinity and at least one pole, constructing the Julia set for these maps. We show that this Julia set sha… ▽ More The Fatou-Julia theory for rational functions has been extended both to transcendental meromorphic functions and more recently to several different types of quasiregular mappings in higher dimensions. We extend the iterative theory to quasimeromorphic mappings with an essential singularity at infinity and at least one pole, constructing the Julia set for these maps. We show that this Julia set shares many properties with those for transcendental meromorphic functions and for quasiregular mappings of punctured space. △ Less

Submitted 3 May, 2018; v1 submitted 1 May, 2018; originally announced May 2018.

Comments: 14 pages

MSC Class: 37F10 (Primary); 30C65; 30D05