-
Le Nozze di Giustizia. Interactions between Artificial Intelligence, Law, Logic, Language and Computation with some case studies in Traffic Regulations and Health Care
Authors:
Joost J. Joosten,
Manuela Montoya García
Abstract:
An important aim of this paper is to convey some basics of mathematical logic to the legal community working with Artificial Intelligence. After analysing what AI is, we decide to delimit ourselves to rule-based AI leaving Neural Networks and Machine Learning aside. Rule based AI allows for Formal methods which are described in a rudimentary form. We will then see how mathematical logic interacts…
▽ More
An important aim of this paper is to convey some basics of mathematical logic to the legal community working with Artificial Intelligence. After analysing what AI is, we decide to delimit ourselves to rule-based AI leaving Neural Networks and Machine Learning aside. Rule based AI allows for Formal methods which are described in a rudimentary form. We will then see how mathematical logic interacts with legal rule-based AI practice. We shall see how mathematical logic imposes limitations and complications to AI applications. We classify the limitations and interactions between mathematical logic and legal AI in three categories: logical, computational and mathematical. The examples to showcase the interactions will largely come from European traffic regulations. The paper closes off with some reflections on how and where AI could be used and on basic mechanisms that shape society.
△ Less
Submitted 9 February, 2024;
originally announced February 2024.
-
Dialogues with algorithms
Authors:
Joost J. Joosten
Abstract:
In this short paper we focus on human in the loop for rule-based software used for law enforcement. For example, one can think of software that computes fines like tachograph software, software that prepares evidence like DNA sequencing software or social profiling software to patrol in high-risk zones, among others. An important difference between a legal human agent and a software application li…
▽ More
In this short paper we focus on human in the loop for rule-based software used for law enforcement. For example, one can think of software that computes fines like tachograph software, software that prepares evidence like DNA sequencing software or social profiling software to patrol in high-risk zones, among others. An important difference between a legal human agent and a software application lies in possible dialogues. A human agent can be interrogated to motivate her decisions. Often such dialogues with software are at the best extremely hard but mostly impossible. We observe that the absence of a dialogue can sincerely violate civil rights and legal principles like, for example, Transparency or Contestability. Thus, possible dialogues with legal algorithms are at the least highly desirable. Futuristic as this may sound, we observe that in various realms of formal methods, such dialogues are easily obtainable. However, this triggers the usual tension between the expressibility of the dialogue language and the feasibility of the corresponding computations.
△ Less
Submitted 19 September, 2023;
originally announced September 2023.
-
Model-checking in the Foundations of Algorithmic Law and the Case of Regulation 561
Authors:
Moritz Müller,
Joost J. Joosten
Abstract:
We discuss model-checking problems as formal models of algorithmic law. Specifically, we ask for an algorithmically tractable general purpose model-checking problem that naturally models the European transport Regulation 561, and discuss the reaches and limits of a version of discrete time stopwatch automata.
We discuss model-checking problems as formal models of algorithmic law. Specifically, we ask for an algorithmically tractable general purpose model-checking problem that naturally models the European transport Regulation 561, and discuss the reaches and limits of a version of discrete time stopwatch automata.
△ Less
Submitted 11 July, 2023;
originally announced July 2023.
-
UTC Time, Formally Verified
Authors:
Ana de Almeida Borges,
Mireia González Bedmar,
Juan Conejero Rodríguez,
Eduardo Hermo Reyes,
Joaquim Casals Buñuel,
Joost J. Joosten
Abstract:
FV Time is a small-scale verification project developed in the Coq proof assistant using the Mathematical Components libraries. It is a library for managing conversions between time formats (UTC and timestamps), as well as commonly used functions for time arithmetic. As a library for time conversions, its novelty is the implementation of leap seconds, which are part of the UTC standard but usually…
▽ More
FV Time is a small-scale verification project developed in the Coq proof assistant using the Mathematical Components libraries. It is a library for managing conversions between time formats (UTC and timestamps), as well as commonly used functions for time arithmetic. As a library for time conversions, its novelty is the implementation of leap seconds, which are part of the UTC standard but usually not implemented in existing libraries. Since the verified functions of FV Time are reasonably simple yet non-trivial, it nicely illustrates our methodology for verifying software with Coq.
In this paper we present a description of the project, emphasizing the main problems faced while develo** the library, as well as some general-purpose solutions that were produced as by-products and may be used in other verification projects. These include a refinement package between proof-oriented MathComp numbers and computation-oriented primitive numbers from the Coq standard library, as well as a set of tactics to automatically prove certain decidable statements over finite ranges through brute-force computation.
△ Less
Submitted 13 December, 2023; v1 submitted 28 September, 2022;
originally announced September 2022.
-
Hidden variables simulating quantum contextuality increasingly violate the Holevo bound
Authors:
Adán Cabello,
Joost J. Joosten
Abstract:
In this paper from 2011 we approach some questions about quantum contextuality with tools from formal logic. In particular, we consider an experiment associated with the Peres-Mermin square. The language of all possible sequences of outcomes of the experiment is classified in the Chomsky hierarchy and seen to be a regular language. Next, we make the rather evident observation that a finite set of…
▽ More
In this paper from 2011 we approach some questions about quantum contextuality with tools from formal logic. In particular, we consider an experiment associated with the Peres-Mermin square. The language of all possible sequences of outcomes of the experiment is classified in the Chomsky hierarchy and seen to be a regular language. Next, we make the rather evident observation that a finite set of hidden finite valued variables can never account for indeterminism in an ideally isolated repeatable experiment. We see that, when the language of possible outcomes of the experiment is regular, as is the case with the Peres-Mermin square, the amount of binary-valued hidden variables needed to de-randomize the model for all sequences of experiments up to length n grows as bad as it could be: linearly in n. We introduce a very abstract model of machine that simulates nature in a particular sense. A lower-bound on the number of memory states of such machines is proved if they were to simulate the experiment that corresponds to the Peres-Mermin square. Moreover, the proof of this lower bound is seen to scale to a certain generalization of the Peres- Mermin square. For this scaled experiment it is seen that the Holevo bound is violated and that the degree of violation increases uniformly.
△ Less
Submitted 10 April, 2020;
originally announced April 2020.
-
When logic lays down the law
Authors:
Bjørn Jespersen,
Ana de Almeida Borges,
Jorge del Castillo Tierz,
Juan José Conejero Rodríguez,
Eric Sancho Adamson,
Aleix Solé Sánchez,
Nika Pona,
Joost J. Joosten
Abstract:
We analyse so-called computable laws, i.e., laws that can be enforced by automatic procedures. These laws should be logically perfect and unambiguous, but sometimes they are not. We use a regulation on road transport to illustrate this issue, and show what some fragments of this regulation would look like if rewritten in the image of logic. We further propose desiderata to be fulfilled by computab…
▽ More
We analyse so-called computable laws, i.e., laws that can be enforced by automatic procedures. These laws should be logically perfect and unambiguous, but sometimes they are not. We use a regulation on road transport to illustrate this issue, and show what some fragments of this regulation would look like if rewritten in the image of logic. We further propose desiderata to be fulfilled by computable laws, and provide a critical platform from which to assess existing laws and a guideline for composing future ones.
△ Less
Submitted 6 October, 2018;
originally announced October 2018.
-
The Selfish Algorithm
Authors:
Eduardo Hermo Reyes,
Joost J. Joosten
Abstract:
The principle of Generalized Natural Selection (GNS) states that in nature, computational processes of high computational sophistication are more likely to maintain/abide than processes of lower computational sophistication provided that sufficiently many resources are around to sustain the processes. In this paper we give a concrete set-up how to test GNS in a weak sense. In particular, we work i…
▽ More
The principle of Generalized Natural Selection (GNS) states that in nature, computational processes of high computational sophistication are more likely to maintain/abide than processes of lower computational sophistication provided that sufficiently many resources are around to sustain the processes. In this paper we give a concrete set-up how to test GNS in a weak sense. In particular, we work in the setting of Cellular Automata and see how GNS can manifest itself in this setting.
△ Less
Submitted 10 November, 2014;
originally announced November 2014.
-
Fractal dimension versus process complexity
Authors:
Joost J. Joosten,
Fernando Soler-Toscano,
Hector Zenil
Abstract:
Complexity measures are designed to capture complex behavior and quantify *how* complex, according to that measure, that particular behavior is. It can be expected that different complexity measures from possibly entirely different fields are related to each other in a non-trivial fashion. Here we study small Turing machines (TMs) with two symbols, and two and three states. For any particular such…
▽ More
Complexity measures are designed to capture complex behavior and quantify *how* complex, according to that measure, that particular behavior is. It can be expected that different complexity measures from possibly entirely different fields are related to each other in a non-trivial fashion. Here we study small Turing machines (TMs) with two symbols, and two and three states. For any particular such machine $τ$ and any particular input $x$ we consider what we call the 'space-time' diagram which is the collection of consecutive tape configurations of the computation $τ(x)$. In our setting, we define fractal dimension of a Turing machine as the limiting fractal dimension of the corresponding space-time diagram. It turns out that there is a very strong relation between the fractal dimension of a Turing machine of the above-specified type and its runtime complexity. In particular, a TM with three states and two colors runs in at most linear time iff its dimension is 2, and its dimension is 1 iff it runs in super-polynomial time and it uses polynomial space. If a TM runs in time $O(x^n)$ we have empirically verified that the corresponding dimension is $(n+1)/n$, a result that we can only partially prove. We find the results presented here remarkable because they relate two completely different complexity measures: the geometrical fractal dimension on the one side versus the time complexity of a computation on the other side.
△ Less
Submitted 22 August, 2016; v1 submitted 6 September, 2013;
originally announced September 2013.
-
Complexity fits the fittest
Authors:
J. J. Joosten
Abstract:
In this paper we shall relate computational complexity to the principle of natural selection. We shall do this by giving a philosophical account of complexity versus universality. It seems sustainable to equate universal systems to complex systems or at least to potentially complex systems. Post's problem on the existence of (natural) intermediate degrees (between decidable and universal RE) then…
▽ More
In this paper we shall relate computational complexity to the principle of natural selection. We shall do this by giving a philosophical account of complexity versus universality. It seems sustainable to equate universal systems to complex systems or at least to potentially complex systems. Post's problem on the existence of (natural) intermediate degrees (between decidable and universal RE) then finds its analog in the Principle of Computional Equivalence (PCE). In this paper we address possible driving forces --if any-- behind PCE. Both the natural aspects as well as the cognitive ones are investigated. We postulate a principle GNS that we call the Generalized Natural Selection principle that together with the Church-Turing thesis is seen to be in close correspondence to a weak version of PCE. Next, we view our cognitive toolkit in an evolutionary light and postulate a principle in analogy with Fodor's language principle. In the final part of the paper we reflect on ways to provide circumstantial evidence for GNS by means of theorems, experiments or, simulations.
△ Less
Submitted 11 December, 2012;
originally announced December 2012.
-
On the necessity of complexity
Authors:
Joost J. Joosten
Abstract:
Wolfram's Principle of Computational Equivalence (PCE) implies that universal complexity abounds in nature. This paper comprises three sections. In the first section we consider the question why there are so many universal phenomena around. So, in a sense, we week a driving force behind the PCE if any. We postulate a principle GNS that we call the Generalized Natural Selection Principle that toget…
▽ More
Wolfram's Principle of Computational Equivalence (PCE) implies that universal complexity abounds in nature. This paper comprises three sections. In the first section we consider the question why there are so many universal phenomena around. So, in a sense, we week a driving force behind the PCE if any. We postulate a principle GNS that we call the Generalized Natural Selection Principle that together with the Church-Turing Thesis is seen to be equivalent to a weak version of PCE. In the second section we ask the question why we do not observe any phenomena that are complex but not-universal. We choose a cognitive setting to embark on this question and make some analogies with formal logic. In the third and final section we report on a case study where we see rich structures arise everywhere.
△ Less
Submitted 6 November, 2012;
originally announced November 2012.
-
A secure additive protocol for card players
Authors:
Andres Cordon-Franco,
Hans van Ditmarsch,
David Fernandez-Duque,
Joost J. Joosten,
Fernando Soler-Toscano
Abstract:
Consider three players Alice, Bob and Cath who hold a, b and c cards, respectively, from a deck of d=a+b+c cards. The cards are all different and players only know their own cards. Suppose Alice and Bob wish to communicate their cards to each other without Cath learning whether Alice or Bob holds a specific card.
Considering the cards as consecutive natural numbers 0,1,..., we investigate genera…
▽ More
Consider three players Alice, Bob and Cath who hold a, b and c cards, respectively, from a deck of d=a+b+c cards. The cards are all different and players only know their own cards. Suppose Alice and Bob wish to communicate their cards to each other without Cath learning whether Alice or Bob holds a specific card.
Considering the cards as consecutive natural numbers 0,1,..., we investigate general conditions for when Alice or Bob can safely announce the sum of the cards they hold modulo an appropriately chosen integer. We demonstrate that this holds whenever a,b>2 and c=1. Because Cath holds a single card, this also implies that Alice and Bob will learn the card deal from the other player's announcement.
△ Less
Submitted 1 November, 2011;
originally announced November 2011.
-
Empirical Encounters with Computational Irreducibility and Unpredictability
Authors:
Hector Zenil,
Fernando Soler-Toscano,
Joost J. Joosten
Abstract:
There are several forms of irreducibility in computing systems, ranging from undecidability to intractability to nonlinearity. This paper is an exploration of the conceptual issues that have arisen in the course of investigating speed-up and slowdown phenomena in small Turing machines. We present the results of a test that may spur experimental approaches to the notion of computational irreducibil…
▽ More
There are several forms of irreducibility in computing systems, ranging from undecidability to intractability to nonlinearity. This paper is an exploration of the conceptual issues that have arisen in the course of investigating speed-up and slowdown phenomena in small Turing machines. We present the results of a test that may spur experimental approaches to the notion of computational irreducibility. The test involves a systematic attempt to outrun the computation of a large number of small Turing machines (all 3 and 4 state, 2 symbol) by means of integer sequence prediction using a specialized function finder program. This massive experiment prompts an investigation into rates of convergence of decision procedures and the decidability of sets in addition to a discussion of the (un)predictability of deterministic computing systems in practice. We think this investigation constitutes a novel approach to the discussion of an epistemological question in the context of a computer simulation, and thus represents an interesting exploration at the boundary between philosophical concerns and computational experiments.
△ Less
Submitted 23 June, 2011; v1 submitted 18 April, 2011;
originally announced April 2011.
-
Program-Size Versus Time Complexity, Speed-Up and Slowdown Phenomena in Small Turing Machines
Authors:
Joost J. Joosten,
Fernando Soler-Toscano,
Hector Zenil
Abstract:
The aim of this paper is to undertake an experimental investigation of the trade-offs between program-size and time computational complexity. The investigation includes an exhaustive exploration and systematic study of the functions computed by the set of all 2-color Turing machines with 2, 3 and 4 states--denoted by (n,2) with n the number of states--with particular attention to the runtimes and…
▽ More
The aim of this paper is to undertake an experimental investigation of the trade-offs between program-size and time computational complexity. The investigation includes an exhaustive exploration and systematic study of the functions computed by the set of all 2-color Turing machines with 2, 3 and 4 states--denoted by (n,2) with n the number of states--with particular attention to the runtimes and space usages when the machines have access to larger resources (more states). We report that the average runtime of Turing machines computing a function almost surely increases as a function of the number of states, indicating that machines not terminating (almost) immediately tend to occupy all the resources at hand. We calculated all time complexity classes to which the algorithms computing the functions found in both (2,2) and (3,2) belong to, and made a comparison among these classes. For a selection of functions the comparison was extended to (4,2). Our study revealed various structures in the micro-cosmos of small Turing machines. Most notably we observed "phase-transitions" in the halting-probability distribution that we explain. Moreover, it is observed that short initial segments fully define a function computed by a Turing machine.
△ Less
Submitted 16 April, 2011; v1 submitted 26 February, 2011;
originally announced February 2011.
-
Complejidad descriptiva y computacional en maquinas de Turing pequenas
Authors:
Joost J. Joosten,
Fernando Soler-Toscano,
Hector Zenil
Abstract:
We start by an introduction to the basic concepts of computability theory and the introduction of the concept of Turing machine and computation universality. Then se turn to the exploration of trade-offs between different measures of complexity, particularly algorithmic (program-size) and computational (time) complexity as a mean to explain these measure in a novel manner. The investigation procee…
▽ More
We start by an introduction to the basic concepts of computability theory and the introduction of the concept of Turing machine and computation universality. Then se turn to the exploration of trade-offs between different measures of complexity, particularly algorithmic (program-size) and computational (time) complexity as a mean to explain these measure in a novel manner. The investigation proceeds by an exhaustive exploration and systematic study of the functions computed by a large set of small Turing machines with 2 and 3 states with particular attention to runtimes, space-usages and patterns corresponding to the computed functions when the machines have access to larger resources (more states).
We report that the average runtime of Turing machines computing a function increases as a function of the number of states, indicating that non-trivial machines tend to occupy all the resources at hand. General slow-down was witnessed and some incidental cases of (linear) speed-up were found. Throughout our study various interesting structures were encountered. We unveil a study of structures in the micro-cosmos of small Turing machines.
△ Less
Submitted 15 April, 2011; v1 submitted 7 October, 2010;
originally announced October 2010.
