Back to: Programme, CCC 2013 home

CCC 2013 - Abstracts

All abstracts as one pdf file (printouts of the abstracts will be handed out at Gregynog).

Vladislav Amstislavskiy (Novosibirsk)
On the structures of continuous and smooth functions

We study some new applications of the generalized method of interpretations. With this method offered by Kudinov O.V. we proved decidability of the theory of the lattice of continuous functions from R to R and from R^n to R for n>1.

Using this method we also proved that the theories of the structures of continuous functions over some perfectly normal space are m-equivalent to the theories of open subsets of this space. Thereby, by proving that the theory of the structure of open subsets of some perfectly normal space is decidable, decidability of the theory of the structure of continuous functions over this space is proved as well.

All these results are about the lattices of continuous functions. In our recent work we study the question of decidability of the theory of smooth functions. To use the generalized method of interpretations it is required to understand where we can interpret this theory satisfying all the formal conditions of the method.

Let us denote the structure of smooth functions as C and the algebraic structure of differences of open subsets of R with the inclusion operator, predicate of open sets and some additional partial operations as D.

Lemma. The theory of the structure D is decidable.

Since we can use the generalized method of interpretations to prove m-reducibility of the theory of C to the theory of D, the next statement is true.

Theorem. The theory of the smooth functions structure C is decidable.

The new applications of the generalized method of interpretations let consider it as a useful tool to prove decidability of theories.

Ulrich Berger (Swansea)
Opening: Continuity, Computability, Constructivity - From Logic to Algorithms

The talk will begin with an overview of the aims and scope of the COMPUTAL project and the workshop series CCC.

In the second part I will report about a recent approach to extend program extraction to Church's Simple Theory of Types.

Pieter Collins (Maastricht)
Computability and Dynamical Systems (tutorial)

Dynamical systems are ubiquitous as descriptions of natural phenomena, man-made technologies, living organisms and socioeconomic behaviour. The behaviour of most systems of scientific and technological interest is too complicated to be studied analytically, requiring the use of computational approaches.

The study of dynamical systems is a rich ground for the application of computability theory. In safety-critical situations, one needs guarentees that a system satisfies its specifications, and computability theory is required to determine how to specify systems and which properties can be verified. Properties of chaotic systems are subtle, and it is unclear whether common numerically-calculated descriptors of chaos, such as Lyapounov exponents or invariant measures, are computable, and what the relationship is between numerical results and system properties. Indeed, for some systems, notably hybrid systems and partial differential equations, it is not clear whether the evolution can be computed to arbitrarily accuracy over finite time intervals, and computability theory is required to provide a suitable semantics of evolution.

In this tutorial, I will give an overview of dynamical systems theory from the point of view of the computability of system properties. The following topics will be covered (time permitting):
- Introduction: Dynamical systems; evolution, properties and chaos
- Continuous-time systems: solution of differential equations
- Safety and verification: set-based analysis, reachability and chain reachability
- Hybrid systems: solution of algebraic equations, semantics and semicomputability
- Uncertain systems: differential inclusions and stochastic systems; probability theory and geometry
- Chaotic systems: symbolic dynamics, strange attractors. Chaos in the Lorentz equations
I will base the computability results on "computable type theory" based on Cartesian closed categories, which relates computability and continuity, and allows deep and meaningful results to be obtained from elementary abstract nonsense. I will also illustrate computability results with examples of efficient rigorous numerical methods for computing properties of interest with rigorous error bounds.

George Davie (University of South Africa)
Some uses of compressibility in probability and computable analysis

An infinite binary sequence $\omega $ is algorithmically random if there exists a natural number $d$ such that $K(\omega _{1:n})\geq n-d$ for each initial segment $\omega _{1:n}$ of $\omega ,$ where $K$ is prefix-complexity.

The compressibility coefficient $d$ allows one to prove (more) effective versions of many basic results in probability theory and computable analysis. We will discuss some recent applications to probability theory, Brownian motion and ergodic theory.

Willem Fouche (University of South Africa)
Fourier spectra of measures associated with algorithmically random Brownian motion

