Tree-Adjoining Grammars as Abstract Categorial Grammars
Tree-Adjoining Grammars as Abstract Categorial Grammars
复制标题
作为抽象范畴语法的树邻接语法
DOI：
--
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
P. D. Groote
中科院分区：
文献类型：
--
作者：
P. D. Groote
范畴语法并不打算作为另一种语法形式主义，与其他已建立的形式主义竞争。它更应该被看作是一个语法框架的核心--本着（Ranta，2002）的精神--其他现有的语法模型可能被编码在这个框架中。本文通过展示树邻接文法（Joshi和Schabes，1997）如何嵌入抽象范畴文法来说明这一事实。这种嵌入体现了ACG框架的几个特征：·ACG操作的基本对象是λ项，这一事实允许定义更高阶的操作。典型地，树附加是这样的高阶操作（Abrusci，Fouquere和Vauzeilles，1999; Joshi和Kulick，1997; Monnich，1997）。·框架的灵活性允许在两个阶段中定义嵌入。第一ACG允许生成给定TAG的树语言。该第一ACG的抽象语言对应于TAG的派生树。然后，第二ACG允许提取相应的字符串语言。该第二ACG的抽象语言对应于第一ACG的对象语言。2.抽象范畴语法本节定义了抽象范畴语法的概念。我们首先介绍了线性蕴涵类型、高阶线性签名、建立在高阶线性签名上的线性λ-项和词典的概念。设A是一组原子类型。建立在A上的线性蕴涵类型的集合T（A）归纳定义如下：1.如果a ∈ A，则a ∈ T（A）; 2.若α，β ∈ T（A），则（α− <$β）∈ T（A）.高阶线性签名由三重矩阵组成，其中：A是原子类型的有限集合; c © 2002 Philippe de Groote。第六届国际树邻接语法和相关框架研讨会（TAG+6）的会议记录。101-106.威尼斯大学。102 TAG+6会议记录2。C是一个有限的常数集; 3.τ：C → T（A）是一个函数，它赋予C中的每个常数一个T（A）中的线性蕴涵类型。设X是λ-变量的无限可数集。建立在高阶线性签名上的线性λ项的集合Λ（λ）= λ A，C，τ λ被归纳定义如下：1.若c ∈ C，则c ∈ Λ（λ）; 2.如果x ∈ X，则x ∈ Λ（λ）; 3.若x ∈ X，t ∈ Λ（λ），且x在t中自由出现一次，则（λx. t）∈ Λ（λ）; 4.若t，u ∈ Λ（ε），且t和u的自由变量集不相交，则（tu）∈ Λ（ε）.Λ（λ）具有避免替换的捕获、α-转换和β-归约的通常概念（Barendregt，1984）。给定一个高阶线性特征码λ = λ A，C，τ λ，Λ（λ）中的每个线性λ-项可以在T（A）中被分配一个线性蕴涵类型。这种类型分配服从一个推理系统，其判断是以下形式的序列：Γ − t：α其中：1。Γ是一个有限的λ-变量类型声明集，其形式为'x：β'（其中x ∈ X且β ∈ T（A）），使得任何λ-变量最多被声明一次; 2. t ∈ Λ（λ）; 3.α ∈ T（A）.公理和推理规则如下：
categorial grammars are not intended as yet another grammatical formalism that would compete with other established formalisms. It should rather be seen as the kernel of a grammatical framework — in the spirit of (Ranta, 2002) — in which other existing grammatical models may be encoded. This paper illustrates this fact by showing how tree-adjoining grammars (Joshi and Schabes, 1997) may be embedded in abstract categorial grammars. This embedding exemplifies several features of the ACG framework: • The fact that the basic objects manipulated by an ACG are λ-terms allows higher-order operations to be defined. Typically, tree-adjunction is such a higher-order operation (Abrusci, Fouquere and Vauzeilles, 1999; Joshi and Kulick, 1997; Monnich, 1997). • The flexibility of the framework allows the embedding to be defined in two stages. A first ACG allows the tree langage of a given TAG to be generated. The abstract language of this first ACG corresponds to the derivation trees of the TAG. Then, a second ACG allows the corresponding string language to be extracted. The abstract language of this second ACG corresponds to the object language of the first one. 2. Abstract Categorial Grammars This section defines our notion of an abstract categorial grammar. We first introduce the notions of linear implicative types, higher-order linear signature, linear λ-terms built upon a higher-order linear signature, and lexicon. Let A be a set of atomic types. The set T (A) of linear implicative types built upon A is inductively defined as follows: 1. if a ∈ A, then a ∈ T (A); 2. if α, β ∈ T (A), then (α−◦ β) ∈ T (A). A higher-order linear signature consists of a triple Σ = 〈A,C, τ〉, where: 1. A is a finite set of atomic types; c © 2002 Philippe de Groote. Proceedings of the Sixth International Workshop on Tree Adjoining Grammar and Related Frameworks (TAG+6), pp. 101–106. Universita di Venezia. 102 Proceedings of TAG+6 2. C is a finite set of constants; 3. τ : C → T (A) is a function that assigns to each constant in C a linear implicative type in T (A). Let X be a infinite countable set of λ-variables. The set Λ(Σ) of linear λ-terms built upon a higher-order linear signature Σ = 〈A,C, τ〉 is inductively defined as follows: 1. if c ∈ C, then c ∈ Λ(Σ); 2. if x ∈ X , then x ∈ Λ(Σ); 3. if x ∈ X , t ∈ Λ(Σ), and x occurs free in t exactly once, then (λx. t) ∈ Λ(Σ); 4. if t, u ∈ Λ(Σ), and the sets of free variables of t and u are disjoint, then (t u) ∈ Λ(Σ). Λ(Σ) is provided with the usual notion of capture avoiding substitution, α-conversion, and β-reduction (Barendregt, 1984). Given a higher-order linear signature Σ = 〈A,C, τ〉, each linear λ-term in Λ(Σ) may be assigned a linear implicative type in T (A). This type assignment obeys an inference system whose judgements are sequents of the following form: Γ −Σ t : α where: 1. Γ is a finite set of λ-variable typing declarations of the form ‘x : β’ (with x ∈ X and β ∈ T (A)), such that any λ-variable is declared at most once; 2. t ∈ Λ(Σ); 3. α ∈ T (A). The axioms and inference rules are the following: