Search

We present a constructive analysis and machine-checked theory of one-one, many-one, and truth-table reductions based on synthetic computability theory in the Calculus of Inductive Constructions, the type theory underlying the proof assistant Coq. We give elegant, synthetic, and machine-checked proofs of Post’s landmark results that a simple predicate exists, is enumerable, undecidable, but many-one incomplete (Post’s problem for many-one reducibility), and a hypersimple predicate exists, is enumerable, undecidable, but truth-table incomplete (Post’s problem for truth-table reducibility). In synthetic computability, one assumes axioms allowing to carry out computability theory with all definitions and proofs purely in terms of functions of the type theory with no mention of a model of computation. Proofs can focus on the essence of the argument, without having to sacrifice formality. Synthetic computability also clears the lense for constructivisation. Our constructively careful definition of simple and hypersimple predicates allows us to not assume classical axioms, not even Markov’s principle, still yielding the expected strong results., LIPIcs, Vol. 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), pages 21:1-21:21

We present a constructive analysis and machine-checked synthetic approach to the theory of one-one, many-one, and truth-table reductions carried out in the Calculus of Inductive Constructions, the type theory underlying the proof assistant Coq. In synthetic computability, one assumes axioms allowing to carry out computability theory with all definitions and proofs purely in terms of functions of the type theory with no mention of a model of computation. Our synthetic proof of Myhill's isomorphism theorem that one-one equivalence yields a computational isomorphism makes a compelling case for synthetic computability due to its simplicity without sacrificing formality. Synthetic computability also clears the lense for constructivisation. We do not assume classical axioms, not even Markov's principle, possible by a careful constructivised definition of simple and hypersimple predicates, still yielding the expected strong results: a simple predicate exists, is enumerable, undecidable, but many-one incomplete (Post's problem for many-one reducibility), and a hypersimple predicate exists, is enumerable, undecidable, but truth-table incomplete (Post's problem for truth-table reducibility).

International audience; We report about an ongoing collaborative effort to consolidate several Coq developments concerning metamathematical results in first-order logic [1, 2, 11, 10, 8, 7, 6, 15, 12] into a single library. We first describe the framework regarding the representation of syntax, deduction systems, and semantics as well as its instantiation to axiom systems and tools for user-friendly interaction. Next, we summarise the included results mostly connected to completeness, undecidability, and incompleteness. Finally, we conclude by reporting on challenges experienced and anticipated during the integration. The current status of the project can be tracked in a public fork of the Coq Library of Undecidability Proofs [3]. Framework In principle, we follow ideas and suggestions present in various approaches [14, 9, 5, 4, 13] to the representation of first-order logic in CIC. Over the span of our initial projects we tried out several variants and found the final framework to be most suitable. Notably, a previous version used the Autosubst 2 tool [16] to generate the syntax, which we decided to avoid in later versions due to its use of function extensionality. The final framework, however, still follows the same design principles for binding and substitution. The syntax is represented by inductive types for terms t : T and formulas ϕ : F depending on signatures of function symbols f and relation symbols P as well as a collection of binary connectives 2 and quantifiers ∇

We present a generalised, constructive, and machine-checked approach to Kolmogorov complexity in the constructive type theory underlying the Coq proof assistant. By proving that nonrandom numbers form a simple predicate, we obtain elegant proofs of undecidability for random and nonrandom numbers and a proof of uncomputability of Kolmogorov complexity. We use a general and abstract definition of Kolmogorov complexity and subsequently instantiate it to several definitions frequently found in the literature. Whereas textbook treatments of Kolmogorov complexity usually rely heavily on classical logic and the axiom of choice, we put emphasis on the constructiveness of all our arguments, however without blurring their essence. We first give a high-level proof idea using classical logic, which can be formalised with Markov’s principle via folklore techniques we subsequently explain. Lastly, we show a strategy how to eliminate Markov’s principle from a certain class of computability proofs, rendering all our results fully constructive. All our results are machine-checked by the Coq proof assistant, which is enabled by using a synthetic approach to computability: rather than formalising a model of computation, which is well known to introduce a considerable overhead, we abstractly assume a universal function, allowing the proofs to focus on the mathematical essence., LIPIcs, Vol. 237, 13th International Conference on Interactive Theorem Proving (ITP 2022), pages 12:1-12:19

