.A term rewrite system is called simply terminating if its termination can be shown by means of a simplification ordering. According to a result of Weiermann, the derivation length function of any simply terminating finite rewrite system is eventually dominated by a Hardy function of ordinal less than the small Veblen ordinal. This bound had appeared to be of rather theoretical nature, because all known examples had had multiple recursive complexities, until recently Touzet constructed simply terminating examples with (...) complexities beyond multiple recursion. This was established by simulating the Hydra battle for all ordinal segments below the proof-theoretic ordinal of Peano arithmetic. By extending this result to the small Veblen ordinal we prove the huge bound of Weiermann to be sharp. As a spin-off we can show that total termination allows for complexities as high as those of simple termination. (shrink)

Let F be a signature and R a strictly orthogonal rewrite system on ground terms of F . We give an effective proof of a bounding condition for R , based on a detailed analysis of how terms are transformed during the rewrite process, which allows us to give recursive bounds on the derivation lengths of terms. We give a syntactic characterisation of the Grzegorczyk hierarchy and a rewriting schema for calculating its functions. As a consequence of this, (...) using results of Elias Tahhan–Bittar, it can be shown that, for n⩾3 , the derivation length functions for functions in Grzegorczyk class E n belong to Grzegorczyk class E n+1 . We also give recursive bounds for the derivation lengths of functions defined by parameter recursion. (shrink)

Recently, Brass and Dix showed 143–165) that the well founded semantics WFS can be defined as a confluent calculus of transformation rules. This led not only to a simple extension to disjunctive programs 167–213), but also to a new computation of the well-founded semantics which is linear for a broad class of programs. We take this approach as a starting point and generalize it considerably by developing a general theory of Confluent LP-systems CS . Such a system CS is (...) a rewriting system on the set of all logic programs over a fixed signature L and it induces in a natural way a canonical semantics. Moreover, we show four important applications of this theory: most of the well-known semantics are induced by confluent LP-systems , there are many more transformation rules that lead to confluent LP-systems , semantics induced by such systems can be used to model aggregation , the new systems can be used to construct interesting counterexamples to some conjectures about the space of well-behaved semantics. (shrink)

We present a characterization of confluence for term rewriting systems, which is then refined for special classes of rewriting systems. The refined characterization is used to obtain a polynomial time algorithm for deciding the confluence of ground term rewrite systems. The same approach also shows the decidability of confluence for shallow and linear term rewriting systems. The decision procedure has a polynomial time complexity under the assumption that the maximum arity of a function symbol in (...) the signature is a constant. (shrink)

The termination of rewrite systems for parameter recursion, simple nested recursion and unnested multiple recursion is shown by using monotone interpretations both on the ordinals below the first primitive recursively closed ordinal and on the natural numbers. We show that the resulting derivation lengths are primitive recursive. As a corollary we obtain transparent and illuminating proofs of the facts that the schemata of parameter recursion, simple nested recursion and unnested multiple recursion lead from primitive recursive functions to primitive (...) recursive functions. (shrink)

The “official” history of connexive logic was written in 2012 by Storrs McCall who argued that connexive logic was founded by ancient logicians like Aristotle, Chrysippus, and Boethius; that it was further developed by medieval logicians like Abelard, Kilwardby, and Paul of Venice; and that it was rediscovered in the 19th and twentieth century by Lewis Carroll, Hugh MacColl, Frank P. Ramsey, and Everett J. Nelson. From 1960 onwards, connexive logic was finally transformed into non-classical calculi which partly concur with (...) systems of relevance logic and paraconsistent logic. In this paper it will be argued that McCall’s historical analysis is fundamentally mistaken since it doesn’t take into account two versions of connexivism. While “humble” connexivism maintains that connexive properties only apply to “normal” antecedents, “hardcore” connexivism insists that they also hold for “abnormal” propositions. It is shown that the overwhelming majority of the forerunners of connexive logic were only “humble” connexivists. Their ideas concerning connexive implication don’t give rise, however, to anything like a non-classical logic. (shrink)

The main powerful method for establishing termination of term rewriting systems was discovered by Nachum Dershowitz through the introduction of certain natural well founded orderings (lexicographic path orderings). This leads to natural decision problems which may be of the highest computational complexity of any decidable problems appearing in a natural established computer science context.

