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.

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

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.

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.

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]

Consider a multi-state dynamics which is a finite family of dynamical systems and state conditi

[pdf]

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.

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.

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]

[pdf]

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.

[pdf]

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.

[pdf]

Back to: Programme, CCC 2013 home

Last modified: Thu June 20 2013