User:LajujKej

From Wikipedia, the free encyclopedia

In phrase structure grammars, such as generalised phrase structure grammar, head-driven phrase structure grammar and lexical functional grammar, a feature structure is essentially a set of attribute-value pairs. For example the attribute named number might have the value singular. The value of an attribute may be either atomic, e.g. the symbol singular, or complex (most commonly a feature structure, but also a list or a set).

A feature structure can be represented as a directed acyclic graph (DAG), with the nodes corresponding to the variable values and the paths to the variable names. Operations defined on feature structures, e.g. unification, are used extensively in phrase structure grammars. In most theories (e.g. HPSG), operations are strictly speaking defined over equations describing feature structures and not over feature structures themselves, though feature structures are usually used in informal exposition.

Often, feature structures are written like this:

\begin{bmatrix} \mbox{category} & noun\ phrase\\ \mbox{agreement} & \begin{bmatrix} \mbox{number} & singular \\ \mbox{person} & third \end{bmatrix} \end{bmatrix}

Here we have the two features category and agreement. Category has the value noun phrase whereas the value of agreement is indicated by another feature structure with the features number and person being singular and third.

This particular notation is called attribute value matrix (AVM)

The matrix has two columns. One for the feature names and the other for the values. In this sense a feature structure is a list of key-value pairs. The value might be atomic or another feature structure. This leads to another notation for feature structures - the use of trees. In fact some systems use S-expression to represent feature structures.


Contents

[edit] Connections to Modal Logic

We know that feature structures can be represented as directed acyclic graphs. Blackburn (2003) makes the crucial insight that these directed acyclic graphs are Krikpe frames and unification implies modal satisfaction.


[edit] From the Feature Language F to the Modal Model M

Let F=\langle L, A \rangle be a language where A is a set of A-indexed propositional letters, i.e., atomic values. L is an L-indexed set of modal operators, i.e., attributes. A feature structure of signature L, A is a triple \langle N, \{R_{l}\}_{l \in L}, \{Q_{a}\}_{a \in A} \rangle where:

  1. N is a non-empty set of nodes.
  2. \{R_{l}\}_{l \in L} is a binary partial function on N for all l \in L. Notice that N, \{R_{l} \}_{l \in L} is an L-indexed multiframe. Call it L.
  3. \{Q_{a}\}_{a \in A} is a unary relation on N for all a \in A. Notice that \{Q_{a}\}_{a \in A} is an interpretation of propositional letters.

With a frame and a valuation we have a modal model. Let M = \langle N, \{R_{l}\}_{l \in L}, \{Q_a\}_{a \in A} \rangle be any arbitrary feature structure.


[edit] Syntax

Using some truth-functionally adequate collection of Boolean connectives, parentheses and the members of \langle L, A \rangle, build wffs of F as follows:

  1. All propositional variables are wffs.
  2. If φ,ψ are wffs, then (\neg \phi ) and (\phi \land \psi) are wffs.
  3. If f is a modality and φ is a wff, then (\langle f \rangle \phi) is a wff.
  4. Nothing is a wff unless constructed in accordance with 1-3.

We can define \vee ,\to ,\leftrightarrow. Let f[\phi] = \neg f \langle \neg \phi \rangle for all l \in L.


[edit] An Example of a wff

\langle category \rangle p_{noun\ phrase} \land \langle agreement \rangle ( \langle number \rangle p_{singular} \land \langle person \rangle p_{third} )

This formula is precisely the AVM given above. Notice that conjunction encodes stacking.


[edit] Semantics

Remember that M is an arbitrary feature structure with any frame F = \langle N, \{R_l\}_{l \in L} \rangle and any valuation \{Q_{a}\}_{a \in A} . For all n \in N:

M, n \vDash p_{a} iff n \in Q_{a} for all a \in A.
M, n \vDash \neg \phi iff M,n \nvDash \phi
M, n \vDash (\phi \vee \psi) iff M,n \vDash \phi or M,n \vDash \psi
M, n \vDash \langle f \rangle \phi iff there is some n' Rf-related to n and M,n \vDash \phi for all f \in L

[edit] Unification and Satisfiability

We know that unification is the combination of the information in two feature structures, yielding a new feature structure. This new feature structure must be a wff, so we can capture unification in the modal language with the principle:

Two wffs φ and ψ are unifiable iff their conjunction is satisfiable.

The following proofs about satisfiability are therefore also proofs about feature unification.


[edit] Soundness and Completeness

The model logic defined by AVMs is sound and strongly complete with respect to the class of all functional frames. The completeness result can be extended to all point generated and acyclic feature structures.


