Complex-Antecedent Constraint Compilation

[User's Manual]
[Code] Unlike ALE that uses only type constraints (i.e., only types are allowed as the antecedent of constraints), TRALE employs complex antecedent constraints. These constraints allows arbitrary function-free and inequation-free antecedents. For a detailed discussion of these constraints, refer to the User's Guide.

Compilation of complex antecedent constraints is done by compile_complex_assert/0 in three steps as follows:

1. Separate all existential quantifiers from the antecedent. Recall that TRALE interprets the scope of existentially quantified variables in complex antecedent constraints loosely. This step is necessary to identify such variables.
2. Find a trigger for the antecedent (defined below).
3. Replace the constraint with one that has the trigger found in the previous step as the antecedent.

The predicate that is responsible for separating existential quantifiers from the antecedent of a constraint is find_narrow_vars/3. For example, consider the following call to find_narrow_vars/3.

find_narrow_vars(A^B^C(A;(B,C)),Antec,Vars)

This will unify Antec with A;(B,C), and Vars with [C,B,A].

The next step is to find a trigger for the complex antecedent. The trigger is the most specific type whose most general satisfier subsumes the most general satisfier of the antecedent. The predicate find_trigger_type/3 is responsible for finding the trigger. There are five possibilities, as follows:

• $trigger(\tau)=\tau$ where $\tau\in Type$
• $trigger(x)=\bot$ where $x$ is a variable
• $trigger(F)=intro(F)$ where $F\in Feat$ and $intro(F)$ is the introducer of $F$
• $trigger(\phi_1\wedge\phi_2)=trigger(\phi_1)\sqcup trigger(\phi_2)$
• $trigger(\phi_1\vee\phi_2)=trigger(\phi_1)\sqcap trigger(\phi_2)$

The final step is to assert a kind of type-antecedent constraint for the trigger. The difference between this and a regular type-antecedent constraint is that in the former, the constraint only applies to a subset of objects of the specified type: those that match the description given in the original complex-antecedent.

Let us suppose there is a predicate, whenfs(X=Desc,Goal), which delays Goal until X was subsumed by the most general satisfier of description Desc. Thus all principles $\alpha \Longrightarrow (\gamma \wedge \rho)$ could be converted into:

$$trigger(\alpha) \Longrightarrow x\ \wedge\ \mathtt{whenfs}((x=\alpha), ((x=\gamma) \wedge \rho))$$

This typically involves compiling unifications of feature structures into unifications of their term encodings plus a type check to see whether one or more constraint consequents need to be enforced.

Figure 7.1: Part of the signature underlying the FMP constraint

For example, if we formulate the Finiteness Marking Principle (FMP) for German as the following complex-antecedent constraint (assuming the type signature depicted in Figure 7.1):

synsem:loc:cat:(head:verb,marking:fin)
     *> synsem:loc:cat:head:vform:bse

then we can observe that the antecedent is a feature value description (F:$\phi$), so the trigger is intro(SYNSEM), the unique introducer of the SYNSEM feature, which happens to be the type sign. We can then transform this constraint, as follows:

sign cons X goal whenfs((X=synsem:loc:cat:(head:verb,
                                           marking:fin)),
                        (X=synsem:loc:cat:head:vform:bse)).

The effect of the hypothetical whenfs/3 predicate is achieved by ALE's coroutining predicate, when_type/3 (see Chapter 6), and farg/3. Given when_type(Type,FS,Goal), ALE delays Goal until FS is of type Type. farg(F,X,FVal) binds FVal to the argument position of term encoding X that corresponds to the feature F once X has been instantiated to a type for which F is appropriate.

The corresponding type-antecedent constraint generated for our example is thus as follows:

sign cons X 
     goal (farg(synsem,X,SynVal),farg(loc,SynVal,LocVal),
           farg(cat,LocVal,CatVal),farg(head,CatVal,HdVal),
           when_type(verb,HdVal,(farg(marking,CatVal,MkVal),
           when_type(fin,MkVal,
                     (X=synsem:loc:cat:head:vform:bse))))).

The above constraint now waits until the value of the HEAD feature of SYNSEMLOCCAT in a sign is verb and the value of its MARKING feature is fin before it enforces the constraint, which is unifying X with synsem:loc:cat:head:vform:bse.