Logic and Computation in Finitely Presentable Infinite Structures
Prof Valentin Goranko, University of the Witwatersrand, Johannesburg
Thursday 30 November 2006, 14h00, M 111 (Seminar Room)
Infinite structures abound not only in mathematics, but also in the modelling of computer systems and software: infinite or unbounded data-structures, infinite state transition systems (pushdown configuration graphs, counter systems, Petri nets, parameterized network systems), models of computation with unbounded memory (stacks, queues, FIFO channels), etc.
In order to deal effectively with an infinite structure, and in particular to solve algorithmic and computational problems in it, one needs a suitable finitary presentation of that structure, which enables algorithmic computation of queries and verification of properties specified in a suitable formal logical language. Typical such logical languages are first- and second- order logic, as well as a variety of modal and temporal logics used in program verification.
In this talk I will survey some of the most useful and well-studied types of finitary presentations, and the associated classes of infinite structures with good computational behaviour, such as automatic structures (with decidable first-order theories), the Caucal/pushdown hierarchy of infinite graphs with decidable monadic second-order theory (pushdown, prefix-recognizable, and further up), and rational structures. I will discuss automata-based presentations and computational decision procedures, as well as logical characterizations and properties of these structures.
At the end, I will discuss briefly my current and intended research in the area, some open problems, and research directions.
The talk will assume some (basic) background on first-order and second-order logic, and automata on finite and infinite words and trees.
Seminar Series on Abstract Stone Duality (ASD)
Dr Paul Taylor, University of Manchester, UK
Thursdays 5-19 October 2006, 14h00, M 111 (Seminar Room)
Topics
- 5 October, A Curious Equation in Topology and Higher Order Logic
- 12 October, Interval Analysis Without Intervals
- 19 October, ASD beyond local compactness
Webpage: http://www.cs.man.ac.uk/~pt/ASD
Effective Borel Degrees of Some Topological Functions
Guido Gherardi, University of Siena, Italy,
Thursday 8 June 2006, 14h00, M 111 (Seminar Room)
The topic of my seminar talk is the incomputability of some topological functions (with respect to certain representations) using the tools of the Borel computability theory. First, we analyze some basic topological functions on closed subsets of Euclidean space, like closure, border, intersection, and derivative, and we prove for such functions completeness results in the effective Borel hierarchy. Then, we re-consider two well-known topological results: the lemmas of Urysohn and Urysohn-Tietze for generic metric spaces (for the latter we refer to the proof given by Dieudonné). Both lemmas define Borel-computable functions of degree 2 which in some cases are even complete.
Plottable Real Number Functions and the Computable Graph Theorem
Prof Vasco Brattka, University of Cape Town,
Friday 21 April 2006, 16h00, Great Westerford Building, Newlands
The Graph Theorem of classical recursion theory states that a total function on the natural numbers is computable, if and only if its graph is recursive. It is known that this result can be generalized to real number functions where it has an important practical interpretation: the total computable real number functions are precisely those which can be effectively plotted with any given resolution. We generalize the Graph Theorem to appropriate partial real number functions and even further to functions defined on certain computable metric spaces. Besides the non-uniform version of the Graph Theorem which logically relates computability properties of the function and computability properties of its graph, we also discuss the uniform version: given a program of a function, can we algorithmically derive a description of its graph? And, vice versa, given a description of the graph, can we derive a program of the function? While the passage from functions to graphs always is computable, the inverse direction from graphs to functions is problematic and it turns out that the answers to the uniform and the non-uniform questions do not coincide. We prove that in both cases certain topological and computational properties (such as compactness or effective local connectedness) are sufficient for a positive answer and we provide counterexamples which show that the corresponding properties are not superfluous. Additionally, we briefly discuss the special situation of the linear case.
This seminar will be a videoseminar in cooperation with the Computability and Complexity in Analysis and Dynamics Seminar of the Department of Computer Science, University of Toronto, and the Fields Institute for Research in Mathematical Sciences, Canada.
Bisimulations and Pictures of Sets: A survey of hyperset theories, their key modeling tools, and applications to computer science
Prof Stephen Harnish, Visiting Researcher and Bluffton University, Ohio, USA,
Wednesday 5 April 2006, 15h30, M 111 (Seminar Room)
ZFC provides a standard, robust foundation for modeling mathematics and its applications. Yet, some systems studied by computer scientists are most naturally modeled by self-referential sets with cyclic- and other infinite- element chains that are prohibited by ZFC’s axiom of foundation. In recent decades the properties and applications of various non-well-founded (NWF) set theories have been developed by logicians such as Aczel, Scott, Finsler, Barwise and Moss. I will review the properties of these sets, explain one key modeling tool (the solution lemma), and describe several areas of application for computer science, situation theory, and linguistics.
On Effectivity and Continuity of Multifunctions
Prof Dieter Spreen, University of Siegen, Germany,
Friday 24 March 2006, 15h00, M 111 (Seminar Room)