In this talk we discuss the behaviour at infinity of the Fourier transform of Radon measures supported by the images of fractal sets under an algorithmically random Brownian motion. We show that, under some computability conditions on these sets, the Fourier transform of the associated measures have, relative to the Hausdorff dimensions of these sets, optimal asymptotic decay at infinity.

Peter Hertling (Munich)
Semicontinuity of Clarke's Generalized Gradient

Clarke (1973, 1975, 1983) introduced a generalized gradient for Lipschitz continuous functions on Banach spaces and a notion of upper semicontinuity for set-valued functions. He showed that the function that maps a point to its generalized gradient is upper semicontinuous in this sense if the underlying Banach space is finite dimensional. This raises the question whether it must also be upper semicontinuous in this sense if the unterlying Banach space is infinite-dimensional; see Edalat (2008). We construct a counterexample.

Hajime Ishihara (JAIST, Kanazawa)
Classical propositional logic and decidability of variables in intuitionistic propositional logic (invited talk)

[pdf]

Akitoshi Kawamura (Tokyo)
On small complexity classes for computable analysis

Type-two Theory of Effectivity (TTE) gives a general framework for Computable Analysis. To refine it with computational complexity while keeping some generality, Kawamura and Cook recently proposed using machines that have random access to an oracle and run in second-order polynomial time/space in the "size" of the oracle. In this talk, we will go down further and study the analogues of classes NC and L. We will discuss some issues with the formulation that arise for these small complexity classes. (Based on joint work with Hiroyuki Ota.)

Takayuki Kihara (JAIST, Kanazawa)
A theorem on computable martingales

Many results from algorithmic randomness theory suggest that an infinite binary sequence is far from being random if and only if it has few derandomization power. In this talk, we add new evidence supporting this view.

A {\em dividend} is a function $\delta:2^{<\omega}\to[1,\infty)$. A {\em $\delta$-martingale} is a function $d:2^{<\omega}\to[0,\infty)$ with $d(\sigma)=d(\sigma 0)/\delta(\sigma 0)+d(\sigma 1)/\delta(\sigma 1)$. The value $d(\sigma)$ indicates a gambler's capital based on a dividend $\delta$ when the history of coin-tosses is $\sigma$. If $\delta$ is a constant function $2$, we simply say that $d$ is a martingale. At each time $n$, if a gambler bets all her/his money on $x(n)$, her/his capital $d(x\upharpoonright n)$ along $x$ would increase to $\prod_n\delta(x\upr n)$ dollars. A dividend $\delta$ is {\em legal} if $\prod_{n}\delta(x\upharpoonright n)$ diverges to infinity for any $x\in 2^\omega$. A $\delta$-martingale $d$ {\em frequently succeeds on $x$} if there exists a computable function $l:\omega\to\omega$ such that for every $n\in\omega$, $d(x\upharpoonright k)\geq n$ for some $k\in[l(n),l(n+1))$.

It is well-known that the probability of making much money as she/he wants is $0\%$. We may find out more about such events by seeing the internal structure of the $\sigma$-ideal of null subsets of Cantor space. Such $\sigma$-ideals have been deeply studied in modern set theory. Among them are the {\em strong measure zero} sets, the {\em meager-additive} sets, and the {\em null-additive} sets.

By borrowing a technique used in Pawlikowski's characterization of strong measure zero in set theory, we show the following equivalence for computable martingales:
(1) For every computable legal dividend $\delta$, a computable $\delta$-martingale frequently succeeds on $x$.
(2) For every infinite binary sequence $y\in 2^\omega$, a computable martingale frequently succeeds on $y$ if and only if an $x$-truth-table martingale frequently succeeds on $y$.
(3) For every infinite binary sequence $y\in 2^\omega$, a computable martingale frequently succeeds on $y$ if and only if a computable martingale frequently succeeds on $x+y$.
Here, for infinite binary sequences $x,y\in 2^\omega$, the bitwise-addition $x+y$ is defined by $(x+y)(n)\equiv x(n)+y(n)\mod 2$.
[pdf]

