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 
Emailpierre.clairambault@cl.cam.ac.uk 
UrlUniversity of Cambridge 



Aucun document lié à cet événement.

Retour
Retour à l'index