International audience; We formalise the undecidability of solvability of Diophantine equations, i.e. polynomial equations over natural numbers, in Coq's constructive type theory. To do so, we give the first full mechanisation of the Davis-Putnam-Robinson-Matiyasevich theorem, stating that every recursively enumerable problem -- in our case by a Minsky machine -- is Diophantine. We obtain an elegant and comprehensible proof by using a synthetic approach to computability and by introducing Conway's FRACTRAN language as intermediate layer. Additionally, we prove the reverse direction and show that every Diophantine relation is recognisable by µ-recursive functions and give a certified compiler from µ-recursive functions to Minsky machines.

The weak call-by-value λ-calculus Łand Turing machines can simulate each other with a polynomial overhead in time. This time invariance thesis for L, where the number of β-reductions of a computation is taken as its time complexity, is the culmination of a 25-years line of research, combining work by Blelloch, Greiner, Dal Lago, Martini, Accattoli, Forster, Kunze, Roth, and Smolka. The present paper presents a mechanised proof of the time invariance thesis for L, constituting the first mechanised equivalence proof between two standard models of computation covering time complexity. The mechanisation builds on an existing framework for the extraction of Coq functions to L and contributes a novel Hoare logic framework for the verification of Turing machines. The mechanised proof of the time invariance thesis establishes Łas model for future developments of mechanised computational complexity theory regarding time. It can also be seen as a non-trivial but elementary case study of time-complexity-preserving translations between a functional language and a sequential machine model. As a by-product, we obtain a mechanised many-one equivalence proof of the halting problems for Łand Turing machines, which we contribute to the Coq Library of Undecidability Proofs., LIPIcs, Vol. 193, 12th International Conference on Interactive Theorem Proving (ITP 2021), pages 19:1-19:20

International audience; We propose a talk on our library of mechanised reductions to establish undecidability results in Coq. The library is a collaborative effort, growing constantly and we are seeking more outside contributors willing to work on undecidability results in Coq.