Margarita Korovina (Novosibirsk)
Computing Combinatorial Types of Multi-State Pfaffian Dynamics (invited talk)

In this talk I will present ongoing research which is aimed at creating a logical framework for formal verification of definable dynamical systems. The key idea of this framework is based on computing combinatorial types of trajectories of multi-state dynamical systems.
Consider a multi-state dynamics which is a finite family of dynamical systems and state conditi In this talk we propose algorithms for solving such problems for a wide class of multi-state Pfaffian dynamics, which have elementary (doubly-exponential) upper complexity bounds.
[pdf]

Oleg Kudinov (Novosibirsk)
Some analogue of the class of formally p-adic fields in any characteristic p>0

Considering fields of characteristic $p>0$ with distingueshed element $t$, we are interested whether such field $F$ does possess such a valuation $v$ that the element $v(t)$ is not p-divisible in the valuation group. This class of fields turns out to be $\forall$-axiomatizable and can be characterised in terms of nice operator $\Gamma_t(a) \, = \, (1-ta^p)^{-1}$. Moreover, the elementary theory of this class of fields (called formally $t$-pure), being considered in the language of fields with the only constant element $t$ and the predicate for the ring of valuation, has a model completion. The last theory coinsides with elementary theory of the class of formally $t$-pure fields $F$ without any proper algebraic extension that is formally $t$-pure again. In particular, the last theory is model complete. Similar results on model completeness usually were used to establish decidability results for corresponding theories. In considered case, it is not hard to deduce from above the decidability of elementary theories of some fields of kind $k\langle\langle \Gamma \rangle\rangle$ for some groups $\Gamma$. But the question related to decidability of the elementary theory of the field $F_p\langle\langle t \rangle\rangle$ is still open.

Andrew Lawrence, Monika Seisenberger and Ulrich Berger (Swansea)
Program Extraction in Action: A Verified Clause Learning SAT Solver

Modern SAT solvers typically include optimizations such as clause learning which are rarely treated with formal methods in practice. In this talk we show how to obtain such an optimized SAT solver together with a formal correctness proof by the method of program extraction from proofs: we have formalized a constructive proof of completeness for a modified DPLL proof system combined with unit resolution and extract a conflict driven clause learning SAT algorithm. This algorithm is capable of learning information during the search for a proof as well as performing non-chronological backtracking. This is a new case study in the area of program extraction and opens up many possibilities for future work. It also demonstrates how efficiency considerations can be taken into account at the proof level. The formalization and extraction has been carried out in the interactive proof assistant Minlog.

Norbert Müller (Trier)
Fast implementation of exact real number computation (tutorial)

The iRRAM is a software package written in C++ for the exact computation with real numbers in the sense of TTE (Type 2 Theory of Effectivity).

The tutorial will give an introduction to the use of this package, from installation via basic usage to more elaborate aspects like the implementation of real sequences, functions or even functors.

It addresses scientists with basic knowledge in recursive analysis and in imperative (and object oriented) programming.

Jean-Michel Muller (Lyon)
Proof of Properties in Floating-Point Arithmetic (invited talk)

Floating-point (FP) arithmetic was originally designed as a mere approximation to real arithmetic. And yet, since the behaviour of each operation is fully specified by the IEEE-754 standard for floating-point arithmetic, FP arithmetic can also be viewed as a mathematical structure on which it is possible to design algorithms and proofs. We give some examples that show the interest of that point of view.

Mitsuhito Ogawa and To Van Khanh (JAIST, Kanazawa)
A practical alternative to QE-CAD for solving polynomial constraints over real numbers

We have proposed raSAT loop, which refines over and under approximations to solve a bounded quantification of polynomial inequalities over real numbers. It holds soundness and (limited) completeness under certain conditions on an over-approximation theory.
We explore theoretical possibility in two directions, (1) completeness, and (2) polynomial equality handling, which make raSAT loop to be an alternative of QE-CAD (Quantifier Elimination by Cylindrical Algebraic Decomposition).
The current implementation status of SMT raSAT is also reported.

Arno Pauly (Cambridge)
Weihrauch degrees of unsolvability (tutorial)

