Author name cluster

Ulrich Schöpp

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.

6 papers

2 author rows

I&C Journal 2016 Journal Article

Computation by interaction for space-bounded functional programming

Ugo Dal Lago
Ulrich Schöpp

When programming with sublinear space constraints one often needs to use special implementation techniques even for simple tasks, such as function composition. In this paper, we study how such implementation techniques can be supported in a functional programming language. Our approach is based on modelling computation by interaction using the Int construction of Joyal, Street & Verity. We apply this construction to a term model of a first-order programming language and use the resulting structure to derive the functional programming language intml. Intml can be understood as a programming language simplification of Stratified Bounded Affine Logic. We formulate intml by means of a type system inspired by Baillot & Terui's Dual Light Affine Logic. We show that it captures the complexity classes flogspace and nflogspace. We illustrate its expressiveness by showing how typical graph algorithms, such a test for acyclicity in undirected graphs, can be represented.

Details DOI

LPAR Conference 2008 Conference Paper

A Formalised Lower Bound on Undirected Graph Reachability

Ulrich Schöpp

Abstract We study the expressivity of Jumping Automata on Graphs ( jag s), an idealised model of computation with logarithmic space. jag s operate on graphs by using finite control and a constant number of pebbles. In this paper we revisit the proof of Cook & Rackoff that jag s cannot decide s - t -reachability in undirected graphs. Cook & Rackoff prove this result by constructing, for any given jag, a finite graph that cannot be traversed exhaustively by the jag. We generalise this result from the graphs constructed by Cook & Rackoff to a general class of group action graphs. We establish a bound on the number of nodes that a jag can visit on such action graphs. This generalisation allows us to strengthen the result of Cook & Rackoff to the existence of a graph of small degree whose diameter (rather than its number of nodes) is larger than the number of nodes the jag can visit. The main result has been formalised in the theorem prover Coq, using Gonthier’s tactic language SSReflect.

Details

CSL Conference 2008 Conference Paper

Pure Pointer Programs with Iteration

Martin Hofmann 0001
Ulrich Schöpp

Abstract Many logspace algorithms are naturally described as programs that operate on a structured input (e. g. a graph), that store in memory only a constant number of pointers (e. g. to graph nodes) and that do not use pointer arithmetic. Such “pure pointer algorithms” thus are a useful abstraction for studying the nature of logspace -computation. In this paper we introduce a formal class purple of pure pointer programs and study them on locally ordered graphs. Existing classes of pointer algorithms, such as Jumping Automata on Graphs ( jag s) or Deterministic Transitive Closure ( dtc ) logic, often exclude simple programs. purple subsumes these classes and allows for a natural representation of many graph algorithms that access the input graph by a constant number of pure pointers. It does so by providing a primitive for iterating an algorithm over all nodes of the input graph in an unspecified order. Since pointers are given as an abstract data type rather than as binary digits we expect that logarithmic-size worktapes cannot be encoded using pointers as is done, e. g. in totally-ordered dtc logic. We show that this is indeed the case by proving that the property “the number of nodes is a power of two, ” which is in logspace, is not representable in purple.

Details

LFMTP Workshop 2006 Conference Paper

Modelling Generic Judgements

Ulrich Schöpp

We propose a semantics for the ∇-quantifier of Miller and Tiu. First we consider the case for classical first-order logic. In this case, the interpretation is close to standard Tarski-semantics and completeness can be shown using a standard argument. Then we put our semantics into a broader context by giving a general interpretation of ∇ in categories with binding structure. Since categories with binding structure also encompass nominal logic, we thus show that both ∇-logic and nominal logic can be modelled using the same definition of binding. As a special case of the general semantics in categories with binding structure, we recover Gabbay & Cheney's translation of FO λ ∇ into nominal logic.

Details

CSL Conference 2006 Conference Paper

Space-Efficient Computation by Interaction

Ulrich Schöpp

Abstract We introduce a typed functional programming language for logarithmic space. Its type system is an annotated subsystem of Hofmann’s polytime LFPL. To guide the design of the programming language and to enable the proof of logspace -soundness, we introduce a realisability model over a variant of the Geometry of Interaction. This realisability model, which takes inspiration from Møller-Neergaard and Mairson’s work on BC \(^{\rm --}_{\epsilon}\), provides a general framework for modelling space-restricted computation.

Details

CSL Conference 2004 Conference Paper

A Dependent Type Theory with Names and Binding

Ulrich Schöpp
Ian Stark

Abstract We consider the problem of providing formal support for working with abstract syntax involving variable binders. Gabbay and Pitts have shown in their work on Fraenkel-Mostowski (FM) set theory how to address this through first-class names: in this paper we present a dependent type theory for programming and reasoning with such names. Our development is based on a categorical axiomatisation of names, with freshness as its central notion. An associated adjunction captures constructions known from FM theory: the freshness quantifier И, name-binding, and unique choice of fresh names. The Schanuel topos — the category underlying FM set theory — is an instance of this axiomatisation. Working from the categorical structure, we define a dependent type theory which it models. This uses bunches to integrate the monoidal structure corresponding to freshness, from which we define novel multiplicative dependent products ∏ * and sums ∑ *, as well as a propositions-as-types generalisation H of the freshness quantifier.

Details