In various documents the view emerges that contemporary biotechnosciences are currently experiencing a scientific revolution: a massive increase of pace, scale and scope. A significant part of the research endeavours involved in this scientific upheaval is devoted to understanding and, if possible, ameliorating humankind: from our genomes up to our bodies and brains. New developments in contemporary technosciences, such as synthetic biology and other genomics and “post-genomics” fields, tend to blur the distinctions between prevention, therapy and enhancement. An important dimension (...) of this development is “biomimesis”: i.e. the tendency of novel technologies and materials to mimic or plagiarize nature on a molecular and microscopic level in order to optimise prospects for the embedding of technological artefacts in natural systems such as human bodies and brains. In this paper, these developments are read and assessed from a psychoanalytical perspective. Three key concepts from psychoanalysis are used to come to terms with what is happening in research laboratories today. After assessing the general profile of the current revolution in this manner, I will focus on a particular case study, a line of research that may serve as exemplification of the vicissitudes of contemporary technosciences, namely viral biomaterials. Viral life forms can be genetically modified (their genomes can be rewritten) in such a manner that they may be inserted in human bodies in order to produce substances at specific sites such as hormones (testosterone), neurotransmitters (dopamine), enzymes (insulin) or bone and muscle tissue. Notably, certain target groups such as top athletes, soldiers or patients suffering from degenerative diseases may become the pioneers serving as research subjects for novel applications. The same technologies can be used for various purposes ranging from therapy up to prevention and enhancement. (shrink)

The debate on sustainable globalized development rests on two clearly stated economic assumptions: that "development" proceeds, solely and inevitably, through industrialization and the proliferation of capital intensive high-technology, towards the creation of service sector economies; and that globalization, based on a neoliberal, capitalist, free market ideology, provides the only vehicle for such development. Sustainability, according to the proponents of globalized development, is merely a function of market forces, which will generate the solutions for all problems including the environmental dilemmas that (...) loom over the globe today. The social focus of globalized development is clearly the "individual" and the much-touted goal of development in the context of these debates, is the emancipation of the individual from want. This glorification of the individual, so characteristic of the Enlightenment, has defined all aspects of modernity, leading to approaches that are self-focused and that give little thought to the needs of society or even the social context. The increasing impoverishment of human life and the growing environmental degradation, however, provide a poignant counterpoint to this onrush of capital interests, demanding a reassessment of sustainability separate from the logic of industrialization and globalized development. This paper examines the unfolding of the logic of capitalism, which underlies the structure of the Rostowian model of development and the problems in the assumptions underlying today''s globalized development process. The evident impossibility of sustainability in the current growth-based market system leads to the examination of alternatives including a reflexive understanding of the choices and the inclusion of opportunity costs, related to the social, environmental and economic aspects of decision making. The integration of all factors of production into the logic of development provides a sustainable alternative to the current system. (shrink)

Inspired by Judith Butler's conceptualization of drag as ‘gender parody’, I develop the conceptual frame of ‘textual drag’ in order to define and examine the relationship between parody, satire and gender. I test this frame by reading two seminal feminist works, Virginia Woolf's Orlando and Monique Wittig's Le Corps lesbien. Both texts lend themselves particularly persuasively to analysis with this frame, as they each use parodic strategies to facilitate proto-queer satirical critiques of reductive gender norms. Orlando deploys an exaggerated nineteenth-century (...) biographical style, which foregrounds the protagonist's gender fluidity and her developing critique of the norms and systems that surround her, while Le Corps lesbien rewrites canonical romance narratives from a lesbian perspective, challenging the heterosexism inherent in these narratives and providing new modes of thinking about gender, desire and sexual interaction. (shrink)

Brown famously held that in the field of public education, segregation has no place. But segregation was undefined. Was segregation constituted by mere racial classification, by the fact that the state had divided children into racial groups? Or did Brown condemn a caste system whose effect was to stigmatize black children. In Parents Involved v. Seattle Justice Roberts says segregation is about children not black children. This colorblind approach represents both a rewriting and appropriation of Brown in the service of (...) formalism. The Roberts court writes not only a new version of Brown but a new historical narrative about the meaning of segregation. The theme of this new story is formal equality - equality of opportunity only - as a universal ideal. This new story is woven entirely out of the language of Brown detached from all historical context. Conservatives have long canonized Brown. It has been a kind of second constitution for the second reconstruction. But how does this new story compare to the original understanding ?: Was this the evil that Brown denounced? By framing the issue in this way the paper seeks to make an end run around an impasse in our social and legal debate. Many progressive scholars have challenged the conservative conception of formal equality by suggesting alternative ways of thinking about it: anti-subordination models, a heightened call that equality should take issues of racial caste into account. But this external critique has stalled, perhaps in part because of the slippery indeterminacy of normative ideals. Segregation is far more determinate; it is something that has been concretized not only by the lived experience of black people, but by an earlier realist tradition on the part of the Warren court which saw it as it was. Retelling the two parts of this forgotten history we expose the disconnect between the Supreme Court's universalism and the actual meaning of segregation in context. Also, by focusing on the original understanding we seek a kind of internal critique showing how the politics of historical revision does not withstand the conservatives own interpretive approach. (shrink)