Weihrauch reducibility was proposed by Brattka and Gherardi as a conceptual tool to compare the computational content of mathematical theorems. This yields a picture reminiscent of both reverse mathematics and Brouwerian counterexamples, yet offers a finer view (and some subtle differences). While quite a few have been classified with Weihrauch reducibility, there are also many open questions.

As a second fundamental aspect, the Weihrauch degrees exhibit a complex algebraic structure, which has many features of a substructural logic. There is a close interaction between the algebraic structure and both classification statements as well as techniques to prove separation results for Weihrauch degrees.

Besides presenting these two main parts of the theory of Weihrauch degrees, the tutorial will also discuss the precise choice of definitions (and rejected alternatives), as well as proof techniques applicable to Weihrauch reducibility.
[pdf]

Carsten Rösnick (Darmstadt)
Closed Sets and Operators thereon: Representations, Computability and Complexity

In this talk will see four (of many) seemingly different ways to encode closed/compact/convex/regular sets via infinite binary strings, how to feed them to an OTM, and how to compute with them set operators like union and intersection, point finding and projection, or even the image and the inverse of a given function. We will see how to measure the (second–order, parameterized) complexity of these operations (and operators), and whether (or not) these set encodings (representations) are (polytime) equivalent.
[pdf]

Matthias Schröder (Vienna)
The extensional hierarchy and the intensional hierarchy over the reals do not coincide (invited talk)

In functional programming, one considers two approaches to computability on the real numbers. The *extensional* approach assumes an idealistic functional language that contains the real numbers as a datatype. The *intensional* approach uses datatypes of ordinary functional languages and encodes real numbers as streams using the signed-digit representation.

Bauer, Escardo and Simpson showed that both concepts yield the same classes of Type-1 and Type-2 functionals over the reals. However, whether this is true for functionals of type $n \geq 3$ was an open problem for a long time. Bauer, Escardo and Simpson aslo discovered that there is a relationship to topological properties of the Kleene-Kreisel continuous functionals over the natural numbers $N$. Normann came up with a purely topological condition on the Kleene-Kreisel spaces that is equivalent to the Coincidence Problem.

In this talk, I will show that the Kleene-Kreisel space $(N->N)->N$ does not satisfy Normann's equivalence condition. By Normann's result, this proves that the extensional hierarchy and the intensional hierarchy do not agree from the level 3 on. I will also present an example of a Type-3 functional that is belongs to the extensional, but not to the intensional hierarchy.

Svetlana Selivanova and Victor Selivanov (Novosibirsk)
Computing Solution Operators of Boundary-value Problems for Some Linear Hyperbolic Systems of PDEs

We discuss possibilities of application of Numerical Analysis methods to proving computability, in the sense of the TTE approach, of solution operators of boundary-value problems for systems of PDEs. We prove computability of the solution operator for a symmetric hyperbolic system with computable real coefficients and dissipative boundary conditions, and of the Cauchy problem for the same system (in this case we also prove computable dependence on the coefficients) in a cube $Q\subseteq\mathbb R^m$. Such systems describe a wide variety of physical processes (e.g. elasticity, acoustics, Maxwell equations). Moreover, many boundary-value problems for the wave equation also can be reduced to this case, thus we partially answer a question by K. Weihrauch and N. Zhong. Compared with most of other existing methods of proving computability for PDEs, this method does not require existence of explicit solution formulas and is thus applicable to a broader class of (systems of) equations.
[pdf]

Anton Setzer (Swansea)
Coalgebraic Programming Using Copattern Matching

In many approaches for representing computational real numbers in theorem provers one arrives at a coalgebraic formulation. Essentially a computational number is a program which provides in response to user input arbitrarily good approximations of the real number in question. In order to prove properties and programming about these real numbers in a theorem prover based on Martin-Löf Type Theory (MLTT) such as Agda, we need therefore a theory of coalgebraic types. Originally MLTT had only dependent function types and inductive data types, and therefore there is a need to add coinductive types to MLTT, and a representation in theorem provers which is easy to use - ideally as easy as it is the case for inductive data types such as the natural numbers.

