Author name cluster

Klaus Aehlig

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

5 papers

2 author rows

CSL Conference 2007 Conference Paper

Propositional Logic for Circuit Classes

Klaus Aehlig
Arnold Beckmann

Abstract By introducing a parallel extension rule that is aware of independence of the introduced extension variables, a calculus for quantified propositional logic is obtained where heights of derivations correspond to heights of appropriate circuits. Adding an uninterpreted predicate on bit-strings (analog to an oracle in relativised complexity classes) this statement can be made precise in the sense that the height of the most shallow proof that a circuit can be evaluated is, up to an additive constant, the height of that circuit. The main tool for showing lower bounds on proof heights is a variant of an iteration principle studied by Takeuti. This reformulation might be of independent interest, as it allows for polynomial size formulae in the relativised language that require proofs of exponential height.

Details

CSL Conference 2007 Conference Paper

Relativizing Small Complexity Classes and Their Theories

Klaus Aehlig
Stephen A. Cook
Phuong Nguyen 0001

Abstract Existing definitions of the relativizations of NC 1, L and NL do not preserve the inclusions NC 1 ⊆ L, NL ⊆ AC 1. We start by giving the first definitions that preserve them. Here for L and NL we define their relativizations using Wilson’s stack oracle model, but limit the height of the stack to a constant (instead of log( n )). We show that the collapse of any two classes in { AC 0 ( m ), TC 0, NC 1, L, NL } implies the collapse of their relativizations. Next we develop theories that characterize the relativizations of subclasses of P by modifying theories previously defined by the second two authors. A function is provably total in a theory iff it is in the corresponding relativized class. Finally we exhibit an oracle α that makes AC k ( α ) a proper hierarchy. This strengthens and clarifies the separations of the relativized theories in [Takeuti, 1995]. The idea is that a circuit whose nested depth of oracle gates is bounded by k cannot compute correctly the ( k + 1) compositions of every oracle function.

Details

CSL Conference 2006 Conference Paper

A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata

Klaus Aehlig

Abstract Model checking properties are often described by means of finite automata. Any particular such automaton divides the set of infinite trees into finitely many classes, according to which state has an infinite run. Building the full type hierarchy upon this interpretation of the base type gives a finite semantics for simply-typed lambda-trees. A calculus based on this semantics is proven sound and complete. In particular, for regular infinite lambda-trees it is decidable whether a given automaton has a run or not. As regular lambda-trees are precisely recursion schemes, this decidability result holds for arbitrary recursion schemes of arbitrary level, without any syntactical restriction. This partially solves an open problem of Knapik, Niwinski and Urzyczyn.

Details

TCS Journal 2004 Journal Article

An arithmetic for non-size-increasing polynomial-time computation

Klaus Aehlig
Ulrich Berger
Martin Hofmann
Helmut Schwichtenberg

An arithmetical system is presented with the property that from every proof a realizing term can be extracted that is definable in a certain affine linear typed variant of Gödel's T and therefore defines a non-size-increasing polynomial time computable function.

Details DOI

CSL Conference 2002 Conference Paper

On Continuous Normalization

Klaus Aehlig
Felix Joachimski

Abstract This work aims at explaining the syntactical properties of continuous normalization, as introduced in proof theory by Mints, and further studied by Ruckert, Buchholz and Schwichtenberg. In an extension of the untyped coinductive λ-calculus by void construcors (so-called repetition rules), a primitive recursive normalization function is defined. Compared with other formulations of continuous normalization, this definition is much simpler and therefore suitable for analysis in a coalgebraic setting. It is shown to be continuous w. r. t. the natural topology on non-wellfounded terms with the identity as modulus of continuity. The number of repetition rules is locally related to the number of β-reductions necessary to reach the normal form (as represented by the Böhm tree) and the number of applications appearing in this normal form.

Details