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.

We give a term rewriting characterization of the polyspace functions. Our work follows investigations on term rewriting characterizations of some classes of (sub-) recursive functions as initiated by Cichon and Weiermann [4] and continued by Beckmann and Weiermann [1].The main novelty of this paper is a technique for reformulating recursion schemes. The aim of this technique is to provide rewriting rules which give rise to rewriting chains whose terms are suitably bounded. This bounding is (...) crucial when dealing with computational classes with space constraints. (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.

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 basic notions of the theory of term rewriting are defined for terms that may involve function letters of infinite arity. A sufficient condition for completeness is derived, and its use demonstrated by the example of abstract clones over infinitary signatures.

This paper builds a three-part argument in favour of a more transcendentally focused form of ‘postphenomenology’ than is currently practised in philosophy of technology. It does so by problematising two key terms, ‘constitution’ and ‘postphenomenology’, then by arguing in favour of a ‘transcendental empiricist’ approach that draws on the work of Foucault, Derrida, and, in particular, Deleuze. Part one examines ‘constitution’, as it moves from the context of Husserl’s phenomenology to Ihde and Verbeek’s ‘postphenomenology’. I argue that the term (...) tends towards different senses in these contexts, and that this renders its sense more problematic than the work of Ihde and Verbeek makes it appear. Part two examines ‘postphenomenology’. I argue that putatively ‘poststructuralist’ thinkers such as Derrida, Foucault, and Deleuze may be better characterised as ‘postphenomenologists’, and that approaching them in this way may allow better access to their work from a philosophy of technology perspective. Part three argues for a ‘transcendental empiricist’ approach to philosophy of technology. In doing so, it argues for a rewriting of contemporary philosophy of technology’s political constitution: since an ‘empirical turn’ in the 1990s, I argue, philosophy of technology has been too narrowly focused on ‘empirical’ issues of fact, and not focused enough on ‘transcendental’ issues concerning conditions for these facts. (shrink)

This article reads Maurice Merleau-Ponty's ontology of the “flesh of the world” alongside the ontology that seems to undergird Frantz Fanon's sociodiagnostics as well as his theory of sociogeny. It argues that reading Fanonian sociogeny in terms of the ambiguity and intercorporeality of the flesh of the world renders the ethical and political imperatives of Fanon's decolonial project all the more pressing, since the “new human” is prefigured—if not totally determined—in the national consciousness obtained by “les damnés” through the decolonization (...) process. It then examines how Sylvia Wynter's Fanonian call to (re)fashion the future of humanness through (re)conceptualizing “being human as praxis,” also seems to rely on this ontology of the flesh of the world. Bringing these arguments together, the article suggests that the conceptual content of the new human can be found in the liberation struggles of les damnés across what Wynter calls the “poverty archipelagos” wrought by colonial humanism. Hence, the “new skin” for which Fanon calls is fashioned through forming international solidarity with les damnés, with the conceptual content of the new humanism emerging sociogenically—and autopoetically—from those struggles themselves. (shrink)

.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)

Inoperative Learning draws upon the movement towards a weak philosophy that is currently gaining ground in educational philosophy: this weak philosophy does not offer a set of solutions or guidelines for improving educational outcomes, but rather renders assumptions about the theory-practice coupling that is so popular in contemporary education inoperative. By arguing that such logic reduces education to merely instrumental ends, which can only be assessed in terms of predefined measurement tools, this book presents a challenge to contemporary notions of (...) education as learning. There are various forms of inoperative education that temporarily suspend the goal-directedness of learning. From the perspective of learning, the neutralization of progress, growth, and maturity would usually be seen as obstacles needing to be overcome on the path toward set goals. Yet Lewis argues that a serious investigation of inoperativity opens up possibilities that would be otherwise unavailable in a world fixated on the question of learning. In dialogue with philosophers (Agamben, Benjamin, and Esposito), as well as authors (Kafka and Walser), and qualitative researchers (Lather), Lewis turns our collective attention to what remains when concepts such as learning, child development, teacher effectivity, and personal growth are left idle. Inoperative Learning presents a radical rewriting of educational possibilities. It should therefore be of great interest to educational researchers and educational philosophers concerned with the question of alternative logics of education beyond learning. The book may also be of interest to educational policy specialists who are looking for new and innovative forms of critique and analysis. (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)

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)

