The Experts below are selected from a list of 246 Experts worldwide ranked by ideXlab platform
John Case - One of the best experts on this subject based on the ideXlab platform.
-
Effectivity questions for Kleene's Recursion Theorem
Theoretical Computer Science, 2018Co-Authors: John Case, Sanjay Jain, Frank StephanAbstract:Abstract The present paper investigates the quality of numberings measured in three different ways: (a) the complexity of finding witnesses of Kleene's Recursion Theorem in the numbering; (b) for which learning notions from inductive inference the numbering is an optimal hypothesis space; (c) the complexity needed to translate the indices of other numberings to those of the given one. In all three cases, one assumes that the corresponding witnesses or correct hypotheses are found in the limit and one measures the complexity with respect to the best criterion of convergence which can be achieved. The convergence criteria considered are those of finite, explanatory, vacillatory and behaviourally correct convergence. The main finding is that the complexity of finding witnesses for Kleene's Recursion Theorem and the optimality for learning are independent of each other. Furthermore, if the numbering is optimal for explanatory learning and also allows to solve Kleene's Recursion Theorem with respect to explanatory convergence, then it also allows to translate indices of other numberings with respect to explanatory convergence.
-
effectivity questions for kleene s Recursion Theorem
Foundations of Computer Science, 2013Co-Authors: John Case, Sanjay Jain, Frank StephanAbstract:The present paper explores the interaction between two Recursion-theoretic notions: program self-reference and learning partial recursive functions in the limit. Kleene’s Recursion Theorem formalises the notion of program self-reference: It says that given a partial-recursive function ψ p there is an index e such that the e-th function ψ e is equal to the e-th slice of ψ p . The paper studies constructive forms of Kleene’s Recursion Theorem which are inspired by learning criteria from inductive inference and also relates these constructive forms to notions of learnability. For example, it is shown that a numbering can fail to satisfy Kleene’s Recursion Theorem, yet that numbering can still be used as a hypothesis space when learning explanatorily an arbitrary learnable class. The paper provides a detailed picture of numberings separating various versions of Kleene’s Recursion Theorem and learnability.
-
LFCS - Effectivity Questions for Kleene's Recursion Theorem
Logical Foundations of Computer Science, 2013Co-Authors: John Case, Sanjay Jain, Frank StephanAbstract:The present paper explores the interaction between two Recursion-theoretic notions: program self-reference and learning partial recursive functions in the limit. Kleene’s Recursion Theorem formalises the notion of program self-reference: It says that given a partial-recursive function ψ p there is an index e such that the e-th function ψ e is equal to the e-th slice of ψ p . The paper studies constructive forms of Kleene’s Recursion Theorem which are inspired by learning criteria from inductive inference and also relates these constructive forms to notions of learnability. For example, it is shown that a numbering can fail to satisfy Kleene’s Recursion Theorem, yet that numbering can still be used as a hypothesis space when learning explanatorily an arbitrary learnable class. The paper provides a detailed picture of numberings separating various versions of Kleene’s Recursion Theorem and learnability.
-
Memory-limited non-U-shaped learning with solved open problems
Theoretical Computer Science, 2013Co-Authors: John Case, Timo KötzingAbstract:In empirical cognitive science, for human learning, a semantic or behavioral U-shape occurs when a learner first learns, then unlearns, and, finally, relearns, some target concept. Within the formal framework of Inductive Inference, for learning from positive data, previous results have shown, for example, that such U-shapes are unnecessary for explanatory learning, but are necessary for behaviorally correct and non-trivial vacillatory learning. Herein we also distinguish between semantic and syntactic U-shapes. We answer a number of open questions in the prior literature as well as provide new results regarding syntactic U-shapes. Importantly for cognitive science, we see more of a previously noticed pattern that, for parameterized learning criteria, beyond very few initial parameter values, U-shapes are necessary for full learning power. We analyze the necessity of U-shapes in two memory-limited settings. The first setting is Bounded Memory State (BMS) learning, where a learner has an explicitly-bounded state memory, and otherwise only knows its current datum. We show that there are classes learnable with three (or more) memory states that are not learnable non-U-shapedly with any finite number of memory states. This result is surprising, since, for learning with one or two memory states, U-shapes are known to be unnecessary. This solves an open question from the literature. The second setting is that of Memoryless Feedback (MLF) learning, where a learner may ask a bounded number of questions about what data has been seen so far, and otherwise only knows its current datum. We show that there is a class learnable memorylessly with a single feedback query such that this class is not learnable non-U-shapedly memorylessly with any finite number of feedback queries. We employ self-learning classes together with the Operator Recursion Theorem for many of our results, but we also introduce two new techniques for obtaining results. The first is for transferring inclusion results from one setting to another. The main part of the second is the Hybrid Operator Recursion Theorem, which enables us to separate some learning criteria featuring complexity-bounded learners, employing self-learning classes. Both techniques are not specific to U-shaped learning, but applicable for a wide range of settings.
-
Program Self-Reference in Constructive Scott Subdomains
Theory of Computing Systems, 2012Co-Authors: John Case, Samuel E. MoeliusAbstract:Intuitively, a Recursion Theorem asserts the existence of self-referential programs . Two well-known Recursion Theorems are Kleene’s Recursion Theorem ( krt ) and Rogers’ Fixpoint Recursion Theorem ( fprt ). Does one of these two Theorems better capture the notion of program self-reference than the other? In the context of the partial computable functions over the natural numbers ( $\mathcal {PC}$ ), fprt is strictly weaker than krt , in that fprt holds in any effective numbering of $\mathcal {PC}$ in which krt holds, but not vice versa. It is shown that, in this context, the existence of self-reproducing programs (a.k.a. quines ) is assured by krt , but not by fprt . Most would surely agree that a self-reproducing program is self-referential. Thus, this result suggests that krt is better than fprt at capturing the notion of program self-reference in $\mathcal {PC}$ . A generalization of krt to arbitrary constructive Scott subdomains is then given. (For fprt , a similar generalization was already known.) Surprisingly, for some such subdomains, the two Theorems turn out to be equivalent . A precise characterization is given of those constructive Scott subdomains in which this occurs. For such subdomains, the two Theorems capture the notion of program self-reference equally well.
Konrad Slind - One of the best experts on this subject based on the ideXlab platform.
-
Wellfounded schematic definitions
Lecture Notes in Computer Science, 2000Co-Authors: Konrad SlindAbstract:A program scheme looks like a recursive function definition, except that it has free variables 'on the right hand side'. As is well-known, equalities between schemes can capture powerful program transformations, e.g., translation to tail-recursive form. In this paper, we present a simple and general way to define program schemes, based on a particular form of the wellfounded Recursion Theorem. Each program scheme specifies a schematic induction Theorem, which is automatically derived by formal proof from the wellfounded induction Theorem. We present a few examples of how formal program transformations are expressed and proved in our approach. The mechanization reported here has been incorporated into both the HOL and Isabelle/HOL systems.
-
CADE - Wellfounded Schematic Definitions
Automated Deduction - CADE-17, 2000Co-Authors: Konrad SlindAbstract:A program scheme looks like a recursive function definition, except that it has free variables ‘on the right hand side’. As is well-known, equalities between schemes can capture powerful program transformations, e.g., translation to tail-recursive form. In this paper, we present a simple and general way to define program schemes, based on a particular form of the wellfounded Recursion Theorem. Each program scheme specifies a schematic induction Theorem, which is automatically derived by formal proof from the wellfounded induction Theorem. We present a few examples of how formal program transformations are expressed and proved in our approach. The mechanization reported here has been incorporated into both the HOL and Isabelle/HOL systems.
-
function definition in higher order logic
Theorem Proving in Higher Order Logics, 1996Co-Authors: Konrad SlindAbstract:We use a formally proven wellfounded Recursion Theorem as the basis upon which to build a function definition facility for Higher Order Logic. This approach offers flexibility in the choice of wellfounded relations used, the deferral of termination arguments, and automatic isolation of termination conditions. Building on this platform, we provide the ability to define recursive functions via pattern matching. The system is parameterized and has been instantiated to quite different Theorem provers.
-
TPHOLs - Function Definition in Higher-Order Logic
Lecture Notes in Computer Science, 1996Co-Authors: Konrad SlindAbstract:We use a formally proven wellfounded Recursion Theorem as the basis upon which to build a function definition facility for Higher Order Logic. This approach offers flexibility in the choice of wellfounded relations used, the deferral of termination arguments, and automatic isolation of termination conditions. Building on this platform, we provide the ability to define recursive functions via pattern matching. The system is parameterized and has been instantiated to quite different Theorem provers.
Jean-yves Marion - One of the best experts on this subject based on the ideXlab platform.
-
From Turing machines to computer viruses
Philosophical Transactions of the Royal Society A: Mathematical Physical and Engineering Sciences, 2012Co-Authors: Jean-yves MarionAbstract:Self-replication is one of the fundamental aspects of computing where a program or a system may duplicate, evolve and mutate. Our point of view is that Kleene's (second) Recursion Theorem is essential to understand self-replication mechanisms. An interesting example of self-replication codes is given by computer viruses. This was initially explained in the seminal works of Cohen and of Adleman in the 1980s. In fact, the different variants of Recursion Theorems provide and explain constructions of self-replicating codes and, as a result, of various classes of malware. None of the results are new from the point of view of computability theory. We now propose a self-modifying register machine as a model of computation in which we can effectively deal with the self-reproduction and in which new offsprings can be activated as independent organisms.
-
A Classification of Viruses through Recursion Theorems
2007Co-Authors: Guillaume Bonfante, Matthieu Kaczmarek, Jean-yves MarionAbstract:We study computer virology from an abstract point of view. Viruses and worms are self-replicating programs, whose definitions are based on Kleene's second Recursion Theorem. We introduce a notion of delayed Recursion that we apply to both Kleene's second Recursion Theorem and Smullyan's double Recursion Theorem. This leads us to define four classes of viruses, two of them being polymorphic. Then, we work on a simple imperative programming language in order to show how those theoretical constructions can be implemented. In particular, we propose a general virus builder, and distribution engines.
-
CiE - A Classification of Viruses Through Recursion Theorems
Lecture Notes in Computer Science, 2007Co-Authors: Guillaume Bonfante, Matthieu Kaczmarek, Jean-yves MarionAbstract:We study computer virology from an abstract point of view. Viruses and worms are self-replicating programs, whose constructions are essentially based on Kleene's second Recursion Theorem. We show that we can classify viruses as solutions of fixed point equations which are obtained from different versions of Kleene's second Recursion Theorem. This lead us to consider four classes of viruses which various polymorphic features. We propose to use virus distribution in order to deal with mutations. Topics covered.Computability theoretic aspects of programs, computer virology.
-
On Abstract Computer Virology from a Recursion Theoretic Perspective
Journal in Computer Virology, 2006Co-Authors: Guillaume Bonfante, Matthieu Kaczmarek, Jean-yves MarionAbstract:We are concerned with theoretical aspects of computer viruses. For this, we suggest a new definition of viruses which is clearly based on the iteration Theorem and above all on Kleene's Recursion Theorem. We in this study capture in a natural way previous definitions, and in particular the one of Adleman. We establish generic virus constructions and we illustrate them by various examples. Lastly, we show the results on virus detection.
-
Toward an abstract computer virology
2005Co-Authors: Guillaume Bonfante, Matthieu Kaczmarek, Jean-yves MarionAbstract:We are concerned with theoretical aspects of computer viruses. For this, we suggest a new definition of viruses which is clearly based on the iteration Theorem and above all on Kleene's Recursion Theorem. We show that we capture in a natural way previous definitions, and in particular the one of Adleman. We establish generic constructions in order to construct viruses, and we illustrate them by various examples. We discuss about the relationship between information theory and virus and we propose a defense against some kind of viral propagation. Lastly, we show that virus detection is Π 02 -complete. However, since we are able to deal with system vulnerability, we exhibit another defense based on controlling system access.
Frank Stephan - One of the best experts on this subject based on the ideXlab platform.
-
Effectivity questions for Kleene's Recursion Theorem
Theoretical Computer Science, 2018Co-Authors: John Case, Sanjay Jain, Frank StephanAbstract:Abstract The present paper investigates the quality of numberings measured in three different ways: (a) the complexity of finding witnesses of Kleene's Recursion Theorem in the numbering; (b) for which learning notions from inductive inference the numbering is an optimal hypothesis space; (c) the complexity needed to translate the indices of other numberings to those of the given one. In all three cases, one assumes that the corresponding witnesses or correct hypotheses are found in the limit and one measures the complexity with respect to the best criterion of convergence which can be achieved. The convergence criteria considered are those of finite, explanatory, vacillatory and behaviourally correct convergence. The main finding is that the complexity of finding witnesses for Kleene's Recursion Theorem and the optimality for learning are independent of each other. Furthermore, if the numbering is optimal for explanatory learning and also allows to solve Kleene's Recursion Theorem with respect to explanatory convergence, then it also allows to translate indices of other numberings with respect to explanatory convergence.
-
effectivity questions for kleene s Recursion Theorem
Foundations of Computer Science, 2013Co-Authors: John Case, Sanjay Jain, Frank StephanAbstract:The present paper explores the interaction between two Recursion-theoretic notions: program self-reference and learning partial recursive functions in the limit. Kleene’s Recursion Theorem formalises the notion of program self-reference: It says that given a partial-recursive function ψ p there is an index e such that the e-th function ψ e is equal to the e-th slice of ψ p . The paper studies constructive forms of Kleene’s Recursion Theorem which are inspired by learning criteria from inductive inference and also relates these constructive forms to notions of learnability. For example, it is shown that a numbering can fail to satisfy Kleene’s Recursion Theorem, yet that numbering can still be used as a hypothesis space when learning explanatorily an arbitrary learnable class. The paper provides a detailed picture of numberings separating various versions of Kleene’s Recursion Theorem and learnability.
-
LFCS - Effectivity Questions for Kleene's Recursion Theorem
Logical Foundations of Computer Science, 2013Co-Authors: John Case, Sanjay Jain, Frank StephanAbstract:The present paper explores the interaction between two Recursion-theoretic notions: program self-reference and learning partial recursive functions in the limit. Kleene’s Recursion Theorem formalises the notion of program self-reference: It says that given a partial-recursive function ψ p there is an index e such that the e-th function ψ e is equal to the e-th slice of ψ p . The paper studies constructive forms of Kleene’s Recursion Theorem which are inspired by learning criteria from inductive inference and also relates these constructive forms to notions of learnability. For example, it is shown that a numbering can fail to satisfy Kleene’s Recursion Theorem, yet that numbering can still be used as a hypothesis space when learning explanatorily an arbitrary learnable class. The paper provides a detailed picture of numberings separating various versions of Kleene’s Recursion Theorem and learnability.
-
kolmogorov complexity and the Recursion Theorem
Transactions of the American Mathematical Society, 2011Co-Authors: Bjorn Kjoshanssen, Wolfgang Merkle, Frank StephanAbstract:Several classes of diagonally nonrecursive (DNR) functions are characterized in terms of Kolmogorov complexity. In particular, a set of natural numbers A can wtt-compute a DNR function iff there is a nontrivial recursive lower bound on the Kolmogorov complexity of the initial segments of A. Furthermore, A can Turing compute a DNR function iff there is a nontrivial A-recursive lower bound on the Kolmogorov complexity of the initial segments of A. A is PA-complete, that is, A can compute a {0, 1}-valued DNR function, iff A can compute a function F such that F(n) is a string of length n and maximal C-complexity among the strings of length n. A ≥ T K iff A can compute a function F such that F(n) is a string of length n and maximal H-complexity among the strings of length n. Further characterizations for these classes are given. The existence of a DNR function in a Turing degree is equivalent to the failure of the Recursion Theorem for this degree; thus the provided results characterize those Turing degrees in terms of Kolmogorov complexity which no longer permit the usage of the Recursion Theorem.
-
kolmogorov complexity and the Recursion Theorem
arXiv: Logic, 2009Co-Authors: Bjorn Kjoshanssen, Wolfgang Merkle, Frank StephanAbstract:Several classes of DNR functions are characterized in terms of Kolmogorov complexity. In particular, a set of natural numbers A can wtt-compute a DNR function iff there is a nontrivial recursive lower bound on the Kolmogorov complexity of the initial segments of A. Furthermore, A can Turing compute a DNR function iff there is a nontrivial A-recursive lower bound on the Kolmogorov complexity of the initial segements of A. A is PA-complete, that is, A can compute a {0,1}-valued DNR function, iff A can compute a function F such that F(n) is a string of length n and maximal C-complexity among the strings of length n. A solves the halting problem iff A can compute a function F such that F(n) is a string of length n and maximal H-complexity among the strings of length n. Further characterizations for these classes are given. The existence of a DNR function in a Turing degree is equivalent to the failure of the Recursion Theorem for this degree; thus the provided results characterize those Turing degrees in terms of Kolmogorov complexity which do no longer permit the usage of the Recursion Theorem.
Samuel E. Moelius - One of the best experts on this subject based on the ideXlab platform.
-
Program Self-Reference in Constructive Scott Subdomains
Theory of Computing Systems, 2012Co-Authors: John Case, Samuel E. MoeliusAbstract:Intuitively, a Recursion Theorem asserts the existence of self-referential programs . Two well-known Recursion Theorems are Kleene’s Recursion Theorem ( krt ) and Rogers’ Fixpoint Recursion Theorem ( fprt ). Does one of these two Theorems better capture the notion of program self-reference than the other? In the context of the partial computable functions over the natural numbers ( $\mathcal {PC}$ ), fprt is strictly weaker than krt , in that fprt holds in any effective numbering of $\mathcal {PC}$ in which krt holds, but not vice versa. It is shown that, in this context, the existence of self-reproducing programs (a.k.a. quines ) is assured by krt , but not by fprt . Most would surely agree that a self-reproducing program is self-referential. Thus, this result suggests that krt is better than fprt at capturing the notion of program self-reference in $\mathcal {PC}$ . A generalization of krt to arbitrary constructive Scott subdomains is then given. (For fprt , a similar generalization was already known.) Surprisingly, for some such subdomains, the two Theorems turn out to be equivalent . A precise characterization is given of those constructive Scott subdomains in which this occurs. For such subdomains, the two Theorems capture the notion of program self-reference equally well.
-
Properties Complementary to Program Self-Reference
Fundamenta Informaticae, 2011Co-Authors: John Case, Samuel E. MoeliusAbstract:In computability theory, program self-reference is formalized by the not-necessarily-constructive form of Kleene's Recursion Theorem (krt). In a programming system in which krt holds, for any preassigned, algorithmic task, there exists a program that, in a sense, creates a copy of itself, and then performs that task using the self-copy. Interpreted in this way, such self-copying programs have usable self-knowledge. Herein, properties complementary to krt are considered. Of particular interest are those properties involving the implementation of control structures. One main result is that no property involving the implementation of denotational control structures is complementary to krt. This is in contrast to a result of Royer, which showed that implementation of if-then-else — a denotational control structure — is complementary to the constructive form of Kleene's Recursion Theorem. Examples of non-denotational control structures whose implementation is complementary to krt are then given. Some such control structures so nearly resemble denotational control structures that they might be called quasi-denotational.
-
Characterizing Programming Systems Allowing Program Self-Reference
Theory of Computing Systems, 2009Co-Authors: John Case, Samuel E. MoeliusAbstract:The interest is in characterizing insightfully the power of program self-reference in effective programming systems ( $\mathsf{epses}$ ), the computability-theoretic analogs of programming languages (for the partial computable functions). In an $\mathsf{eps}$ in which the constructive form of Kleene’s Recursion Theorem ( KRT ) holds, it is possible to construct, algorithmically, from an arbitrary algorithmic task, a self-referential program that, in a sense, creates a self-copy and then performs that task on the self-copy. In an $\mathsf{eps}$ in which the not-necessarily -constructive form of Kleene’s Recursion Theorem ( krt ) holds, such self-referential programs exist, but cannot, in general, be found algorithmically. In an earlier effort, Royer proved that there is no collection of recursive denotational control structures whose implementability characterizes the $\mathsf{epses}$ in which KRT holds. One main result herein, proven by a finite injury priority argument, is that the $\mathsf{epses}$ in which krt holds are, similarly, not characterized by the implementability of some collection of recursive denotational control structures. On the positive side, however, a characterization of such $\mathsf{epses}$ of a rather different sort is shown herein. Though, perhaps not the insightful characterization sought after, this surprising result reveals that a hidden and inherent constructivity is always present in krt .
-
CiE - Program Self-reference in Constructive Scott Subdomains
Mathematical Theory and Computational Practice, 2009Co-Authors: John Case, Samuel E. MoeliusAbstract:Intuitively, a Recursion Theorem asserts the existence of self-referential programs . Two well-known Recursion Theorems are Kleene's Recursion Theorem (krt) and Rogers' Fixpoint Recursion Theorem (fprt). Does one of these two Theorems better capture the notion of program self-reference than the other? In the context of the partial computable functions over the natural numbers ( ), fprt is strictly weaker than krt, in that fprt holds in any effective numbering of in which krt holds, but not vice versa. It is shown that, in this context, the existence of self-reproducing programs (a.k.a. quines ) is assured by krt, but not by fprt. Most would surely agree that a self-reproducing program is self-referential. Thus, this result suggests that krt is better than fprt at capturing the notion of program self-reference in . A generalization of krt to arbitrary constructive Scott subdomains is then given. (For fprt, a similar generalization was already known.) Surprisingly, for some such subdomains, the two Theorems turn out to be equivalent . A precise characterization is given of those constructive Scott subdomains in which this occurs. For such subdomains, the two Theorems capture the notion of program self-reference equally well.
-
Program self-reference
2009Co-Authors: John Case, Samuel E. MoeliusAbstract:The interest is in understanding and insightfully characterizing the power of program self-reference (synonyms: self-knowledge, self-reflection). Kleene's Recursion Theorem (krt) formalizes this notion in the context of effective programming systems (epses), the computability theoretic analogs of programming languages for the partial computable functions. krt holds in some epses, but not in others. Thus, to characterize the power of program self-reference is, at least in part, to characterize the epses in which krt holds. This dissertation presents three such characterizations. It also presents several interesting results concerning krt that were obtained along the way. A comparison is given between krt and some other forms of the Recursion Theorem, including Rogers' Fixpoint Recursion Theorem ( fprt). fprt is strictly weaker than krt, in that fprt holds in any eps in which krt holds, but not vice versa. Thus, one could ask: are there programs that one would reasonably call self-referential, and whose existence is assured by krt, but not by fprt? It is shown that self-reproducing programs (a.k.a. quines) satisfy these technical conditions. Since most would surely agree that a self-reproducing program is self-referential, this result suggests that krt is better than fprt at capturing the notion of program self-reference. It is shown that there exist epses in which an extremely non-constructive form of krt holds. Roughly, in such epses, self-referential programs exist, but cannot be found algorithmically—not even with access to an oracle for K (the diagonal halting problem). Several results are presented concerning the relationship between krt and various kinds of control structures. For example, it is shown that there is no class of recursive denotational control structures whose implementation characterizes krt . It is also shown that there is no class of recursive denotational control structures whose implementation is complementary to krt. This latter result is in contrast to a result of Royer, which showed that implementation of if-then-else—a denotational control structure—is complementary to the constructive form of Kleene's Recursion Theorem. On the other hand, it is shown that there exist non-denotational control structures whose implementation is complementary to krt. Examples of such control structures are given herein. The proofs of several of these results involve priority methods.