The book uses a combination of a string and an integer as a representation of a variable in first-order logic. An alternative is to use a Haskell variable. In this approach, a quantified formula consists of the constructor for the quantifier and a function from terms to formulas. In other words, we treat \[ \forall x\: \varphi \] as a shorthand for \[ \forall (\lambda x.\varphi), \] where the \(\lambda\)-abstract is a real function, not an expression. The local variable in the function definition plays the role of the bound variable.
The method of using the variable binding mechanism present in the metalanguage to represent variable binding in the object language is called higher-order abstract syntax. The advantage of this approach is that you do not have to worry about choosing the names of variables, because the metalanguage interpreter takes care of the task of managing metalanguage variables.
The truth definition for first-order logic represented this way also becomes simpler—you can easily get by without variable assignments and use substitution of parameters (standing for elements of the universe of the model) for variables instead. Since the scope of the quantifier is a real function, there's no need to define substitution; simply apply the \(\lambda\)-abstract to whatever term you want to substitute for the variable.
Imports Model.hs from the book. (I haven't checked this code thoroughly.)
FsynF and MCWPL, write a function
some_boy_helped_some_girl :: Int -> Sentthat behaves as follows:
*Exercise1> some_boy_helped_some_girl 0 Sent (NP1 Some Boy) (VP1 Helped (NP1 Some Girl)) *Exercise1> some_boy_helped_some_girl 1 Sent (NP1 Some Boy) (VP1 Helped (NP2 Some (RCN1 Girl That (VP1 Helped (NP1 Some Girl))))) *Exercise1> some_boy_helped_some_girl 2 Sent (NP1 Some Boy) (VP1 Helped (NP2 Some (RCN1 Girl That (VP1 Helped (NP2 Some (RCN1 Girl That (VP1 Helped (NP1 Some Girl)))))))) *Exercise1> some_boy_helped_some_girl 3 Sent (NP1 Some Boy) (VP1 Helped (NP2 Some (RCN1 Girl That (VP1 Helped (NP2 Some (RCN1 Girl That (VP1 Helped (NP2 Some (RCN1 Girl That (VP1 Helped (NP1 Some Girl))))))))))) *Exercise1> lfSent (some_boy_helped_some_girl 2) E x4 conj[boy[x4],E x3 conj[conj[girl[x3],E x2 conj[conj[girl[x2],E x1 conj[girl[x1],help[x2,x1]]],help[x3,x2]]],help[x4,x3]]] *Exercise1> lfSent (some_boy_helped_some_girl 3) E x5 conj[boy[x5],E x4 conj[conj[girl[x4],E x3 conj[conj[girl[x3],E x2 conj[conj[girl[x2],E x1 conj[girl[x1],help[x2,x1]]],help[x3,x2]]],help[x4,x3]]],help[x5,x4]]] *Exercise1>
lfSent given in the book is suboptimal because bInLF unfolds an LF that has already been constructed to collect all integers used in variables inside it. (Try running lfSent (some_boy_helped_some_girl 20).) What is the number of times bInLF is called during the execution of lfSent (some_boy_helped_some_girl n)?
lfSent, call it lfSentTD, for which we get
*Exercise1> lfSentTD (some_boy_helped_some_girl 2) E x1 conj[boy[x1],E x2 conj[conj[girl[x2],E x3 conj[conj[girl[x3],E x4 conj[girl[x4],help[x3,x4]]],help[x2,x3]]],help[x1,x2]]] *Exercise1> lfSentTD (some_boy_helped_some_girl 3) E x1 conj[boy[x1],E x2 conj[conj[girl[x2],E x3 conj[conj[girl[x3],E x4 conj[conj[girl[x4],E x5 conj[girl[x5],help[x4,x5]]],help[x3,x4]]],help[x2,x3]]],help[x1,x2]]] *Exercise1> lfSentTD (Sent (NP1 The Boy) (VP1 Helped (NP1 The Girl))) E x1 conj[A x2 (boy[x2]<=>x1==x2),E x2 conj[A x3 (girl[x3]<=>x2==x3),help[x1,x2]]] *Exercise1>The running time of
lfSentTD s should be linear in the size of s. Hint: Define a function that takes a sentence and an integer and returns an LF. The integer should be used in the variable bound by the leftmost quantifier in the LF.
lfSent, call it lfSentBU, which works bottom-up like lfSent but runs in linear time. Hint: Define a function that takes a sentence and returns a pair consisting of an LF and an integer. The integer should be the maximal integer used in variables inside the LF.Last modified: 2017-04-06 19:08:06 JST