Moses Isegawa's Abyssinian Chronicles sets out to rewrite history in that it corrects the distorted colonial vision by creating symbols for a new national identity—dealing with self-consciousness, loss of self-identity, and search for identity in coming to terms with the wreckage of war and independence. In Snakepit, Isegawa returns to his native Uganda haunted by greed and megalomania, a period when Idi Amin's dictatorship turned men in power into agents of deception, extortion, and murder. This article critically analyzes the “postcolonial“ (...) imagery in Snakepit as forms of resistance in the aftermath of colonialism and in the story “The Return of Shadow” in Viviane Sassen's collection of photographs Flamboya, and so challenge the way Western eyes have perceived the African continent. Snakepit and Flamboya thus both function as tools with which Africa's collective identity is redefined, the former coping with Uganda's post-European struggle for independence and fight against African corruption, the latter shedding light on the “darkness” Africa has been associated with by casting a post-European shadow on the image of Africa. (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 article draws on research at an eco/feminist peace camp set up to facilitate blockades against clear-cut logging in coastal temperate rainforest in Clayoquot Sound on Vancouver Island, British Columbia, in Canada in the early 1990s. The camp was said to be based on feminist principles and sometimes these were even articulated as eco/feminist principles. The slippage between these terms provides a focus for my discussion. Specifically the article explores the apparent paradox of the sheer vitality of this eco/feminist activism, (...) and in particular its insistence on international connections, in contrast to the widely circulating accounts of the end of feminism, and especially the end of global sisterhood, which emerged in the early 1990s. Thus this article is also necessarily about how recent histories of eco/feminism, including tensions between theory and activism, are narrated. I take as a departure point references to the work of Vandana Shiva and the Chipko movement which circulated in accounts of the camp, and explore ways in which eco/feminists might read such utterances as more than evidence of a naive and problematic universalism. I situate eco/feminism’s internationalism genealogically in feminism and eco/feminism and read this as a counter-narrative to the ending of global sisterhood. Through paying attention to various movements, back and forth, between Clayoquot and Chipko, Canada and India, and drawing on Anna Tsing’s notion of ‘friction’, I offer an account of what has been at stake in disavowals of the possibility of reading Chipko as eco/feminist, and suggest the importance of a more generous reading of eco/feminists’ attention to the Chipko movement. (shrink)

