Category Archives: Service

Seminars in JAIST

JAIST Logic Seminar Series

The lectures below is held as a part of JSPS Core-to-Core Program, A. Advanced Research Networks, and EU FP7 Marie Curie Actions IRSES project CORCON.
(http://www.jaist.ac.jp/logic/ja/core2core, https://corcon.net/)

On Tuesday 6 September, 2016, 13:30-17:00, JAIST, Lecture room I2

Josef Berger (Ludwig-Maximilians-Universität München), The fan theorem and convexity (joint work with Gregor Svindland)

The fan theorem is the following statement: (FAN) Let B be a decidable set of finite binary sequences. Assume that every infinite binary sequence has an initial part that belongs to B. Then there exist an N such that  every infinite binary sequence has an initial part of length smaller than N that belongs to B.

This axiom plays an important role in Intuitionism, a philosophy of mathematics that was introduced by the Dutch mathematician L.E.J. Brouwer. We work in constructive mathematics in the tradition of Errett Bishop. Here, the fan theorem is neither provable nor falsifiable. Many theorems of analysis are equivalent to the fan theorem. One example for such a theorem is: (POS) Every positive-valued uniformly continuous function on the unit interval has positive infimum.

In our paper Convexity and constructive infamy we have shown that, under the additional condition of convexity of the function, POS is constructively valid.

In this talk, we discuss to which extent this gives rise to a notion of  convex bars and a corresponding constructively valid convex fan theorem.

Anton Setzer and Bashar Igried (Swansea University) Coinductive Reasoning in Dependent Type Theory – Copatterns, Objects, Processes (part on Processes joint work with Bashar Igried)

When working in logic in computer science, one is very often confronted with bisimulation. The reason for its importance is that in computer science, one often reasons about interactive or concurrent programs. Such programs can have infinite execution paths, and therefore correspond to coinductive data types. The natural equality on coinductive data types is bisimulation. Proofs of bisimulation form one of the main principles for reasoning about coinductive data types.

However, bisimulation is often very difficult to understand and to teach. This is in contrast to the principle of induction, where there exists a well established tradition of carrying out proofs by induction. One goal of this talk is to demonstrate that one can reason about coinductive data types in a similar way as one can reason inductively about inductive data types.

Reasoning about inductive data types can be done by pattern matching. For instance for reasoning about natural numbers one makes a case distinction on whether the argument is 0 or a successor. For coinductive data types the dual is copattern matching, which is essentially a case distinction on the observations one can make for a coinductively defined set. For instance, streams have observations head and tail, and one can introduce a stream by determining its head and its tail.

We then look at examples of the use of coinductive data types. One is the notion of an object, as it occurs in object-oriented program. Objects are defined by their method calls, which are observations, so they are defined coinductively. The final example will be the representation of processes in dependent type theory, where we will refer to the process algebra CSP.

Seminars in JAIST

The JAIST Logic Seminar series will host the following seminars in August 2016.

The seminars below are held as a part of JSPS Core-to-Core Program, A. Advanced Research Networks, and EU FP7 Marie Curie Actions IRSES project CORCON.

  • Tuesday 2 August, 2016, 13:30-15:10
    Eugenio Moggi (University of Genova)
    Categories of Classes for Collection Types
    Collection types have been proposed by Buneman and others (in the ’90) as a way to capture database query languages in a typed setting. In 1998 Manes introduced the notion of collection monad on the category S of sets as a suitable semantics for collection types. The canonical example of collection monad is the finite powerset monad Pf. In order to account for the algorithmic aspects of database languages, the category S is unsuitable, and should be replaced with other categories, whose arrows are maps computable by “low complexity” algorithms. We propose “realizability for DSL” (Domain Specific Languages), where the starting point is a monoid C of endomaps on a set D, instead of a combinatory algebra on D, as a way to get such categories by constructions like the category A[C] of “assemblies”. To get Pf in a systematic way we borrow ideas from AST (Algebraic Set Theory, started by Joyal and Moerdijk in the ’90), where they fix a notion of “small” map in a category of “classes”, and read “small” as “finite”.
  • Thursday 4 August, 2016, 13:30-15:10
    Eugenio Moggi (University of Genova)
    Hybrid System Trajectories as Partial Continuous Maps
    Hybrid systems (HS) are dynamic systems that exhibit both continuous and discrete dynamic behavior: they can flow (according to a differential equation) and jump (according to a transition relation). HS can be used for modeling rigid body dynamics with impacts, and more generally Cyber-Physical Systems. HS can exhibit Zeno behaviors, that arise naturally in rigid body dynamics with impacts, but are absent from purely discrete or purely continuous systems. Dealing properly with these behaviors is a prerequisite to give sound definitions of concepts such as reachability. We propose the use of partial continuous maps (PCM) as trajectories that describe how a HS evolves over time. PCMs enable a notion of trajectory that can go beyond Zeno points.
  • Friday 5 August, 2016, 10:50-12:30
    Eugenio Moggi (University of Genova)
    Models, Over-approximations and Robustness
    Hybrid systems, and related formalisms, have been successfully  used to model Cyber-Physical Systems. The usual definition of “reachability”, in terms of the reflexive and transitive closure of a transition relation, is unsound for Zeno systems. We propose “safe reachability”, which gives an over-approximation of the set of states that are “reachable in finite time” from a set of initial states. Moreover, mathematical models are always a simplification of the system they are meant to describe, and one must be aware of this mismatch, when using these models for system analyses. In safety analysis it is acceptable to use over-approximations of the system behavior, indeed they are the bread and butter of counterexample guided abstraction refinement (CEGAR). We propose a notion of safe (time-bounded) reachability, which is also robust wrt arbitrary small overapproximations, and argue that it is particularly appropriate for safety analysis.
  • Monday 8 August, 2016, 13:30-15:10, JAIST, Collaboration room 7 (I-56)
    Marco Benini (University of Insubria)
    Variations on the Higman’s Lemma
    The Higman’s Lemma says that if A is a well-quasi-order, so is the set of finite sequences over A with the order induced by embedding. By considering the structure of the categories of well-founded quasi-orders and well-quasi-orders, another proof of the Lemma will be derived, along with a number of variants, which may be of some interest.
  • Thursday 25 August, 2016, 13:30-15:10
    Helmut Schwichtenberg (Ludwig-Maximilians-Universität München)
    Invariance axioms for realizability
    Kolmogorov (1932) proposed to consider mathematical formulas as problems asking for solutions. Following this idea it seems reasonable to extend arithmetical theories by adding invariance axioms, which state that every formula is equivalent to the (internal) formula stating that it has a realizer. We sketch such a theory, which in addition allows to fine-tune the computational content of proofs by decorations of the logical connectives. A soundness theorem holds.