Infinity Symposium

From The Infinity Project

A past event: the spring symposium for our BRICKS project INFINITY.

INFINITY SYMPOSIUM
Tuesday March 21 and Wednesday March 22, 2006
Room S111, Faculty of Sciences, Vrije Universiteit Amsterdam

The project is concerned with infinite objects, computation, modeling, and reasoning (more information can be found here). For participants of the INFINITY project, the symposium is meant as an opportunity to learn about related work and meet people working in related fields. Most talks will be of a tutorial nature. The symposium takes place in between two PhD defenses (see Past events) that both have to do with the subject of INFINITY.

Contents

[edit]

Programme

[edit]

Tuesday March 21, 2006

[edit]

Wednesday March 22, 2006

[edit]

Abstracts

  • Johan van Benthem (University of Amsterdam and Stanford University): Modal Lindström Theorems.
    Modal languages are natural process formalisms, but the question what makes them tick at a suitably abstract level can be, and has been, answered in many different ways. In this talk, we explore a new road via abstract model theory, presenting some new Lindström theorems for basic modal logic and the guarded fragment, while exploring connections with the modal invariance and interpolation theorems. Reference: cf. the recent ILLC Research Report.
  • Stefan Blom (University of Innsbruck): Lifting Böhm trees from terms to term graphs.
    To give semantics to a term graph rewrite system, we can use a generalization of the Böhm tree called Böhm semantics. Proving that a particular Böhm semantics is good is relatively easy if the rewrite system is confluent. Unfortunately, many graph rewrite systems are not. Hence, we present a theory that allows us to derive Böhm semantics for a term graph rewrite system from a term rewrite system. Then, in order to show that the Böhm semantics of a graph rewrite system is good, it suffices to show that the Böhm semantics of the corresponding term rewrite system is good.
  • Mariangiola Dezani (University of Torino): Infinite reductions are insensible to λ-term identity or difference (joint work with Makoto Tatsuta).
    We analyse the computational behaviour of λ-term applications. We are interested to know when there exists a non-terminating reduction and when all reductions are non-terminating.
    For an arbitrary λ-term M we can prove that there is one strongly normalising λ-term X such that there is one non-terminating reduction out of M X ... X (n times X) if and only if there are n strongly normalising λ-terms X1,...,Xn such that there is one non-terminating reduction out of M X1 ... Xn. The analogous property holds when replacing “there is one reduction” by “all reductions” and “strongly normalising” by “weakly normalising”.
    The proof for weak normalisation uses a detailed analysis on how variables are replaced inside λ-terms in normal form. For strong normalisation we consider Klop’s extended λ-calculus (for which it is shown that weak normalisation is equivalent to strong normalisation) and we generalise to this calculus the analysis of variable replacements.
    As an application of the result on strong normalisation we show that the λ-terms whose interpretation is the top element (in the environment which associates the top element to all variables) of the Honsell-Lenisa model are exactly the λ-terms which applied to an arbitrary number of strongly normalising λ-terms produce always strongly normalising λ-terms. This proof uses a finitary logical description of the model by means of intersection types. Therefore we solve an open question stated by Dezani, Honsell and Motohama.
  • Silvio Ghilardi (Università degli Studi di Milano): Bisimulation quantifiers: from Kripke semantics to model-theoretic, categorical and algebraic applications.
    We first introduce bisimulation quantifiers from the point of view of their semantic characterization, sketching also recent computer science oriented applications. We then mention the few interesting logics where bisimulation quantifiers are definable/eliminable and point out the algebraic conditions over the category of finitely presented algebras which are equivalent to this eliminability. From another point of view, we show how definability of bisimulation quantifiers is related to classical model-theoretic topics such as model completeness and (standard, first order) quantifier elimination.
  • Jan Willem Klop (Vrije Universiteit Amsterdam, Radboud Universiteit Nijmegen and CWI): Infinitary normalization and productivity.
    In finitary rewriting the properties of weak and strong normalization (WN and SN) are well-known. In computer science, SN is often referred to as 'termination' for short, and many methods have been developed to prove termination. When we move to the infinitary setting, where terms may be infinite and reduction sequences may have ordinal length, termination in the old sense is no longer a main issue. But infinitary normalization is, and we define this notion in both the weak and strong version, called WN∞ and SN∞. Somewhat surprisingly, as global properties of Term Rewriting Systems (TRSs), these notions coincide, in marked difference with the finitary notions WN and SN, where SN is strictly stronger.
    After this introductory part, which is about joint work with Roel de Vrijer, see report, we discuss a notion stronger than SN∞ known as productivity.
    As a guiding example we discuss infinite computations of 'tree ordinals', a way to squeeze real ordinals in the framework of infinitary rewriting, using fundamental sequences.
  • Alexander Kurz (University of Leicester): Concrete dualities of algebras and coalgebras.
    Algebras and coalgebras are dual notions by definition. This abstract duality is often not very informative because coalgebras over Set are dual to algebras over the dual of Set. In this talk, we are interested in concrete dualities between algebras and coalgebras, that is, we have in addition to the abstract duality that both algebras and coalgebras are set-based. This situation is important as it establishes a tight connection between the inductive world of algebras and the coinductive world of coalgebras. Indeed, from the abstract point of view these two worlds coincide whereas from the concrete point of view the algebraic world provides a logical description that completely captures the coalgebraic world.
  • Lawrence Moss (Indiana University): Recursion and circularity.
    "The (Infinity) project is concerned with infinite objects, computation, modeling, and reasoning" and I would like to address these points with a study of circularity and recursion. Mine will be a survey-like talk, and it has several themes. My starting point is coalgebra, since here one has a convenient presentation of various infinite objects. But one still needs to have tools for reasoning, and here I apply logics of recursion in the form of Moschovakis' FLR_0. In addition, I'll present a sequent-style system for reasoning about circularly defined sets (joint work with Glen Whitney). Finally, I'll turn to related areas concerning computation. I'll sketch a coalgebraic treatment of uninterpreted and especially interpreted recursive program schemes (joint work with Stefan Milius).
  • Grigore Rosu (University of Illinois at Urbana-Champaign): Hidden logics: theory, circular coinduction, applications and tools.
    Hidden logics is a smooth extension of algebraic specifications based on a split of sorts into visible and hidden, and on interpreting equality as behavioral instead of strict. The visible part of a hidden, or behavioral, theory can be specified using the entire arsenal of algebraic specification, while the hidden, or behavioral or observational part, is specified in terms of indistiguishability under experiments. Coinduction is a proof principle for behavioral equivalence in hidden logics which works independently of the existence of a final model but which, unfortunately requires human intervention to pick an appropriate "bisimulation" equivalence. Circular coinduction is an automation of coinduction, aiming at finding an equivalence relation automatically by speculating the typical circular behavior of behavioral theories. There are several interesting and non-trivial examples, such as regular expressions enriched with complement, for which circular coinduction is not only a decision procedure, but in fact gives the best known algorithm to test equivalence of languages. A tool supporting behavioral specification and circular coinduction is currently being developed on top of a fast rewrite engine with meta-level programming capabilities (Maude). In this talk we will present the theoretical foundations of hidden logics, discuss circular coinduction and its implementation in our current tool, and will show many examples of finite and infinite structures that can be shown behavioral equivalent automatically.
  • Jakob Grue Simonsen (University of Copenhagen): Modularity in infinitary rewriting.
    We study properties of infinitary term rewriting systems that are retained when combining systems with rules from two or more disjoint alphabets. In ordinary finitary rewriting, a number of interesting properties -- notably the Church-Rosser property -- are known to be retained under such combinations, thus enabling proofs of desirable properties to be broken down into proofs involving subsystems, and -- colloquially -- allowing "safe" program code to freely call "safe" program code from other program modules.
    In this talk, we sketch why almost none of the standard properties related to confluence and normalization are retained when passing to infinitary rewriting and discuss suitable limitations that enable us to recover some of the positive results from finitary rewriting.
[edit]

Participation and registration

Participation is free.

If you wish to join the organized lunch, please register by sending an email to Elly Lammers, before Thursday March 16, at 12.00. The contribution for the lunch is 10 euro per person per lunch, to be paid in cash. Please note that it is also possible to have lunch in the canteen of the university.

If you wish to join the dinner on Tuesday March 21, please register by sending an email to Elly Lammers, before Thursday March 16, at 12.00. (The price of the dinner will be announced later.)

[edit]

How to get at the Vrije Universiteit

The symposium is in room S111, Faculty of Sciences, Vrije Universiteit Amsterdam. Please see [1] for a route description. Room S111 is best reached via entrance De Boelelaan 1081 (number 4 on the map).

[edit]

Organization

If you have questions please do not hesitate to contact one of the organizers:

Retrieved from "http://fspc282.few.vu.nl/infinity/index.php/Infinity_Symposium"