[edit] KAV , the Minimal Axiomatization of M

The minimal axiomatization of M contains all propositional logic tautologies, the K-axiom \langle f \rangle (\phi \to \psi) \to (\langle f \rangle \phi \to \langle f \rangle \psi) and \langle f \rangle \phi \to [f]\psi. The rules of proof are modus ponens and necessitation. Call this axiom schema KAV.


[edit] Soundness of KAV

Show \Sigma \vdash_{AV} \phi \Rightarrow \Sigma \vDash_{AV} \phi. Proof by induction on the complexity of derivations.

Base case of complexity m = 1, i.e., the sentence letters. There are three cases:

  1. φ is an tautology of modal logic. We know that any tautology of modal logic can be obtained from a tautology of propositional logic by uniformly substituting modal formulas for propositional symbols, so \vDash_{AV} \phi.
  2. φ is an instance of the K axiom. \Sigma \vDash \phi because for all modal structures M and all worlds w \in W^{M}, M, w \vDash \Box(\chi \to \psi) \to (\Box \chi \to \Box \psi).
  3. Suppose φ is an instance of \langle f \rangle \phi \to [f]\psi. We will show that φ is true in all frames generated from \{R_{l}\}_{l \in L}, which by definition is a partial funcion. Suppose M,n \vDash \langle f \rangle \psi for some n \in N and f \in L, i.e., there is some n \in N such that nRfn' and M, n \vDash \psi. Now suppose for contradiction that there is some n'' \in N such that nRfn'' and M, n \vDash \psi. But then nRfn' and nRfn'' and n \neq n'', which contradicts the claim that \{R_{l}\}_{l \in L} is a function. Assuming that \neg [f]\psi produces a contraction, so \langle f \rangle \psi \to [f]\psi is valid on all frames generated from \{R_{l}\}_{l \in L}.

Induction Hypothesis: Assume for all derivations of complexity < m that \Sigma \vdash_{AV} \phi \to \Sigma \vDash_{AV} \phi. We can construct a derivation of complexity m by:

  1. Adding an axiom (in which case the proof is exactly the same as in the base case).
  2. Modus ponens (in which case the proof is exactly the same as for propositional logic).
  3. φ follows from necessitation, i.e., φ = [f]ψ for arbitrary f \in L. By the definition of necessitation, ψ is a theorem, i.e., \vdash_{AV} \psi. Since we are constructing a derivation of length m, it must be the case that the derivation of ψ from the empty set is of complexity < m, thus \vDash_{AV} \psi by the induction hypothesis. But if \vDash_{AV} \psi, then for all n \in N^{M}, M, n \vDash_{AV} \psi, so for all nodes n \in N that are Rf-related to n, M, n \vDash_{AV} \psi, so \vDash_{AV} [f]\psi.

The induction is complete.


[edit] Strong Completeness of KAV

Show \Sigma \vDash_{AV} \phi \Rightarrow \Sigma \vdash_{AV} \phi. We will use the Henkin method.

Let M_{{can}_{AV}} be the canonical model on the Henkin multiframe of signature \langle L,A \rangle. M_{{can}_{AV}} is a triple \langle N^{{can}_{AV}}, \{R^{{can}_{AV}}_{l}\}_{l \in L}, \{Q^{{can}_{AV}}_{a}\}_{a \in A} \rangle where:

N^{{can}_{AV}} is the set of all maximal KAV consistent sets.
\{R^{{can}_{AV}}_l\}_{l \in L} is the binary relation on N^{{can}_{AV}} defined by nR^{{can}_{AV}}_{f}n' iff for all f \in L and for all φ, [f]\phi \in n implies \phi \in n'. Call \{R^{{can}_{AV}}_l\}_{l\in L} the canonical relation.
n \in \{Q_a\}_{a \in A}(p_{a}) iff p_{a} \in n for all a \in A and n \in N^{{can}_{AV}}. Call \{Q_{a}\}_{a \in A} the canonical or natural valuation.

Henkin Lemma: \Sigma \Vdash_{AV} \phi \Rightarrow \Sigma \vdash_{AV} \phi. Proof by induction on the complexity of formulae.

Base Case (i.e., formula of complexity n = 1): Immediate from the definition of the canonical valuation.

