On Word and Frontier Languages of Unsafe Higher-Order Grammars

TL;DR

This paper establishes a correspondence between unsafe higher-order word languages and frontier languages of unsafe higher-order tree languages, extending known results from safe to unsafe languages using intersection types.

Contribution

It proves that unsafe order-(n+1) word languages are equivalent to frontier languages of unsafe order-n tree languages, filling a gap in higher-order grammar theory.

Findings

Established the equivalence for unsafe languages, previously known only for safe languages.

Used intersection types to transform higher-order grammars between word and tree forms.

Derived several known results on higher-order grammars as corollaries.

Abstract

Higher-order grammars are extensions of regular and context-free grammars, where non-terminals may take parameters. They have been extensively studied in 1980's, and restudied recently in the context of model checking and program verification. We show that the class of unsafe order-(n+1) word languages coincides with the class of frontier languages of unsafe order-n tree languages. We use intersection types for transforming an order-(n+1) word grammar to a corresponding order-n tree grammar. The result has been proved for safe languages by Damm in 1982, but it has been open for unsafe languages, to our knowledge. Various known results on higher-order grammars can be obtained as almost immediate corollaries of our result.