On implementation of tree synchronized languages

摘要

Tree languages have been extensively studied and have many applications related to the rewriting framework such as order sorted specifications,higher order matching or unification.In this paper,we focus on the implementatioon of such languages and,inspired by the Definite Clause Grammars that allows to write word grammars as Horn clauses in a Prolog environment,we propose to build a similar framework for particular tree languages (TTSG) which introduces a notion of synchronization between production rules.Our main idea is to define a proof theoretical semantics for grammars and thus to change from syntactical tree manipulations to logical deduction.This is achieved by a sequent calculus proof system which can be refined and translated into Prolog Horn clauses.This work provides a scheme to build goal directed procedures for the recognition fo tree languages.