We re-express our theorem on the strong-normalisation of display calculi as a theorem about the well-foundedness of a certain ordering on first-order terms, thereby allowing us to prove the termination of systems of rewrite rules. We first show how to use our theorem to prove the well-foundedness of the lexicographic ordering, the multiset ordering and the recursive path ordering. Next, we give examples of systems of rewrite rules which cannot be handled by these methods but which (...) can be handled by ours. Finally, we show that our method can also prove the termination of the Knuth-Bendix ordering and of dependency pairs. Keywords: rewriting, termination, well-founded ordering, recursive path ordering.. (shrink)

In this paper, we give a step by step introduction to the theory of well quasi-ordered transition systems. The framework combines two concepts, namely (i) transition systems which are monotonic wrt. a well-quasi ordering ; and (ii) a scheme for symbolic backward reachability analysis. We describe several models with infinite-state spaces, which can be analyzed within the framework, e.g., Petri nets, lossy channel systems, timed automata, timed Petri nets, and multiset rewriting systems. We will also present (...) better quasi-ordered transition systems which allow the design of efficient symbolic representations of infinite sets of states. (shrink)

Logic is traditionally considered to be a purely syntactic discipline, at least in principle. However, prof. David Isles has shown that this ideal is not yet met in traditional logic. Semantic residue is present in the assumption that the domain of a variable should be fixed in advance of a derivation, and also in the notion that a numerical notation must refer to a number rather than be considered a mathematical object in and of itself. Based on his work, the (...) central question of this thesis is what kind of logic, if any, results from removing this semantic residue from traditional logic.We differ from traditional logic in two significant ways. The first is that the assumption that a numerical notation must refer to a number is denied. Numerical notations are considered as mathematical objects in their own right, related to each other by means of rewrite rules. The traditional notion of reference is then replaced by the notion of reduction (by means of the rewrite rules) to a normal form. Two numerical notations that reduce to the same normal form would traditionally be considered identical, as they would refer to the same number, and hence they would be interchangeable salva veritate. In the new system, called Buridan-Volpin (BV), the numerical notations themselves are the elements of the domains of variables, and two numerical notations that reduce to the same normal form need not be interchangeable salva veritate, except when they are syntactically identical (i.e., have the same Gödel number).The second is that we do away with the assumption that the domains of variables need to be fixed in advance of a derivation. Instead we focus on what is needed to guarantee preservation of truth in every step of a derivation. These conditions on the domains of the variables, accumulated in the course of a derivation, are combined in a reference grammar. Whereas traditionally a derivation is considered valid when the conclusion follows from the premisses by way of the derivation rules (and possibly axioms), in the BV system a derivation must meet the extra condition that no inconsistency occurs within the reference grammar. For if the reference grammar were to give rise to inconsistency (i.e., it would be impossible to assign domains to all the variables without breaking at least one of the conditions placed on them in the reference grammar), there is no longer a guarantee that truth has been preserved in every step of the derivation, and hence the truth of the conclusion is not guaranteed by the derivation.In Chapter 2 the BV system is introduced in some formal detail. Chapter 3 gives some examples of derivations, notably totality of addition, multiplication and exponentiation, as well as a lemma needed for the proof of Euclid’s Theorem. These examples, taken from prof. Isles’ First-Order Reasoning and Primitive Recursive Natural Number Notations, show that there is a real proof-theoretical difference between traditional logic and the BV system. Here we also find the first major point of departure between myself and prof. Isles, centered on the notion of inheritance of conditions in the reference grammar by way of lemmata. These different points of view are best illustrated in the sections on the totality of exponentiation and on Euclid’s Lemma: prof. Isles maintains that the proof of totality of exponentiation is not BV valid, while I maintain that it is. But I do agree with him that the traditional proof of Euclid’s Lemma is not BV valid. Chapter 6 also expands the arguments for my choice in this matter.Now that it has been shown that there is a difference between traditional logic and BV, the properties of BV need to be examined. In Chapter 4 we give a proof of Cut-elimination for BV minus induction and the subformula property for BV, which allows us to prove the consistency of BV minus induction. We also expand on the reasons for excluding induction. In Chapter 5 we consider in detail the proof of a finite analog to the Löwenheim–Skolem theorem given by prof. Isles in his article with the same title. He proves that under certain conditions it is always possible, given the existence of a (possibly uncountable) model for a derivation, to give a finite model for this derivation. The system he considers deviates from BV as considered in this thesis in two significant ways: it does not contain the induction rule and the domains contain numbers instead of numerical notations. We then go on to show that it is possible to extend the result to include induction, in the sense that the existence of a possibly uncountable model for a derivation guarantees the existence of a model that is at most countable. We also consider the complications that arise from taking numerical expressions instead of numbers as the elements of domains.Finally, in Chapter 6 we consider the philosophical consequences of the BV system, informed by the formal results from the previous chapters. In particular we discuss the relation between reduction and reference, the status of reference grammars, the notion of induction and its function within BV, and some brief considerations on the consequences of the BV system for the discussion regarding nominalism and realism with regard to mathematical objects. The object of the chapter is twofold. On the one hand applying the formal results to philosophical questions, on the other hand arguing that BV is not just a theoretically acceptable alternative to traditional logic, but is in fact deserving of further development and research into its properties. The latter will probably appeal most to those of a nominalist and/or finitist bent.Abstract prepared by Harrie de Swart and Sven Storms.E-mail:[email protected]:https://research.tilburguniversity.edu/files/6170 1294/Storms_The_Buridan_Volpin_04_05_2022.pdf. (shrink)