In 1879, Wilhelm Marr coined the term ‘Antisemitismus’, which aroused extensive discussion in academic circles. With the deepening of research, scholars’ research on anti-Semitism gradually traced back to the ancient world. Texts with anti-Semitic thought appeared as early as Ptolemaic Egypt. Essentially, the main purpose of these words were self-justification, a response to the sinful image of the Egyptians in the narrative of Exodus. The early Ptolemaic Egyptian writers got rid of the charges against the Egyptians by rewriting (...) the narrative of Exodus and shifting responsibility for the entire event to the Jews. It is obvious that in the process, the image of the Jewish people has been severely vilified. Although the writers did not express a strong anti-Semitic tendency subjectively, they all expressed a certain degree of anti-Semitic thought objectively. The anti-Semitic thought was inherited by later writers in the Roman world and had a profound impact. This article focuses on the works of three Ptolemaic Egyptian writers and discusses their reasons and influences for rewriting the narrative of the Exodus in combination with their historical background. Contribution: This article discusses the origin and spread of anti-Semitic thought in the ancient world. It has important reference value for the study of ancient writers’ understanding of the Old Testament. At the same time, it has important academic value for the study of Jewish history. (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 the paper we present completeness theorems for hybrid logics, discuss the problem of finite axiomatization and study term rewriting and unification for the variety of distributive lattices and the variety of groups of exponent 2.

SummaryThis essay aims to discuss the historiographical implications and premises of Peter Gordon's masterly book Continental Divide, in which he re-evaluates the Davos meeting between Ernst Cassirer and Martin Heidegger. This impressive reminder of the prospects of intellectual history deserves to be paid serious attention, particularly in European philosophy departments. Gordon's book exemplifies how problems of systematic philosophy can be clarified by a detour through history.I want to highlight three aspects of Gordon's book that fundamentally transform and deepen our understanding (...) of intellectual history in general and the Davos meeting in particular. First, I highlight one of the main merits of Gordon's study: his emphasis on the plurality behind the term ‘continental philosophy’. This opens up a whole new perspective on a seemingly well-known event within the history of twentieth-century philosophy. Second, I address Gordon's methodological premises, which challenge and fundamentally transform our understanding of intellectual history. Third, I attempt to summarise, from an intellectual history perspective, Gordon's argument about Cassirer's relevance. Here we are faced with the task of realigning and legitimising philosophy in a radically historicised world. To adumbrate the core of my comment I should say that I am thrilled by Gordon's book. I agree with nearly everything he says apart from his conclusions. In a closing remark I will try to explain the reasons for this surprising divergence. (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 (...) for the implicational fragment of ticket entailment. (shrink)

This paper draws together as many as possible of the clues and pieces of the puzzle surrounding T. S. Eliot’s “infamous” literary term “objective correlative”. Many different scholars have claimed many different sources for the term, in Pound, Whitman, Baudelaire, Washington Allston, Santayana, Husserl, Nietzsche, Newman, Walter Pater, Coleridge, Russell, Bradley, Bergson, Bosanquet, Schopenhauer and Arnold. This paper aims to rewrite this list by surveying those individuals who, in different ways, either offer the truest claim to being the (...) source of the term, or contributed the most to Eliot’s development of it: Allston, Husserl, Bradley and Bergson. What the paper will argue is that Eliot’s possible inspiration for the term is more indebted to the idealist tradition, and Bergson’s aesthetic development of it, than to the phenomenology of Husserl. (shrink)

The paper traces the development and the role of syntactic reduction in Edmund Husserl’s early writings on mathematics and logic, especially on arithmetic. The notion has its origin in Hermann Hankel’s principle of permanence that Husserl set out to clarify. In Husserl’s early texts the emphasis of the reductions was meant to guarantee the consistency of the extended algorithm. Around the turn of the century Husserl uses the same idea in his conception of definiteness of what he calls “mathematical manifolds.” (...) The paper argues that the notion anticipates the notion of reduction in term rewrite theory in computer science. The role of the reduction for Husserl is, however, primarily epistemological: its purpose is to impart clarity to formal mathematics. (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).

Unification was originally introduced in automated deduction and term rewriting, but has recently also found applications in other fields. In this article, we give a survey of the results on unification obtained in two closely related, yet different, application areas of unification: description logics and modal logics.

In Transparent Intensional Logic we can recognize two distinct notions of computation that loosely correspond to term rewriting and term interpretation as known from lambda calculus. Our goal will be to further explore these two notions and examine some of their properties.

This volume presents the proceedings of the workshop CSL '91 (Computer Science Logic) held at the University of Berne, Switzerland, October 7-11, 1991. This was the fifth in a series of annual workshops on computer sciencelogic (the first four are recorded in LNCS volumes 329, 385, 440, and 533). The volume contains 33 invited and selected papers on a variety of logical topics in computer science, including abstract datatypes, bounded theories, complexity results, cut elimination, denotational semantics, infinitary queries, Kleene algebra (...) with recursion, minimal proofs, normal forms in infinite-valued logic, ordinal processes, persistent Petri nets, plausibility logic, program synthesis systems, quantifier hierarchies, semantics of modularization, stable logic, term rewriting systems, termination of logic programs, transitive closure logic, variants of resolution, and many others. (shrink)

This paper starts from the observation that the standard arguments for compositionality are really arguments for the computability of semantics. Since computability does not entail compositionality, the question of what justifies compositionality recurs. The paper then elaborates on the idea of recursive semantics as corresponding to computable semantics. It is then shown by means of time complexity theory and with the use of term rewriting as systems of semantic computation, that syntactically unrestricted, noncompositional recursive semantics leads to computational (...) explosion (factorial complexity). Hence, with combinatorially unrestricted syntax, semantics with tractable time complexity is compositional. (shrink)

Building on previous work by Coquand and Spiwack [T. Coquand, A. Spiwack, A proof of strong normalisation using domain theory, in: Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, LICS’06, IEEE Computer Society Press, 2006, pp. 307–316] we construct a strict domain-theoretic model for the untyped λ-calculus with pattern matching and term rewriting which has the property that a term is strongly normalising if its value is not . There are no disjointness or (...) confluence conditions imposed on the rewrite rules, and under a mild but necessary condition completeness of the method is proven. As an application, we prove strong normalisation for barrecursion in higher types combined with polymorphism and non-deterministic choice. (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)

Inspired by Pohlers' local predicativity approach to Pure Proof Theory and Howard's ordinal analysis of bar recursion of type zero we present a short, technically smooth and constructive strong normalization proof for Gödel's system T of primitive recursive functionals of finite types by constructing an ε 0 -recursive function [] 0 : T → ω so that a reduces to b implies [a] $_0 > [b]_0$ . The construction of [] 0 is based on a careful analysis of the Howard-Schütte (...) treatment of Gödel's T and utilizes the collapsing function ψ: ε 0 → ω which has been developed by the author for a local predicativity style proof-theoretic analysis of PA. The construction of [] 0 is also crucially based on ideas developed in the 1995 paper "A proof of strongly uniform termination for Gödel's T by the method of local predicativity" by the author. The results on complexity bounds for the fragments of T which are obtained in this paper strengthen considerably the results of the 1995 paper. Indeed, for given n let T n be the subsystem of T in which the recursors have type level less than or equal to n+2. (By definition, case distinction functionals for every type are also contained in T n .) As a corollary of the main theorem of this paper we obtain (reobtain?) optimal bounds for the T n -derivation lengths in terms of ω n+2 -descent recursive functions. The derivation lengths of type one functionals from T n (hence also their computational complexities) are classified optimally in terms of $ -descent recursive functions. In particular we obtain (reobtain?) that the derivation lengths function of a type one functional a ∈ T 0 is primitive recursive, thus any type one functional a in T 0 defines a primitive recursive function. Similarly we also obtain (reobtain?) a full classification of T 1 in terms of multiple recursion. As proof-theoretic corollaries we reobtain the classification of the IΣ n+1 -provably recursive functions. Taking advantage from our finitistic and constructive treatment of the terms of Gödel's T we reobtain additionally (without employing continuous cut elimination techniques) that PRA + PRWO ( $\varepsilon_0) \vdash \Pi^0_2$ - Refl(PA) and PRA + PRWO ( $\omega_{n+2}) \vdash \Pi^0_2$ - Refl(I Σ n+1 ), hence PRA + PRWO( $\epsilon_0) \vdash$ Con(PA) and PRA + PRWO( $\omega_{n+2}) \vdash$ Con(IΣ n+1 ). For programmatic reasons we outline in the introduction a vision of how to apply a certain type of infinitary methods to questions of finitary mathematics and recursion theory. We also indicate some connections between ordinals, term rewriting, recursion theory and computational complexity. (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)