Aim:
- Map GF abstract syntax to logical statements
- every (abstract) sentence is mapped to a logical proposition
- Reason about such propositions, in some way
(Based on work presented this year at IWCS)
- GF syntaxes generally follow Montague’s homomorphism principle: syntax is a prelude to semantics. (that is, syntax is not there only to give a language model — a set of strings. It serves to reveal the structure which underlies the semantics)
- Both a programming language and a logical framework
- The type system is a superset of GF’s
- Higher order logic (very expressive logic, so “anything you can think of” can be expressed)
- Has good reasoning facilities (“tactics”) (some can solve decidable subtheories)
- Can work on “open terms” (some definitions can remain abstract)
- The mapping is done using the programming bits of Coq
- The reasoning is done with the HOL bits of Coq
- Not a decidable logic (cannot evaluate the truth value)
- Not a theorem prover (cannot in general prove true conjectures)
- From a pedagogical point of view, maybe it could be better to clearly separate the programming bits and the reasoning bits.
- The programming bits are restricted to total programs (which can sometimes mean extra work)
- Not the same support for overloading as GF
- Other type-theoretical proof assistants: Agda, Idris, …
- Separate semantics and inference
- Program in your favorite language with higher-order functions (a type-system helps). In particular, you can use the concrete syntax mechanism of GF for the simplest semantic mappings. (You may have difficulties with quantifiers; supporting anaphora is most certainly very difficult.)
- Use your favorite reasoning tool (HOL, SAT solvers, SMT, etc.)
In GF:
- the abstract syntax is a type assignment (symbols are mapped to types)
- the concrete syntax is a program assignment (symbols are mapped to definitions) (aka. linearization)
- GF checks that the definitions in question are correct (type-wise)
Semantics are just another concrete syntax (mapping symbols to definitions).
| Surface syntax | Abstract syntax | Semantics |
|---|---|---|
| LinCat | Cat | Type |
| function | constructor | function |
| String | Cl | Prop |
| … | NP | object |
| … | VP | object → Prop |
| λnp vp. np ++ vp | mkCl : NP → VP → Cl | fun np vp => vp np. |
Example:
- ⟦gives a ball to the boy⟧ : object → Prop
- ⟦John⟧ : object
- mkCl ⟦John⟧ ⟦gives a ball to the boy⟧ : Prop = ⟦gives a ball to the boy⟧ ⟦John⟧
Clause categories can be mapped to other things than propositions:
- Commands (programs)
- Database queries/updates
- …
In such a case “reasoning” does not take the usual mathematical form of proving/testing conjectures
→ not coq
- Get them from the GF shell (“ai” –abstract info– can be used for this purpose)
- Get them from the file (probably the easiest)
abstract Grammar = {
flags startcat = S ;
cat
S ; Cl ; NP ; VP ; AP ; CN ; PN ;
Det ; N ; A ; V ; V2 ; AdA ;
Pol ;
Conj ;
data
UseCl : Pol -> Cl -> S ;
PredVP : NP -> VP -> Cl ;
ComplV2 : V2 -> NP -> VP ;
DetCN : Det -> CN -> NP ;
ModCN : AP -> CN -> CN ;
CompAP : AP -> VP ;
AdAP : AdA -> AP -> AP ;
ConjS : Conj -> S -> S -> S ;
ConjNP : Conj -> NP -> NP -> NP ;
UseV : V -> VP ;
UsePN : PN -> NP ;
UseN : N -> CN ;
UseA : A -> AP ;
some_Det, every_Det : Det ;
i_NP, you_NP : NP ;
very_AdA : AdA ;
Pos, Neg : Pol ;
and_Conj, or_Conj : Conj ;
}
abstract Test = Grammar ** {
fun
man_N, woman_N, house_N, tree_N : N ;
big_A, small_A, green_A : A ;
walk_V, arrive_V : V ;
love_V2, please_V2 : V2 ;
john_PN, mary_PN : PN;
} ;- Every category must have a definition (of type Type).
- Every (data) constructor must have a definition (whose type is the same as its GF type). Some ()
When we do not know what definition to use, we can abstract over it instead. In Coq this is conveniently done using the “Parameter” command.
Parameter S : Type.
Parameter Cl : Type.
Parameter VP : Type.
Parameter PN : Type.
Parameter NP : Type.
Parameter AP : Type.
Parameter A : Type.
Parameter CN : Type.
Parameter Det : Type.
Parameter N : Type.
Parameter V : Type.
Parameter V2 : Type.
Parameter AdA : Type.
Parameter Pol : Type.
Parameter Conj : Type.
Parameter UseCl : Pol -> Cl -> S.
Parameter PredVP : NP -> VP -> Cl.
Parameter ComplV2 : V2 -> NP -> VP.
Parameter DetCN : Det -> CN -> NP.
Parameter ModCN : AP -> CN -> CN.
Parameter CompAP : AP -> VP.
Parameter AdAP : AdA -> AP -> AP.
Parameter ConjS : Conj -> S -> S -> S.
Parameter ConjNP : Conj -> NP -> NP -> NP.
Parameter UsePN : PN -> NP.
Parameter UseV : V -> VP.
Parameter UseN : N -> CN.
Parameter UseA : A -> AP.
Parameter some_Det : Det.
Parameter every_Det : Det.
Parameter we_NP : NP.
Parameter you_NP : NP.
Parameter very_AdA : AdA.
Parameter Pos : Pol.
Parameter Neg : Pol.
Parameter and_Conj : Conj.
Parameter or_Conj : Conj.
Parameter man_N : N.
Parameter woman_N : N .
Parameter house_N : N.
Parameter tree_N : N .
Parameter big_A : A .
Parameter small_A : A .
Parameter green_A : A .
Parameter walk_V : V .
Parameter arrive_V : V .
Parameter love_V2 : V2 .
Parameter please_V2 : V2 .
Parameter john_PN : PN .
Parameter mary_PN : PN.Now, every correct GF abstract syntax expression is a well-typed expression in Coq as well. We can even do (trivial) reasoning.
Theorem thm0 : UseCl Pos (PredVP (UsePN john_PN) walk_V) ->
UseCl Pos (PredVP (UsePN john_PN) walk_V).
intro H.
exact H.
Qed.This may seem useless, but in fact, unless you have a very precise idea of your semantic domain, much of the lexicon will remain abstract.
Definition S : Type := Prop .
Definition Cl : Type := Prop .
Definition Pol : Type := Prop -> Prop .
Definition Pos : Pol := fun p => p.
Definition Neg : Pol := fun p => not p.
Definition UseCl : Pol -> Cl -> S :=
fun pol c => pol c. Theorem thm1 : UseCl Pos (PredVP (UsePN john_PN) walk_V) ->
UseCl Neg (PredVP (UsePN john_PN) walk_V) -> False.
unfold UseCl.
unfold Pos.
unfold Neg.
intros P N.
exact (N P).
Qed.
Theorem thm1prime : forall c, UseCl Pos c -> UseCl Neg c -> False.
cbv.
intros P N.
exact (N P).
Qed.Parameter object : Type.
Definition PN : Type := object.
Definition NP : Type := PN.
Definition UsePN : PN -> NP := fun x ==> x.
Definition VP : Type := object -> Prop.
Definition V : Type := object -> Prop.
Definition UseV : V -> VP := fun v => v.
Definition PredVP : NP -> VP -> Cl := fun np vp => vp np.
Eval cbv in UseCl Pos (PredVP (UsePN john_PN) walk_V).= walk_V john_PN : S
The previous definition of NP is too restrictive in the presence of quantifiers. Indeed a PN is too restrictive to represent phrases such as ‘every man’, ‘some tree’, etc. Montague’s solution is to generalize NPs to be predicates over VPs:
Definition NP : Type := VP -> Prop . (* NP := (PN -> Prop) -> Prop *)
Definition UsePN : PN -> NP := fun pn vp => vp pn.
Definition PredVP : NP -> VP -> Cl := fun np vp => np vp.Eval cbv in UseCl Pos (PredVP (UsePN john_PN) walk_V).
Exercise: evaluate the above example step by step.
UseCl Pos (PredVP (UsePN john_PN) walk_V).
UseCl Pos (PredVP (\vp -> vp john_PN) walk_V).
UseCl Pos ((\vp -> vp john_PN) walk_V).
UseCl Pos (walk_V john_PN).
walk_V john_PN.Then we can interpret “everyone” as follows:
Definition everyoneNP : NP := fun vp => forall x, vp x.Namely, we’re applying the VP to every possible ‘thing’.
Exercise: evaluate everyoneNP walk_V
We may want to restrict the domain: “every man”, “some tree”, etc. Thus we will represent common nouns as predicates (like VPs) and weaken the propositions accordingly. A determiner transforms common nouns into NPs.
Definition CN : Type := PN -> Prop .
Definition N : Type := CN .
Definition Det : Type := CN -> NP .
Definition DetCN : Det -> CN -> NP := fun det cn => det cn.
Definition every_Det : Det := fun cn vp => forall x, cn x -> vp x.
Definition some_Det : Det := fun cn vp => exists x, cn x /\ vp x.Note the inversion of polarity in the connectives.
Definition N : Type := CN .
Parameter UseN : N -> CN. Theorem thm2 :
UseCl Pos (PredVP (DetCN every_Det man_N) walk_V) ->
(man_N john_PN) ->
(walk_V john_PN).
cbv.
intros H1 H2.
exact (H1 john_PN H2).
Qed.We can try the usual recipe and represent adjectives as predicates:
Definition AP : Type := object -> Prop .
Definition A : Type := AP .
Definition ModCN : AP -> CN -> CN := fun ap cn x => ap x /\ cn x.
Definition CompAP : AP -> VP := fun ap => ap.
(*Definition CompAP : AP -> VP := fun ap => "is " ++ ap. fake gf *)“every green tree is green.”
Theorem thm3 :
UseCl Pos (PredVP (DetCN every_Det (ModCN (UseA green_A) (UseN tree_N)))
(CompAP (UseA green_A))).
cbv.
intuition.
Qed.Definition V2 : Type := PN -> VP .
Definition ComplV2 : V2 -> NP -> VP := fun v object subject => object (v subject).Definition Conj : Type := Prop -> Prop -> Prop .
Definition ConjS : Conj -> S -> S -> S := fun c => c.
Definition ConjNP : Conj -> NP -> NP -> NP := fun c np1 np2 vp =>
np1 (fun x => np2 (fun y => c (vp x) (vp y))).
Definition and_Conj : Conj := fun x y => x /\ y.
Definition or_Conj : Conj := fun x y => x \/ y.“John loves Mary and a tree.” Eval cbv in UseCl Pos (PredVP (UsePN john_PN) (ComplV2 love_V2 (ConjNP and_Conj (UsePN mary_PN) (DetCN some_Det (UseN tree_N))))). exists x : PN, tree_N x /\ love_V2 john_PN mary_PN /\ love_V2 john_PN x
Even in the presence of abstract parameters, one can add arbitrary assumptions.
example: green and black are disjoint properties:
Parameter green_black_disjoint: forall x, green_A x -> black_A x -> False.Other types of knowledge which can be treated this way:
- Pragmatics
- John saw that x ⇒ x is true
- Hyperintentionality:
- John believes y ∧ John believes (x → y) ⇒ John believes y
Pause and reflect
The above is a basic approach only. In the papers (linked below) we have supported more (generally useful) constructions.
Wishes?
In general, the meaning of an ajective depends on the noun that it modifies. Adjectives and adjectival phrases are represented as modifiers of common nouns.
Definition A := CN -> CN.- Intersective (fun cn x => a x /\ cn x).
- Subsective (fun cn x => a cn x /\ cn x). (Skillful doctor, Skillful archer). Skillful does not transfer across nouns. A skillful doctor who also practises archery is not necessary a skillful archer.
- Privative. (fun cn x => a x /\ not (cn x)). Heavily depends on the domain and the goals of the semantics. (“Fake gun”, “Interrupted route”, “Healthy patient”)
- Non-commital (fun cn x => a cn x /\ cn x)
An intersective adjective (IntersectiveA) is fully defined by a
predicate over objects. The adjectival meaning is the conjunction of
such predicate and the bare noun (wkIntersectiveA). Additionally,
to relieve the user from calling this semantic function in in many
places, we declare it as an implicit coercion.
Definition IntersectiveA := object -> Prop.
Definition wkIntersectiveA : IntersectiveA -> A
:= fun a cn (x:object) => a x /\ cn x.
Coercion wkIntersectiveA : IntersectiveA >-> A.Later on it suffices to define
Parameter green_A : IntersectiveA. To specify the class.
Subsective adjectives may transfer across equivalent nouns.
Inductive ExtensionalSubsectiveA : Type :=
mkExtensionalSubsective :
forall (a : (object -> Prop) -> (object -> Prop)),
forall (ext : forall (p q:object -> Prop),
(forall x, p x -> q x) -> (forall x, q x -> p x) -> forall x, a p x -> a q x),
ExtensionalSubsectiveA.
Definition apExtensionalSubsectiveA
: ExtensionalSubsectiveA -> A
:= fun a cn (x:object) => let (aa,_) := a in
aa cn x /\ cn x .
Coercion apExtensionalSubsectiveA : ExtensionalSubsectiveA >-> A.In the same way we treated intersective adjectives, we add the semantics as a coercion for subsectives as well. It should be stressed that it suffices to declare an adjective as extensional subsective for Coq to remember the extensional property, even though it does not appear in the interpretation as a coerced general adjective.
Adverbs are similar to adjectives, except that they modify verbal predicates or propositions instead of nouns. For FraCas we chose adverbs to be veridical and covariant.
Definition ADV := (object -> Prop) -> (object -> Prop).
Definition Adv:= ADV.
Definition VeridicalAdv :=
{ adv : (object -> Prop) -> (object -> Prop)
& (forall (x : object) (v : object -> Prop), (adv v) x -> v x) *
(forall (v w : object -> Prop),
(forall x, v x -> w x) -> forall (x : object), adv v x -> adv w x)
}.The plain adverbial semantics are recovered by extracting the adv
component. The additional properties are made available solely by
declaring lexical entries as belonging to the correct class. A
coercion between VeridicalAdv and Adv is further defined (in effect we
define veridical adverbs to be subtypes of adverbs). Example:
Parameter on_time_Adv : VeridicalAdv .In the resource grammar, a noun phrase is comprised of several components:
mkNP : Quant -> Num -> CN -> NP
example:
- ⟦this five old men⟧ = mkNP ⟦this⟧ ⟦five⟧ ⟦old men⟧
Additionnally we have predeterminers:
mkNP : Predet -> NP -> NP
example:
- most, all, etc.
This is problematic, because they are naturally interpreted as quantifiers.
- remember the components of the NP as such. Therefore the semantics
that we use is a tuple of the components of noun-phrases: number,
quantifier, and common noun:
Inductive NP : Type := mkNP : Num -> Quant -> CN -> NP. - Predeterminers update the quantifier part of the NP. For example,
the “all” and “most” predeterminers replace the quantifier part
by the corresponding quantifier:
Definition Predet := NP -> NP. Definition all_Predet : Predet := fun np => let (num,qIGNORED,cn) := np in mkNP num all_Quant cn. Definition most_Predet : Predet := fun np => let (num,qIGNORED,cn) := np in mkNP num MOST_Quant cn.
- when appliying a NP (eg. in PredVP), we can apply the quantifier to
the CN (and the number)
Definition NP0 := VP -> Prop.
We can record the number as precisely as possible the information given by the syntax; which can be a singular, a plural, a precise cardinality or even the “more than” modifier.
Inductive Num : Type :=
singular : Num |
plural : Num |
unknownNum : Num |
moreThan : Num -> Num |
cardinal : nat -> Num .Generalised quantifiers turn a number and a common noun into a (usual)
noun-phrase (which we call NP0).
Definition Quant := Num -> CN -> NP0.Certain quantifiers ignore the number, and are thus given usual definitions:
Definition all_Quant : Quant :=fun (num:Num) (cn : CN) (vp : VP) => forall x, cn x->vp cn x.Some others, such as “at most” make essential use of the number:
Definition atMost_quant : Quant
:= fun num cn vp => interpAtMost num (CARD (fun x => cn x /\ vp cn x))In the above, interpAtMost checks that the given number is less than
the given cardinality. The function CARD is a context-dependent
abstract function which turns a predicate into a natural number. We
equip CARD with common-sense axioms of set cardinality, such as
monotonicity:
Parameter CARD : (object -> Prop) -> nat.
Variable CARD_monotonous : forall a b:CN, (forall x, a x -> b x) -> CARD a <= CARD b.The CARD variable is used to interpret several other quantifiers,
including “most”:
Definition MOST_Quant : Quant :=
fun num (cn : CN) (vp : VP) => CARD (fun x => cn x /\ vp cn x) >= MOSTPART (CARD cn).where MOSTPART is another context-dependent abstract function from
natural to natural. To support FraCas examples, it is sufficient to
equip it with a monotonicity axiom:
Parameter MOSTPART: nat -> nat.
Variable MOST_mono : forall x, MOSTPART x <= x.As usual, articles are special cases of quantifiers. When a useful number is provided by the NP, the indefinite article enforces it. Otherwise it generates an existential quantification.
Definition IndefArt:Quant:= fun (num : Num) (P:CN)=> fun Q:VP=> match num with
cardinal n => CARD (fun x => P x /\ Q P x) = n |
moreThan n => interpAtLeast n (CARD (fun x => P x /\ Q P x)) |
_ => exists x, P x/\Q P x end .The definite article checks for plural noun phrases, in which case it
implements definite plurals (universal quantification). Otherwise, it
looks up the object of discourse in an abstract
Definition DefArt:Quant:= fun (num : Num) (P:CN)=> fun Q:VP=> match num with
plural => (forall x, P x -> Q P x) /\ Q P (environment P) /\ P (environment P) |
_ => Q P (environment P) /\ P (environment P) end.Prepositions are interpreted as values transforming simplified noun phrases (1) to predicates. This transformation is veridical (2) and covariant (3). These three aspects are captured in three fields of a record, as follows.
Definition NP1 := (object -> Prop) ->Prop.
Inductive Prep : Type :=
mkPrep : forall
(prep : NP1 -> (object -> Prop) -> (object -> Prop)), (* 1 *)
(forall (prepArg : NP1) (v : object -> Prop) (subject : object), (* 2 *)
prep prepArg v subject -> v subject) ->
(forall (prepArg : NP1) (v w : object -> Prop),
(forall x, v x -> w x) -> forall x, prep prepArg v x -> prep prepArg w x) (* 3 *)
-> Prep.- Change the interpretation of adjective to be a measure:
Inductive A : Type := mkA : forall (measure : (object -> Prop) -> object -> Z) (threshold : Z) (property : (object -> Prop) -> (object -> Prop)), A.
- Now we can precisely compare things!
Definition ComparA : A -> NP -> AP
:= fun a np cn x => let (measure,_,_) := a in
apNP np (fun _class y => (measure cn y < measure cn x)).
Definition ComparAsAs : A -> NP -> AP
:= fun a np cn x => let (measure,_,_) := a in
apNP np (fun _class y => measure cn x = measure cn y).- Subsective adjectives have different comparison classes.
- Most of the time, the comparatives are used in a copula, and in that case the cn comes from the NP.
Relative clauses are interpreted as verb phrases and used intersectively when building noun phrases:
Definition RS := VP.
Definition RelNPa : NP -> RS -> NP
:= fun np rs => let (num,q,cn) := np
in mkNP num q (fun x => cn x /\ rs cn x).General recommended idea:
- define a concept of environment (discourse background)
- change the semantics to be functions from an environment to a pair
of (old) semantics and a new environment [ie. a state monad]
example:
VPbecomesEnv → (Env,VP) - new PN, verbs, etc. update the environment
- pronouns, etc. lookup what they need in the environment
Definition s_063_1_p := (Sentence (UseCl (Present) (PPos) (PredVP
(PredetNP (at_least_Predet) (DetCN (DetQuant (IndefArt) (NumCard
(NumNumeral (N_three)))) (AdjCN (PositA (female_A)) (UseN
(commissioner_N))))) (AdvVP (ComplSlash (SlashV2a (spend_V2)) (MassNP
(UseN (time_N)))) (at_home_Adv))))).
Theorem test : (s_063_1_p -> False).
cbv.
destruct at_home_Adv as [atHome [verid mono]].
simpl.atHome : (object -> Prop) -> object -> Prop verid : forall (x : object) (v : object -> Prop), atHome v x -> v x mono : forall v w : object -> Prop, (forall x : object, v x -> w x) -> forall x : object, atHome v x -> atHome w x ============================ 3 <= CARD (fun x : object => (female_A x /\ commissioner_N x) /\ atHome (fun y : object => exists x0 : object, time_N x0 /\ spend_V2 x0 y) x) -> False
P1 All mice are small animals. P2 All elephants are large animals. P3 Mickey is a large mouse. P4 Dumbo is a small elephant. --------------------------------------- H Dumbo is larger than Mickey.
Definition opposite_adjectives : A -> A -> Prop
:= fun a1 a2 =>
forall cn o, let (mSmall,threshSmall,_) := a1 in
let (mLarge,threshLarge,_) := a2 in
( (mSmall cn o = - mLarge cn o)
/\ (1 <= threshLarge + threshSmall)).
Variable small_and_large_opposite_K : opposite_adjectives small_A large_A.
Theorem FraCas212:s_212_1_p -> s_212_2_p -> s_212_3_p -> s_212_4_p -> s_212_6_h.
cbv.
assert (slK := small_and_large_opposite_K).
destruct small_A as [small smallThreshold].
destruct large_A as [large largeThreshold].
intros P1 P2 [largeM mouse] [smallD eleph].
(* here *)
destruct (slK animal_N DUMBO) as [neg disj].
destruct (slK animal_N MICKEY) as [neg' disj'].
destruct (P1 _ mouse) as [X Y].
destruct (P2 _ eleph) as [Z W].
lia.
Qed.Here:
small : (object -> Prop) -> object -> Z smallThreshold : Z large : (object -> Prop) -> object -> Z largeThreshold : Z slK : opposite_adjectives (mkSubsective small smallThreshold) (mkSubsective large largeThreshold) P1 : forall x : object, mouse_N x -> smallThreshold <= small animal_N x /\ animal_N x P2 : forall x : object, elephant_N x -> largeThreshold <= large animal_N x /\ animal_N x largeM : largeThreshold <= large mouse_N MICKEY mouse : mouse_N MICKEY smallD : smallThreshold <= small elephant_N DUMBO eleph : elephant_N DUMBO ============================ 1 <= large animal_N DUMBO - large animal_N MICKEY
- Ranta, 2004. “Computational semantics in type theory”. http://msh.revues.org/pdf/2925
- Bernardy and Chatzikyriakidis, 2017. (IWCS 2017)
- Bernardy and Chatzikyriakidis, 2019. (NoDaLiDa 2019)
- Drafts