Twenty years is a long time in the life of a science. While the historical roots of psychology have not changed since the first edition of this book, some of the offshoots of the various theories and systems discussed have been crit ically reexamined and have undergone far-reaching modifications. New and bold research has led to a broadening of perspectives, and recent devel opments in several areas required a considerable amount of rewriting. I have been fortunate in the last (...) fifteen years to have worked with about 2,000 psychologists and other behavioral scientists who contributed to several collected volumes I have edited. As the editor-in-chief of the In ternational Encyclopedia of Psychiatry, Psychology, Psychoanalysis and Neurol ogy, I have had the privilege of reading, scrutinizing, and editing the work of 1,500 experts in psychology and related disciplines. In addition, I have written several books and monographs and over one hundred scientific papers. Armed with all that experience, I have carefully examined the pages of the first edition. Chapter 8 required substantial rewriting and several new sections have been added to other chapters: "Current Soviet Psychol ogy" (Chapter 2, Section 7); "New Ideas on Purposivism" (Chapter 5, Sec tion 4); "Recent Developments in the Sociological School of Psychoanalysis" (Chapter 9, Section 4); and "Present Status of Gestalt Psychology" (Chapter 12, Section 4). Chapter 15 was omitted, and two new chapters were added: Chapter 14 ("Humanistic Psychology") and Chapter 16 ("Selected Research Areas"). (shrink)

This essay examines the experience of rewriting historical narratives from a world-system perspective, drawing on the author's attempt to construct an integrated image of the world economy in the thirteenth century. Searching for an intermediate epistemological path between unanchored postmodern hermeneutics and overconfident positivism, the author argues that three apparent deviations from the "ideals of positivist social science," which she ironically labels eccentricity, ideology, and idiosyncrasy, can yield significant "remakings" of world history. Eccentricity, namely, recognizing perspectives other than those that (...) conventionally view the world through the eyes of the West, can help historians to escape from ethnocentrism or Eurocentrism. Ideology, more conventionally called theory, is essential if historians are to select and integrate new material. And idiosyncrasy in the interests and backgrounds of historians can often be the source of the re-vision so essential for challenging earlier historical narratives. The author alludes to parallels with ethnographic research methods and cautions against substituting these three aids to research for rigorous attention to empirical sources and "the real world.". (shrink)