Induction Hypothesis: Assume for all formula of complexity < n that \Sigma \Vdash_{AV} \phi \Rightarrow \Sigma \vdash_{AV} \phi. We now show for all formula of complexity n. There are two cases.

  1. The Boolean cases follows by the definition of maximal consistent set.
  2. φ is of the form [f]ψ for some f \in L. Suppose [f]\psi \in n for some n \in N^{{can}_{AV}}. We need to show that M_{{can}_{AV}}, n \Vdash [f]\psi, which means that for all n' \in N^{{can}_{AV}} that are R^{{can}_{AV}}_{f}-related to n, M_{{can}_{AV}}, n' \Vdash \psi. Hence \psi \in n' by the induction hypothesis. Suppose for contradiction there is a n' \in N^{{can}_{AV}} such that nR^{{can}_{AV}}_{f}n' and \psi \notin n'. Hence \neg \psi \in n'. By the definition of the canonical relation it must be the case that \psi \in n'. But this is a contradiction because \psi \in n' and \neg \psi \in n'.
  3. Suppose [f]\psi \notin n for all f \in L and n \in N^{{can}_{AV}}. We will show that M_{{can}_{AV}}, n \nVdash [f]\psi. To do this we must construct a n' \in N^{{can}_{AV}}, such that nR^{{can}_{AV}}_{f}n' and \psi \notin n'. That is, \langle f \rangle \neg \psi \in n. \langle f \rangle \neg \psi \in n means that \bigwedge n \land \langle f \rangle \neg \psi is consistent. We just have to extend \neg \psi to a maximal consistent set, which we know is possible by Lindenbaum's lemma.

The induction is complete.


[edit] Extending the Completeness of KAV

Because of the axiom \langle f \rangle \phi \rightarrow [f]\phi, we already know that the completeness result holds with respect to the class of functional frames, but KAV is also complete with respect to the class of point generated and acyclic feature structures. KAV completeness can also be extended with the addition of other common axioms for doing computational linguistics.


[edit] Completeness and Point Generated Feature Structures

Extend a set Γ to a maximal KAV consistent set Γ + . The submodel M_{\Gamma^{+}} generated by Γ + is a feature structure and is by definition point generated. Because modal truth transfers to generated submodels, M_{\Gamma^{+}} satisfies Γ + .


[edit] Completeness and Other Axioms
  1. The axiom p_{a} \rightarrow \neg p_{b} eliminates constant-constant clashes. When we add it to the Henkin model, it makes KAV complete with respect to the class of all features structure frames such that no node is labeled with two distinct pieces of atomic information.
  2. The axiom p_{a} \rightarrow \neg \langle f \rangle \top assures that atomic information is only inserted at terminal nodes. When we add it to the Henkin model, it makes KAV complete with respect to the class of all features structures frames such that only terminal nodes are labeled with atomic information.
  3. The axiom \langle F \rangle (\nu \land \phi) \land \langle G \rangle (\nu \land \psi) \rightarrow \langle F \rangle (\nu \land \phi \land \psi), where \langle F \rangle, \langle G \rangle are metavariables over sequences of modalities and ν is a metavariable over atomic variables, assures that each piece of atomic information is associated with a unique node. When we add this axiom to the Henkin model, it makes KAV complete with respect to the class of all feature structure frames such that each node is labelled with unique atomic information. In the canonical model, it means that each piece of atomic information can occur in at most one maximal KAV consistent set.


[edit] KAV, the Finite Model Property, and Decidability

KAV has the finite model property, which will also assure its decidability. It follows from Post's Theorem that every recursively axiomatized modal logic with the finite model property is decidable. Suppose for any formula φ that φ is satisfied in a model M_{K_{AV}} at an arbitrary node n. Build a finite model M'_{K_{AV}} out of M_{K_{AV}} that also satisfies φ at n as follows:

  1. Let the natural number k be the maximum depth of nested modalities in φ.
  2. Let Lφ be the subset of L that contains the indices of the modalities that occur in φ.
  3. Let M'_{K_{AV}} be the structure generated from n, but only with relations l \in L^{\phi} and only generated in k steps.

Notice that M'_{K_{AV}} must be finite. We now show that M'_{K_{AV}} satisfies φ at n. By definition, M'_{K_{AV}} is a generated submodel of M_{K_{AV}}. Therefore M'_{K_{AV}}, n \Vdash \phi because modal truth holds across generated submodels.


[edit] Conclusions

The fact that the feature structure formalisms used by many linguists are essentially modal logics has far reaching consequences. Not only does it allow for feature structures to be tied to other modal and first order logics, but it permits proofs about unification and the computational properties of feature structures. The connection also provides a means to see the implications of supplementing feature structure formalisms with new theoretical machinery. The addition of boxlabels, for example, requires a different modal structure, namely hybrid logic.

 This linguistics article is a stub. You can help Wikipedia by expanding it.
Retrieved from "http://en.wikipedia.org../../../l/a/j/User%7ELajujKej_5c55.html"
In other languages