One approach to coalgebraic data types in functional programming. is using codata types, and that approach has been taken in both Agda and Coq. Elements of codata types are infinite objects which are evaluated lazily. Implicit in formulations of codata types is that codata types fulfil bisimulation equality, which is undecidable. In order to maintain decidable type checking, in the theorem provers Coq and Agda restrictions on the reduction of elements of codata types were imposed. The solutions resulted in a lack of subject reduction in the theorem prover Coq and a formulation of coalgebraic types in Agda, which is severely restricted.

In his PhD thesis [Ch11], Chi-Ming Chuang developed despite these short comings the signed digit and Cauchy real numbers based on the codata approach in Agda. He proved closure under rationals, addition, and multiplication, and executed the underlying provably correct programs. He showed as well that the resulting programs always produce, despite using postulated axioms, results in head normal form.

In order to avoid the problem of subject reduction we go back to the category theoretical approach where final coalgebras are the dual of initial algebras. Whereas the elements of inductive data types are determined by their introduction rules, and the elimination rules are the natural inverse of these introduction rules, the elements of coinductive data types are determined by their elimination rules, and the introduction rules are the natural inverse.

In theorem provers such as Agda the elimination rules for algebras are represented by defining functions using termination checked pattern matching. In our joint POPL'13 article [APTS13] we introduce its dual, defining elements of coalgebras by copattern matching, which, if termination checked, represents the introduction rules for coalgebras. We presented a simply typed recursive calculus which includes both nested pattern and copattern matching, including mixing of the two. The resulting theory fulfils subject reduction.

In this talk we will show how to replace, following the approach in [Ch11], nested pattern and copattern matching to simultaneous non-nested (co)pattern matching and then to full (co)recursion operators. Some cases, which should be those which pass a termination checker, can then be reduced to primitive (co)recursion operators. If only primitive (co)recursion operators are used we obtain by [Me87, Ge92] a calculus which is strongly normalising.

Finally we investigate how to define types such as colists, which are quite conveniently represented as codata types in the coalgebraic approach in such a way that they are easy to use.

References:

[APTS13] Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer: Copatterns: programming infinite structures by observations. In: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '13, pages 27-38, 2013.

[Ch11] Chi~Ming Chuang. Extraction of Programs for Exact Real Number Computation using Agda. PhD thesis, Dept. of Computer Science, Swansea University, Swansea SA2 8PP, UK, March 2011. Available from http://www.swan.ac.uk/~csetzer/articlesFromOthers/index.html.

[Ge92] Herman Geuvers: Inductive and coinductive types with iteration and recursion. In B. Nordström, K. Petersson, and G. Plotkin (Eds.): Informal proceedings of the 1992 workshop on Types for Proofs and Programs, Bastad 1992, Sweden, pages 183 - 207, 1992.

[Me87] N. P. Mendler: Inductive types and type constraints in second-order lambda calculus. In: Proceedings of the Second Symposium of Logic in Computer Science. Ithaca, N.Y., pages 30 - 36. IEEE, 1987.

Stanislav Speranski (Novosibirsk)
Quantified probability logics: expressibility vs. computability

The present talk is devoted to various aspects of so-called quantified probability logics, focusing on issues of expressibility and computability.
[pdf]

Dieter Spreen (Siegen)
The COMPUTAL Project

The talk will explain the EU IRSES programme and give an overview of the COMPUTAL project including its aims, financial regulations, work packages and management structure.

Florian Steinberg (Darmstadt)
Computable analytic functions in iRRAM

[pdf]

Yasuyuki Tsukamoto and Hideki Tsuiki (Kyoto)
A Hausdorff space with a strongly independent dyadic subbase

We construct a Hausdorff space with a strongly independent dyadic subbase. A dyadic subbase of a topological space induces a domain representation. If the space is regular Hausdorff and the dyadic subbase is proper, then the space is represented as a subset of the minimal limit set of the domain. The example which we will construct is Hausdorff but non-regular, and the domain induced by the dyadic subbase has no minimal limit element.

Back to: Programme, CCC 2013 home
Last modified: Thu June 20 2013