For several years now, Siegfried J. Schmidt’s work has provided an important complement to the field, as it bases constructivism in a philosophical and socio-cultural context. With his new book, he develops this approach, striving to overcome simplistic models that fail to specify how human constructions come into being, to challenge traditional dualistic models, and to show how social systems emerge and function… The book provides an important, prolific and strong case for constructivism as a theory of communication.

The International workshop 'Frontiers of Combining Systems' is the only forum that is exclusively devoted to research efforts in this interdisciplinary area. This volume contains selected, edited papers from the second installment of the workshop. The contributions range from theorem proving, rewriting and logic to systems and constraints. While there is a clear emphasis on automated tools and logics, the contributions to this volume show that there exists a rapidly expanding body of solutions of particular instances of the (...) combination problem, and at the same time, that the issue of developing general frameworks for intergrating formalisms and systems is taking on an increasingly important position on the international research agenda. The idea of combining formal systems and algorithms has been attracting interest in areas as diverse as constraint logic programming, automated deduction, verification, information retrieval, computational linguistics, artificial intelligence, and logic. As any interesting real world system is a complex composite entity, decomposing its descriptive requirements (for design, verification, or maintenance purposes) into simpler, more restricted tasks is appealing as it is often the only plausible way of tackling complex modelling problems. A core body of notions, questions and results is beginning to emerge in the area, and we are beginning to understand the computational and logical impact of combining methods and algorithms. (shrink)

This book constitutes the refereed proceedings of the Third International Workshop on Frontiers of Combining Systems, FroCoS 2000, held in Nancy, France, in March 2000.The 14 revised full papers presented together with four invited papers were carefully reviewed and selected from a total of 31 submissions. Among the topics covered are constraint processing, interval narrowing, rewriting systems, proof planning, sequent calculus, type systems, model checking, theorem proving, declarative programming, logic programming, and equational theories.

In this article, I show why it is necessary to abolish the use of predictive algorithms in the US criminal justice system at sentencing. After presenting the functioning of these algorithms in their context of emergence, I offer three arguments to demonstrate why their abolition is imperative. First, I show that sentencing based on predictive algorithms induces a process of rewriting the temporality of the judged individual, flattening their life into a present inescapably doomed by its past. Second, I demonstrate (...) that recursive processes, comprising predictive algorithms and the decisions based on their predictions, systematically suppress outliers and progressively transform reality to match predictions. In my third and final argument, I show that decisions made on the basis of predictive algorithms actively perform a biopolitical understanding of justice as management and modulation of risks. In such a framework, justice becomes a means to maintain a perverse social homeostasis that systematically exposes disenfranchised Black and Brown populations to risk. (shrink)

In this article, I show why it is necessary to abolish the use of predictive algorithms in the US criminal justice system at sentencing. After presenting the functioning of these algorithms in their context of emergence, I offer three arguments to demonstrate why their abolition is imperative. First, I show that sentencing based on predictive algorithms induces a process of rewriting the temporality of the judged individual, flattening their life into a present inescapably doomed by its past. Second, I demonstrate (...) that recursive processes, comprising predictive algorithms and the decisions based on their predictions, systematically suppress outliers and progressively transform reality to match predictions. In my third and final argument, I show that decisions made on the basis of predictive algorithms actively perform a biopolitical understanding of justice as management and modulation of risks. In such a framework, justice becomes a means to maintain a perverse social homeostasis that systematically exposes disenfranchised Black and Brown populations to risk. (shrink)

Deep inference is a natural generalisation of the one-sided sequent calculus where rules are allowed to apply deeply inside formulas, much like rewrite rules in term rewriting. This freedom in applying inference rules allows to express logical systems that are difficult or impossible to express in the cut-free sequent calculus and it also allows for a more fine-grained analysis of derivations than the sequent calculus. However, the same freedom also makes it harder to carry out this analysis, in (...) particular it is harder to design cut elimination procedures. In this paper we see a cut elimination procedure for a deep inference system for classical predicate logic. As a consequence we derive Herbrand's Theorem, which we express as a factorisation of derivations. (shrink)

This paper suggests an online solution for the optimal tracking control of robotic systems based on a single critic neural network -based reinforcement learning method. To this end, we rewrite the robotic system model as a state-space form, which will facilitate the realization of optimal tracking control synthesis. To maintain the tracking response, a steady-state control is designed, and then an adaptive optimal tracking control is used to ensure that the tracking error can achieve convergence in an optimal (...) sense. To solve the obtained optimal control via the framework of adaptive dynamic programming, the command trajectory to be tracked and the modified tracking Hamilton-Jacobi-Bellman are all formulated. An online RL algorithm is the developed to address the HJB equation using a critic NN with online learning algorithm. Simulation results are given to verify the effectiveness of the proposed method. (shrink)

