Calm, Panic and Collapse! Word languages can be safe after all.
Christopher Broadbent
- 15:00 January 2009 ( week First, Hilary Term 2009 )Common Room (103)
Higher-order recursion schemes are systems of rewrite rules that can be used to generate
objects such as infinite trees and word-languages. One motivation for studying them is that
certain verification problems on higher-order programs can be translated to deciding
properties of such objects. Some recursion schemes satisfy a syntactic constraint known as
`safety'. These are in some ways nicer to work with and decision procedures for certain
classes of property were known for the structures generated by safe schemes before algorithms
had been discovered for the general case.
Furthermore, the trees and word-languages generated by safe schemes are precisely those
generated by higher-order pushdown automata (PDA), which are machines with a stack that itself
contains stacks of stacks... of stacks. The known automata-theoretic characterisation of
general recursion schemes requires more sophisticated machines known as `collapsible pushdown
automata' (CPDA), which again can be more complicated to work with.
It is interesting to ask about the extent to which this additional complication is necessary.
Are there really any objects that can only be generated by an unsafe recursion scheme?
Equivalently, to what extent are CPDA more expressive than PDA?
In this talk we will begin by introducing PDA and CPDA in order to define the
automata-theoretic version of this question. We will then informally give an intuitive idea of
how one can obtain a partial answer for word-languages. A word-language generated by an n-CPDA
can always be generated by an (n+1)-PDA. This builds on an idea used by Aehlig, Ong and
Miranda to show that 2-PDA and 2-CPDA generate precisely the same word-languages.
objects such as infinite trees and word-languages. One motivation for studying them is that
certain verification problems on higher-order programs can be translated to deciding
properties of such objects. Some recursion schemes satisfy a syntactic constraint known as
`safety'. These are in some ways nicer to work with and decision procedures for certain
classes of property were known for the structures generated by safe schemes before algorithms
had been discovered for the general case.
Furthermore, the trees and word-languages generated by safe schemes are precisely those
generated by higher-order pushdown automata (PDA), which are machines with a stack that itself
contains stacks of stacks... of stacks. The known automata-theoretic characterisation of
general recursion schemes requires more sophisticated machines known as `collapsible pushdown
automata' (CPDA), which again can be more complicated to work with.
It is interesting to ask about the extent to which this additional complication is necessary.
Are there really any objects that can only be generated by an unsafe recursion scheme?
Equivalently, to what extent are CPDA more expressive than PDA?
In this talk we will begin by introducing PDA and CPDA in order to define the
automata-theoretic version of this question. We will then informally give an intuitive idea of
how one can obtain a partial answer for word-languages. A word-language generated by an n-CPDA
can always be generated by an (n+1)-PDA. This builds on an idea used by Aehlig, Ong and
Miranda to show that 2-PDA and 2-CPDA generate precisely the same word-languages.