Das automatisierte Fahren hat bereits den Weg auf den kommerziellen Markt geschafft und weiterer Fortschritt kann in naher Zukunft erwartet werden. Das Level 3 des automatisierten Fahrens verspricht steigende Sicherheit, Komfort und Verkehrseffizienz. Für den menschlichen Fahrer sind diese Funktionen und damit einhergehende Nutzerschnittstellen eine neuartige Technologie. Im Bereich Human Factors stehen Forschung und Entwicklung vor zwei Herausforderungen, welche (1) der Entwurf von intuitiven und einfach bedienbaren Nutzerschnittstellen und (2) die Entwicklung von Methoden zur Bewertung ebendieser sind. Bei der Bewertung von Technologie wurde bereits häufig auf die sogenannte Preference-Performance Dissoziation aufmerksam gemacht. Diese beschreibt das Ergebnis von Nutzerstudien, in denen die Präferenz (Selbstbericht) der Nutzer nicht mit deren Leistung (beobachtbares Verhalten) übereinstimmt. Dieses Phänomen stellt eine Gefährdung für die Bewertung von Nutzerschnittstellen beim automatisierten Fahren dar. Aufgrund dessen berichtet die vorliegende Dissertation zunächst Untersuchungen zur Messbarmachung von Präferenz und Leistung. Zudem wurde das Verständnis von automatisierten Systemen (mentales Modell) als ein wichtiger Einflussfaktor zur Entstehung des beobachtbaren Verhaltens angenommen und mit in die Arbeiten eingeschlossen. Mithilfe der gewonnenen Erkenntnisse der Messbarmachung widmete sich der zweite Teil der Dissertation den Faktoren, die einen Einfluss auf das Entstehen von Präferenz und/oder Leistung ausüben. Untersuchte Faktoren waren die Anzahl an Wiederholungen von Anwendungsfällen, Rückmeldung zur Bedienleistung, Nutzerschulung und eine statistische post-hoc Analyse. Um die Ziele der Messbarmachung und Einflussnahme zu erreichen wurden drei Fahrsimulatorstudien mit insgesamt N=225 Probanden durchgeführt. Die Haupterkenntnisse waren (1) die Entwicklung einer differenzierten Empfehlung von Fragebögen zur Erfassung der Nutzerpräferenz. Außerdem (2) wurden Erkenntnisse der Entwicklung von Verhaltensmaßen über die Zeit sowie deren Zusammenhang zu Präferenzmaßen gewonnen. Betreffend der mentalen Modelle (3) zeigte die vorliegende Arbeit, dass es wiederholter Interaktion bedarf, damit diese sich korrekt entwickeln. Außerdem kann das Verständnis durch Blickverhaltensmaße erfasst werden. Zusätzlich (4) zeigte sich, dass Leistungsrückmeldung Präferenz, nicht aber Leistung selbst beeinflussen kann. Im Gegensatz dazu (5) wirkt sich Nutzerschulung positiv auf die Korrektheit mentaler Modelle und nachfolgend der Nutzerleistung selbst aus, lässt aber Präferenzmaße unbeeinflusst. Abschließend zeigte sich, dass (6) Nutzer verschiedener Leistungsstufen ähnliche Präferenzurteile fällen. Der theoretische Beitrag der vorliegenden Arbeit liegt in den Einblicken in die Entstehung der beiden Datenquellen der Preference-Performance Dissoziation wodurch diese erklärt und vorhergesagt werden kann. Der praktische Beitrag liegt in der Anwendung der Arbeit zur Messbarmachung von Variablen und Empfehlung zum Studiendesign hinsichtlich Anzahl an Messwiederholungen und Nutzerschulung. Abschließend betreffen die hier gewonnenen Erkenntnisse nicht nur die Bewertung von Nutzerschnittstellen beim automatisierten Fahren, sondern können auch auf andere Automationsbereiche der Mensch-Maschine Interaktion wie beispielsweise Luftfahrt, Robotik oder Medizintechnik übertragen werden. Driving automation systems have already entered the commercial market and further advancements will be introduced in the near future. Level 3 automated driving systems are expected to increase safety, comfort and traffic efficiency. For the human driver, these functions and according human-machine interfaces are a novel technology. In the human factors domain, research and development faces two challenges which are (1) the conceptualization of intuitive and easy to use interfaces and (2) the development of a methodological framework to evaluate these interfaces. In technology evaluation, a methodological phenomenon has frequently been reported which is called the preference-performance dissociation. It describes the outcome of studies where users' preference (i.e., self-report) does not match their performance (i.e., interaction behavior). This phenomenon poses a threat to the evaluation of automated vehicle HMIs. Therefore, the present thesis first reports investigations on how to operationalize both performance and preference. Moreover, the understanding (i.e., mental model) of automated vehicle HMIs was hypothesized as an influential precursor of performance and included in the present work. Using the insights of the operationalization part, the second part of the thesis aimed at finding out about factors that exert influence on preference and/or performance. Investigated factors were the number of use case repetitions, feedback on operator performance, user education and a post-hoc statistical analysis. To reach the operationalization and variation aims, three driving simulator studies with a total of N=225 participants were conducted. The main outcomes were that (1) a sophisticated recommendation regarding preference questionnaire application could be given. Furthermore, (2) insights into the development of behavioral measures over time and their relation to a satisfaction measure could be given. Concerning mental models, (3) the present work showed that it takes repeated interaction to evolve accurately and gaze measures could also be used for capturing these processes. In addition, (4) feedback on operator performance was found to influence preference but not performance while (5) user education increased understanding and subsequent performance but did not affect preference. Eventually it showed that (6) users of different performance levels report similar preference. The theoretical contribution of this work lies in insights into the formation of the two sources of data and its potential to both explain and predict the preference-performance dissociation. The practical contribution lies in the recommendation for research methodology regarding how to operationalize measures and how to design user studies concerning the number of use cases and user education approaches. Finally, the results gained herein do not only apply to automated vehicle HMIs but might also be generalized to related domains such as aviation, robotics or health care.

International audience; We formalise the undecidability of solvability of Diophantine equations, i.e. polynomial equations over natural numbers, in Coq's constructive type theory. To do so, we give the first full mechanisation of the Davis-Putnam-Robinson-Matiyasevich theorem, stating that every recursively enumerable problem-in our case by a Minsky machine-is Diophantine. We obtain an elegant and comprehensible proof by using a synthetic approach to computability and by introducing Conway's FRACTRAN language as intermediate layer.