This essay re-examines Hegel’s critique of Spinoza’s Ethics, focusing on the question of method. Are the axioms and definitions unmotivated presuppositions that make the attainment of absolute knowledge impossible in principle, as Hegel charges? This essay develops a new reading of the Ethics to defend it from this critique. I argue that Hegel reads Spinoza as if his system were constructed only according to the mathematical second kind of knowledge, ignoring Spinoza’s clear preference for knowledge of the third kind. The (...) Ethics, I argue, is a book with several layers: it is at once a deductive mathematical system, and a handbook to aid the intuitive power of the active philosophical reader. The letter of each text may be identical, but they have little else in common – Pierre Menard’s rewriting of Don Quixote given systematic philosophical form. (shrink)

The implicational fragment of the relevance logic "ticket entailment" is closely related to the so-called hereditary right maximal terms. I prove that the terms that need to be considered as inhabitants of the types which are theorems of $T_\rightarrow$ are in normal form and built in all but one casefrom B, B' and W only. As a tool in the proof ordered term rewriting systems are introduced. Based on the main theorem I define $FIT_\rightarrow$ - a Fitch-style calculus (related (...) to $FT_\rightarrow$ ) for the implicational fragment of ticket entailment. (shrink)

This paper is concerned with implicit computational complexity of the exptime computable functions. Modifying the lexicographic path order, we introduce a path order EPO. It is shown that a termination proof for a term rewriting system via EPO implies an exponential bound on the lengths of derivations. The path order EPO is designed so that every exptime function is representable as a term rewrite system compatible with EPO (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim).

We consider a deterministic rewrite system for combinatory logic over combinators , and . Terms will be represented by graphs so that reduction of a duplicator will cause the duplicated expression to be "shared" rather than copied. To each normalizing term we assign a weighting which is the number of reduction steps necessary to reduce the expression to normal form. A lambda-expression may be represented by several distinct expressions in combinatory logic, and two combinatory logic expressions are considered equivalent (...) if they represent the same lambda-expression (up to --equivalence). The problem of minimizing the number of reduction steps over equivalent combinator expressions (i.e., the problem of finding the "fastest running" combinator representation for a specific lambda-expression) is proved to be NP-complete by reduction from the "Hitting Set" problem. (shrink)

We show how to encode context-free string grammars, linear context-free tree grammars, and linear context-free rewriting systems as Abstract Categorial Grammars. These three encodings share the same constructs, the only difference being the interpretation of the composition of the production rules. It is interpreted as a first-order operation in the case of context-free string grammars, as a second-order operation in the case of linear context-free tree grammars, and as a third-order operation in the case of linear context-free rewriting (...) class='Hi'>systems. This suggest the possibility of defining an Abstract Categorial Hierarchy. (shrink)

Stephen Wolfram has recently outlined an unorthodox, multicomputational approach to fundamental theory, encompassing not only physics but also mathematics in a structure he calls The Ruliad, understood to be the entangled limit of all possible computations. In this framework, physical laws arise from the the sampling of the Ruliad by observers (including us). This naturally leads to several conceptual issues, such as what kind of object is the Ruliad? What is the nature of the observers carrying out the sampling, and (...) how do they relate to the Ruliad itself? What is the precise nature of the sampling? This paper provides a philosophical examination of these questions, and other related foundational issues, including the identification of a limitation that must face any attempt to describe or model reality in such a way that the modeller-observers are included. (shrink)

The paper discusses the question whether T-theories explain how it is possible to understand new sentences, or learn an infinite language, as Davidson claimed. I argue against some commentators that for explanatory power we need not require that T-theories are implicitly known or mirror cognitive structures. I note contra Davidson that the recursive nature of T-theories is not sufficient for explanatory power, since humans can work out only what is computationally tractable, and recursiveness by itself allows for intractable computational complexity. (...) I finally consider the complexity of T-theories, transformed into term rewriting systems, and find that the complexity of such systems is indeed tractable. Therefore Davidson's claim stands, even though a further condition had to be met. (shrink)