Evènement pour le groupe Graphes et Logique

Date 2013-06-04  11:00-12:00
TitreBöhm trees as higher-order recursion schemes 
RésuméHigher-order recursive schemes (HORS) are schematic representations of functional programs. They generate possibly infinite ranked labelled trees and, viewed as tree generators, are equivalent to λY-terms of ground type in which free variables can only have types of the form o → ... → o (with o as a special case). In this talk, I will show that any λY-term (with no restrictions on term type or the types of free variables) has an equivalent presentation as a HORS. That is, for any λY-term, there exists a HORS generating a tree that faithfully represents the Böhm tree of the λY-term. In particular, the HORS encodes higher-order binding information contained in the Böhm tree. The result reduces the problem of Böhm tree equivalence for the λY-calculus to the equivalence problem for HORS and enables MSO model-checking of Böhm trees. We also show how to adapt the methodology to finitary PCF (over finite datatypes). This is joint work with Andrzej Murawski. 
LieuSalle 076 
OrateurPierre Clairambault 
UrlUniversity of Cambridge 

Aucun document lié à cet événement.

Retour à l'index