Abstract
Abstract. In order to answer questions and solve problems that require deeper reasoning with respect to a given text, it is necessary to automatically translate English sentences to formulas in an appropriate knowledge representation language. This paper focuses on a method to translate sentences to First-Order Logic (FOL). Our approach is inspired by Montague's use of lambda calculus formulas to represent the meanings of words and phrases. Since our target language is FOL, the meanings of words and phrases are represented as FOL-lambda formulas. In this paper we present algorithms that allow one to construct FOL-lambda formulas in an inverse manner. Given a sentence and its meaning and knowing the meaning of several words in the sentence our algorithm can be used to obtain the meaning of the other words in that sentence. In particular the two algorithms take as input two FOL-lambda formulas G and H and compute a FOL-lambda formula F such that F with input G, denoted by F @G, is H; respectively, G@F = H. We then illustrate our algorithm and present soundness, completeness and complexity results, and briefly mention the use of our algorithm in a NL Semantics system that translates sentences from English to formulas in formal languages.
Introduction
Our overall goal is to translate English to formal logics and Knowledge Representation (KR) languages. In this, our approach is to use λ-calculus formulas [1] to represent the meaning of words, phrases and sentences as previously done in [2] , [3] , [4] and [5] . To construct the meaning of a sentence from the meaning of its constituent words and phrases we use Combinatory Categorial Grammar (CCG) [6] . A big challenge in the above approach is to come up with the λ-calculus formulas that represent the meaning of the words. In some of the above mentioned works, they were either constructed by the authors or generated by a hand crafted set of rules. However, such an approach is not scalable. By analyzing how a human would come up with the λ-calculus formulas of words we noticed that at times a human, given G and H, would try to construct a formula F such that F @G = H or G@F = H.
Introduction
We illustrate the basic idea of inverse application of FOL-λ-calculus formulas and how they can be used in constructing the FOL-λ-calculus expressions of words through the following example. Here we take an example from the database querying domain of [7] that is presented in Table 1 .
Introduction
Texas borders a state N P (S\N P )/N P N P/N P N P N P (S\N P )/N P N P N P (S\N P In Table 1 it is assumed that one knows the meaning or translation of the sentence "Texas borders a state" and knows the FOL-λ-calculus formulas for "Texas", "borders", and "state". But the semantic representation for the word "a" is not known. The first step to compute this missing semantic representation is to take the meaning of the sentence "Texas borders a state" and the meaning of the word "Texas" to compute the semantic representation of "borders a state". But to do that one needs to know or a-priori decide whether it is appropriate to use the meaning of "Texas" as an input to the meaning of "borders a state" or vice versa. Traditional grammars such as Context Free Grammars do not help us in this. On the other hand, Combinatory Categorial Grammars (CCGs) [8] provide us directionality information that can be used in deciding which is the input and which is the function.
Introduction
In Table 1 the top part gives a CCG parse of the sentence "Texas borders a state". The various symbols correspond to basic categories; "S" represents a sentence, "N P " represents a noun phrase; and more complex categories are formed using "\" and "/" slashes which specify directionality. For instance, the category "S\N P " specifies that when a phrase corresponding to that category is concatenated on the left with a phrase of category "N P " , then the resulting phrase is of the category "S"; i.e., a sentence. Intuitively, a non-transitive verb has a category "S\N P ", meaning that if a noun phrase is added on the left, we get a sentence. Similarly, the category "N P/N P " means that a phrase of that category concatenated on the right by a phrase of category "N P " results in a phrase of the category "N P ".
Introduction
The phrase "Texas" has a category "N P " and it is being applied from the right to "borders a state". Therefore, if we take H as the meaning of the sentence and G as the meaning of "Texas", we can see by inspection that an F , the meaning of "borders a state", such that F @G = H can be F = λy.∃x.[state(x) ∧ borders(x, y)]. Now we can take H as the meaning of "borders a state" and G as the meaning of "borders", which has category (S\N P )/N P , and we can can find the meaning of F , for "a state". Since "a state" has category N P and is applied to the right of "borders", we need to find F such that G@F = H which can be F = λy.∃x.[state(x) ∧ y@x]. Finally, with H being the expression for "a state" and G being the expression for "state", with category N P , we can obtain F , a representation for "a", with category N P/N P . Therefore, we need F @G = H, which can be F = λz.λy.∃x. [z@x ∧ y@x] . This is the typed first-order λ-calculus representation for the simple word "a". But how exactly did we compute it?
Introduction
The main goal of this paper is to address that and present algorithms which are capable of automatically computing F such that F @G = H or G@F = H. It is this task we refer to as the Inverse λ-Problem and our algorithms as Inverse λ-Algorithms. The algorithm that computes F such that F @G = H, we call Inverse L , while the second algorithm which computes F such that G@F = H, we call Inverse R . Although our algorithms are defined in a way that they can be useful with respect to multiple KR languages, in this paper we focus on First-Order Logic as the KR language.
Introduction
To help in showing the correctness and applicability of our Inverse L and Inverse R algorithms we need to recap the notion of typed λ first order theories and the notion of order in such theories, as these notions will be used when we present the soundness, completeness and complexity results of our Inverse λ-Algorithms. For example, the completeness result is with respect to typed first order theories up to the second order. This recapping is done in Section 2.
Introduction
The rest of this paper is organized as follows. In Section 3 we present the Inverse λ-Algorithms. In Section 4 we illustrate our algorithms with respect to several examples. In Section 5 we show a use case example. In section 6 we present the complexity, soundness and completeness results. In Section 7 we discuss related work and other approaches in solving the Inverse λ-Problem. Finally, in Section 8 we conclude and briefly mention the companion learning based natural language semantics system that uses our algorithms as described in [9] .
Introduction
Overall, the main contributions of this paper are the development of the Inverse λ-Algorithms for typed λ first order theories and the presentation of soundness, completeness and complexity results for these algorithms.
Background
Montague, [10] , was the first to suggest that natural languages need not be treated differently from formal languages and they could have formal semantics. The approach of using λ-calculus to represent the meaning of words and λ-application as a mechanism to construct the meaning of phrases and sentences is also considered to originate from Montague. As mentioned before, that is also our approach.
Background
However, to further ground the notion of "meaning" (or semantics) it is useful to have a notion of models of λ-calculus expressions. Such notions also allow us to evaluate our natural language meaning representations. Both untyped and typed λ-calculus can be characterized using models, but the one that has had the most impact on natural language semantics is typed λ-calculus, as creating models for typed λ-calculus theories is somewhat simple. When we refer to model, we are looking for a semantic tool that can give us two elements: the entities that we have in our domain, and for every element in our signature, the semantic value associated with it.
Background
We will use the "Simply Typed Lambda Calculus" of Church (1940), since it is most commonly used in linguistics. In this theory, there is only one type constructor, →, to build function types and each term has a single type associated with it [11] . The books [12] and [13] are good reference points for typed lambda calculus.
Typed First-Order Logic Lambda Calculus
First-Order Logic has been widely studied and used for many years. Since a large body of research in natural language semantics has focused on translating natural language to first-order logic we focus our Inverse λ-Algorithms on it, particularly on Typed First-Order Logic Lambda Calculus. For obtaining formal results, we need to define the signature of our language, the construction of typed terms and typed formulas, and the notion of sub-terms of a typed term in the language.
Typed First-Order Logic Lambda Calculus
We start by introducing the signature of the Typed First-Order Logic Lambda Calculus Language (Typed FOL Lambda Calculus). It consists of: -The lambda operator (also called the lambda-abstractor) λ, the lambda application @, the parenthesis (, ), [, ] .
Typed First-Order Logic Lambda Calculus
-For every type a, an infinite set of variables v n,a for each natural number n and a (possibly empty) set of constants c a .
Typed First-Order Logic Lambda Calculus
-The quantifiers ∀ and ∃, the equality symbol =, the connectives ¬, ∨, ∧, →.
Typed First-Order Logic Lambda Calculus
-Predicates symbols and function symbols of any arity n.
Typed First-Order Logic Lambda Calculus
Next, we introduce the set of types that are going to be used with Typed FOL Lambda Calculus, in conjunction with the definition of the semantics of types assigned to the different expressions of the language. We will follow the principles presented in [14] , where D a represents the set of possible objects (denotations) that describe the meanings of expressions of type a. Thus, denotations are the objects of the language that correspond to a given type.
Typed First-Order Logic Lambda Calculus
The set of types ∆ is defined recursively as follows:
Typed First-Order Logic Lambda Calculus
-e is a type. -t is a type.
Typed First-Order Logic Lambda Calculus
-If a and b are types, then (a → b) is a type.
Typed First-Order Logic Lambda Calculus
Let E be a given domain of entities. Then the semantics of the types are defined as: These letters are commonly used in the linguistics literature. An expression of type e denotes individuals that belong to the domain of our model, expressions of type t denote truth values and they will be assigned to expressions that can be evaluated to a truth value in our model. Expressions of type (a → b) denote functions whose input is in D a and whose output values are in D b . For example, the type e → t corresponds to functions from entities to truth values.
Typed First-Order Logic Lambda Calculus
We continue with the definitions for FOL typed term and FOL typed λ-calculus formula. A FOL atomic term is a constant or a variable of any type a. If t 1 , ..., t n are FOL atomic terms, and f is a function symbol, f (t 1 , ..., t n ) is also a FOL atomic term of type e. Definition 1. The elements of the set ∆ α of FOL typed terms of type α are inductively defined as follows:
Typed First-Order Logic Lambda Calculus
1. For each type a, every FOL atomic term of type a belongs to ∆ a . 2. If P is a predicate symbol of arity n and t 1 , ..., t n are FOL atomic terms, then P (t 1 , ..., t n ) is a FOL typed atomic formula that belongs to ∆ t . 3. For any types a and b, if α ∈ ∆ a→b and β ∈ ∆ a , then α@β ∈ ∆ b . 4. For any types a and b, if u is a variable of type a and α ∈ ∆ b has free occurrences of the variable u, then λu.α ∈ ∆ a→b and the free occurrences of u are now bound to the abstractor λu.
Typed First-Order Logic Lambda Calculus
If α and β ∈ ∆ e , then (α = β) ∈ ∆ t . 8. For any type a, if α ∈ ∆ t , and u is a variable of type a, then ∀uα and ∃uα ∈ ∆ t .
Typed First-Order Logic Lambda Calculus
A typed FOL λ-calculus formula is a FOL typed term of type a where every variable is bound to an abstractor (quantifier variables may not) and every abstractor binds to a variable. These conditions ensure that first-order formulas are obtained when the typed FOL λ-calculus formula is in β-normal 2 form and there are no more λ-operators. They also correspond to the definition of closed and λI terms from classical lambda calculus theory.
Typed First-Order Logic Lambda Calculus
Let us show an example. Consider the typed FOL formula λx.person(x), which has type e → t. In this case, the variable x is a typed variable ranging over the entities of the domain and therefore it has type e. When an individual from the domain, such as the typed constant of type e, "John", is applied to the formula, we obtain a First Order Formula person(John) which is of type t. The formula is no more than a function from individuals to truth values.
Typed First-Order Logic Lambda Calculus
This illustrates the signature for Typed FOL λ-calculus and shows how we can specify a model with a domain of entities and a function to assign semantics to elements of the signature. With such a model, we can choose an interpretation for the formula λx.person(x) where only those entities of the domain that belong to the set of the predicate person would return the value true as output of the function. Therefore the interpretation of λx.person(x)@John would be the same as the one for person(John) in the model. This is assured by the well-typed application that takes place between the formula e → t and the argument e, where a well-typed application is one where the type of the argument is the same as the "input" type of the function receiving it. In general, types are in charge of regulating which applications are possible and when both argument and function have the correct types, we have a well-typed expression.
Typed First-Order Logic Lambda Calculus
We end this sub-section with three more definitions that will be used by the Inverse λ-Algorithms.
Definition 2 (Occurrence). The relation P occurs in Q is defined by induction on Q as follows:
-A FOL typed term P occurs in P.
Definition 2 (Occurrence). The relation P occurs in Q is defined by induction on Q as follows:
-If P occurs in M or in N, then P occurs in M@N.
Definition 2 (Occurrence). The relation P occurs in Q is defined by induction on Q as follows:
-If P occurs in M, then P occurs in λx.M.
Definition 2 (Occurrence). The relation P occurs in Q is defined by induction on Q as follows:
-If P occurs in φ or P occurs in ψ, then P occurs in φ ∨ ψ, φ ∧ ψ, φ → ψ.
Definition 2 (Occurrence). The relation P occurs in Q is defined by induction on Q as follows:
-If P occurs in φ, then P occurs in ¬φ.
Definition 2 (Occurrence). The relation P occurs in Q is defined by induction on Q as follows:
-If P occurs in φ, then P occurs in ∀uφ and ∃uφ.
Definition 2 (Occurrence). The relation P occurs in Q is defined by induction on Q as follows:
-If P occurs in φ or P occurs in ψ, then P occurs in φ = ψ.
Definition 2 (Occurrence). The relation P occurs in Q is defined by induction on Q as follows:
-If P occurs in any typed term t i , then P occurs in f (t 1 , ..., t n ). Where f is a predicate symbol or a function symbol.
Definition 2 (Occurrence). The relation P occurs in Q is defined by induction on Q as follows:
A sub-term of a λ-calculus term F is any term P that occurs in F [13] . Example 1. Consider the typed FOL λ-calculus formula J = λw.λu.(man(John) ∧w@λz.(loves(z, u))). The typed terms loves(z, u), man(John), λz.(loves(z, u)), and w occur in J, and hence, are some of the sub-terms of J. However, λw is not a sub-term.
Definition 2 (Occurrence). The relation P occurs in Q is defined by induction on Q as follows:
Definition 3 (FOL λ-component). Constants, quantifier variables, connectives ¬, ∧, ∨ and →, quantifiers ∃ and ∀, predicates and function symbols, and the equality symbol = are denoted as FOL λ-components. The set of FOL λ-components of a formula J is identified as LC(J).
Definition 2 (Occurrence). The relation P occurs in Q is defined by induction on Q as follows:
Basically, all elements of the typed FOL λ-calculus signature except for the λ-application symbol, λ-abstractor and their corresponding bound variables, are considered FOL λ-components.
Definition 2 (Occurrence). The relation P occurs in Q is defined by induction on Q as follows:
Example 2. Consider the typed FOL λ-calculus formula J = λw.λu.(man(John) ∧ w@λz.(loves(z, u))). LC(J) = {man, John, ∧, loves}.
Type Order
So far we have introduced typed λ-calculus and the different types that will be assigned to typed terms. We now define the notion of an order that is associated with these types and that separates typed λ-calculus formulas to several classes. We will use the notion of orders to show that the Inverse λ-Algorithm is a complete algorithm for typed λ-calculus formulas up to order two. We start with a definition of type order and some intuition behind it: This definition is almost identical to the one introduced in [15] , where base types have order one. We, however, follow the intuition introduced in [2] . Some examples of typed FOL λ-calculus formulas of different orders are the following: -Order zero: man(V incent). It has type t. -Order one: λv.λu.(v → u). It has type e → (e → t). -Order two: λv.λu.(v@M ia∧u@V incent). It has type (e → t) → ((e → t) → t).
Type Order
-Order three: λw.(w@(λz.(happy(z)))). It has type ((e → t) → t) → t.
Type Order
With these simple examples, one can see the intuition behind the order of typed FOL λ-calculus formulas. Formulas of order zero correspond to expressions with base types. Formulas of order one correspond to expressions which start with a series of λ-abstractors followed by a FOL formula with variables bound to the initial λ-abstractors.
Type Order
Formulas of order two extend the expressions allowed in order one by including applications. Formulas of order zero can be applied to variables inside the formula. Formulas of order three extend those present in order two by allowing λ-abstractors inside the expression after the initial λ-abstractors. In this case, formulas of order one can be applied to variables, this is why now, we can find λ-abstractors at the beginning and in the middle of the formulas. These claims can be easily proved by contradiction using the given definitions.
The Inverse λ-Algorithms
We start this section by presenting a lemma and some properties that are important for the Inverse λ-Algorithms and that are helpful to understand its completeness. After this introduction, the Inverse λ-operators of the Algorithm will be defined along with the explanation of its different parts. We start by presenting a lemma based on Lemma 1B1.1 from [13] . Lemma 1. Given typed FOL λ-calculus formulas H, G and F , if G@F β-reduces 3 to H, then LC(G@F) = LC(H).
The Inverse λ-Algorithms
Proof. Our definition of typed FOL λ-calculus formulas implies that all variables that appear in a formula are bound (except quantifier variables). Therefore, when one formula is applied to another and β-contractions are performed, none of the λ-components of those formulas will be modified by the application due to the definition of application in λ-calculus. In case of clashes with quantifier variables, α-conversion 4 would be used as usual.
The Inverse λ-Algorithms
With this lemma, it can be shown that given typed FOL λ-calculus formulas H, G and F such that H = G@F or H = F @G, any FOL λ-component of H must be contained in either F or G (since we obtain H from these two formulas), and it can not be the case that a FOL λ-component in F or G will not appear in H (since there would be no proper second formula in the application that gives us H). This characteristic of the structure of the application is an essential part of the Inverse λ-Algorithms and the way in which it constructs the missing formula out of the other two. Also, by the way we defined typed FOL λ-calculus formulas, we eliminated the case where we set F to be λv.H which does not provide any semantic meaning to the expression that F represents but would be a valid classic λ-calculus formula for the application. Our aim is to keep the semantic information between F and G, which combined, give the semantics of H. By assuring that the information in G will lead us to obtain the semantics of H, we are providing F with a semantic representation that contains the value we are looking for.
The Inverse λ-Operators
This sub-section presents the formal definition of the two components of the Inverse λ-Algorithms, Inverse L and Inverse R . First, some definitions and explanations necessary to help understand the terminology used in defining Inverse L and Inverse R will be introduced. The objective of Inverse L and Inverse R , is that given typed λ-calculus formulas H and G, the formula F is computed such that F @G = H and G@F = H. The different symbols used in the algorithm and their meanings are defined as follows:
The Inverse λ-Operators
-Let G, H and J represent typed λ-calculus formulas, J 1 ,J 2 ,...,J n represent typed terms; and v, w and v 1 ,...,v n represent variables. Typed terms that are sub-terms of a typed term J i are denoted as J i k . If the formulas being processed within the algorithm do not satisfy any of the conditions, then the algorithm returns null.
The Inverse λ-Operators
Definition 5 (operator :). Consider two lists (of same length) of typed λ-calculus formulas A 1 , ..., A n and B 1 , .., B n , and a typed FOL λ-calculus formula H. The result of the operation H(A 1 , ..., A n : B 1 , . ., B n ) is defined as:
The Inverse λ-Operators
1. find the first occurrence of formulas A 1 , ..., A n in H. 2. replace each A i by the corresponding B i . 3. find the next occurrence of formulas A 1 , ..., A n in H and go to 2. Otherwise, stop.
The Inverse λ-Operators
Next, we present the definition of the two inverse operators: Definition 6 (Inverse L (H, G) ). Given G and H:
The Inverse λ-Operators
Definition 7 (Inverse R (H, G)). Given G and H: 
The Inverse λ-Operators
In this section we illustrate with examples each of the different conditions of the two algorithms. In each example λ-calculus formulas G and H are given and we want to find F using the given case of the Inverse λ-Algorithms. This section shows how the algorithms apply pattern matching to calculate F in the various cases. A use case example follows in the next section.
The Inverse λ-Operators
Inverse L -Case 1: H = woman(M ia) and G = λx.x. Then, F = λx.(x@H), and in this case F = λx.(x@woman(M ia)).
The Inverse λ-Operators
To demonstrate correctness we now apply G to F to get H:
The Inverse λ-Operators
Inverse L -Case 2:
H(G : v), which in this case yields F = λv.H(man(V incent) : v).
We substitute every appearance of G in H by the variable "v" obtaining
H(G : v), which in this case yields F = λv.H(man(V incent) : v).
Inverse L -Case 3: u) ), and G = λv.λw.(v ∧ happy(w)) G is not λv.v. That satisfies the first condition.
H(G : v), which in this case yields F = λv.H(man(V incent) : v).
To match the formula of G, the following are assigned the subterms of H: Thus, G = λv.J(f (σ 2 , σ 3 ) : v@σ 3 @σ 2 ), which in this case yields G = λv.J(f (M ia, V incent) : v@V incent@M ia). Thus, both conditions are satisfied. So, F can be calculated as follows: F = λwλv 1 (w@λv 1+1 , ..., v 3 .(f (σ 1+1 , ..., σ 3 : v k1+1 , ..., v k3 ) (w@λv 2 , λv 3 .lovesBef ore(v 3 , v 2 , v 1 ) ).
H(G : v), which in this case yields F = λv.H(man(V incent) : v).
Inverse R -Case 3:
H(G : v), which in this case yields F = λv.H(man(V incent) : v).
G is not λv.v@J, since J = M ia@V incent∧v@M ia@Robert cannot be a formula by the definition. That satisfies the first condition. From H, and chosen to match the input to the variable v of G, one has the following formulas that are sub-terms:
H(G : v), which in this case yields F = λv.H(man(V incent) : v).
= Robert Therefore, G can be seen to be of the form:
H(G : v), which in this case yields F = λv.H(man(V incent) : v).
x@M ia@Robert)). Thus, the second condition of case 3 is satisfied. Therefore, one can now calculate F :
Use Case Example
In this section, we revisit our earlier example and give another example to show how we can use the Inverse λ-Algorithms to obtain semantic representations for words when we have a sentence with its logical representation in typed first-order logic λ-calculus, the syntactic categories from CCG parsing and some semantic information. We again use an example from the database querying domain of [7] . Let us start with the sentences: "Texas borders a state.", and "What state borders Texas?". We will consider that our initial lexicon includes the semantics for simple nouns and verbs. If we obtain the output of a simplified CCG parsing with two categories "S" and "NP", and we add the semantics from our lexicon, we obtain what is presented in Table 2 .
Use Case Example
One can see in Table 2 that we are missing the semantic representation for the words "a" and "What". These two words are not part of our initial lexicon but using the Inverse λ-Algorithms we will be able to compute their corresponding typed first-order λ-calculus representation. Let us start with the first sentence.
Use Case Example
Texas borders a state What state borders Texas N P (S\N P )/N P N P/N P N P S/(S\N P )/N P NP (S\N P )/N P NP N P (S\N P )/N P N P S/(S\N P )/N P NP S\N P N P (S\N P ) S/(S\N P ) S\N P S S Texas borders a state texas λw.λx. (w@λy.borders(y, x) We can take the meaning of the sentence and the meaning of "Texas" to calculate the representation of "borders a state".
Use Case Example
We can see in the CCG tree that "borders a state" has category (S\N P ) and therefore the λ-calculus expression will receive the word "Texas" from the left. Following this, if we take H as the meaning of the sentence and G as the meaning of "Texas", we can use Inverse L (H, G) to obtain the expression for "borders a state". In this case, option one of the algorithm is satisfied with texas as formula J and F = λy.∃x.[state(x) ∧ borders(x, y)]. Now we have the expression for "borders a state" and "borders", we can calculate the expression of "a state" calling Inverse R (H, G) with H being the meaning for "borders a state" and G being "borders". Option four of the algorithm is satisfied and we obtain F as λy.∃x.[state(x) ∧ y@x]. Finally, we call Inverse L (H, G) with H being the expression for "a state" and G being "state" to obtain the desired representation for "a". In this case, option two of the algorithm is satisfied and F = λz.λy.∃x.[z@x ∧ y@x]. This is the typed first-order λ-calculus representation for the simple word "a".
Use Case Example
The process to obtain the word "What" from the second sentence follows the same idea as shown above. First we call Inverse L (H, G) with H being the meaning of the sentence and G being "borders Texas" to obtain the meaning of "What state". Option two of the algorithm is satisfied and F = λy.λx.(state(x)∧ y@x). Next, we call Inverse L (H, G) again with "What state" and "state" to obtain the desired meaning of "What". Option two of the algorithm is satisfied and F = λz.λy.λx.(z@x ∧ y@x).
Use Case Example
Using the Inverse λ-Algorithms we have easily added to our lexicon the λ-calculus representation for the words "a" and "What".
Use Case Example
Theorem 1 (Soundness). Given two typed FOL λ-calculus formulas H and
Use Case Example
Theorem 2 (Soundness). Given two typed FOL λ-calculus formulas H and G in β-normal form, if Inverse R (H, G) returns a non-null value F , then H = G @ F .
Theorem 3 (Completeness).
For any two typed FOL λ-calculus formulas H and G in β-normal form, where H is of order two or less, and G is of order one or less, if there exists a set of typed FOL λ-calculus formulas Θ F of order two or less in β-normal form, such that
Theorem 3 (Completeness).
Theorem 4 (Completeness). For any two typed FOL λ-calculus formulas H and G of order two or less in β-normal form, if there exists a set of typed FOL λ-calculus formulas Θ F of order one or less in β-normal form, such that ∀F i ∈ Θ F , H = G@F i , then Inverse R (H, G) will give us an F , where Due to space constraints, we will only comment on how the complexity, soundness and completeness proofs are structured. Inverse L has worst-case complexity in case 3. For every subterm of H it is necessary to check if a partial permutation of its subterms can be used to generate G. If G has k variables, then the number of permutations that needs to be checked is in worst case n! (n−k)! where n is the length of H. When k is small, as it is in most of the applications we have tested (see Section 8 below), the number of permutations becomes approximately O(n k ). The complexity of Inverse R is the same as Inverse L since Inverse L is called as a subroutine in case 1. All other cases of Inverse R run in polynomial time. Note that case 3 of Inverse R has polynomial complexity since the formulas given as input to the applications in G can be used to find the subterms of H that can generate them. Therefore, we do not have to search all permutation of the subterms as in Inverse L .
Theorem 3 (Completeness).
The soundness proof shows how in each of the four cases of Inverse L , the typed FOL λ-calculus formula H is obtained by applying F to G. The application F @G is computed using the expressions from the algorithm for F and G, generating the expression for H given in the algorithm. The same reasoning is followed for Inverse R .
Theorem 3 (Completeness).
The completeness proof is divided to six cases, which correspond to the six possible valid combinations of orders that H, F and G may have, such that the order of the terms will be less than 2. These are shown in Table 3 . For each case, it is proven by contradiction that Inverse L and Inverse R return a formula F if one such F exists. It is done by assuming that they return a null value and reaching a contradiction at the end of the proof. In the process, each of the four conditions of the algorithms are analyzed, where it is shown that at least one of the conditions of the algorithm has been satisfied for each of the six cases.
Theorem 3 (Completeness).
H F G FOL type examples for formula F 0 1 0 e → t 1 1 0 e → (e → t) 2 2 0 e → ((e → t) → t) 0 2 1 (e → t) → t 1 2 1 (e → t) → (e → t) 2 2 1 (e → t) → ((e → t) → t) Table 3 . Possible order combinations for F, G and H formulas, with H = F @G.
Related Work
The problems solved by the Inverse λ-Algorithms are similar to two problems referred to in the literature as "higher-order matching" and "Interpolation problem". This problem consists of determining if a λ-calculus term, in the simply typed λ-calculus, is an instance of another. It can also be understood as solving the equation M = N where M and N are simply typed λ-terms and N is a closed 6 term. More intuitively, the problem is to find a substitution σ assigning terms of consistent types to the free variables of M such that σ(M ) admits N as its normal form. A proof that third-order matching is decidable is presented in [16] . In literature about higher-order matching, the order of atomic types is generally 1. This slightly differs from the definition presented in this work. Thus, third order in [16] has to be understood as second order in this research.
Related Work
The higher-order matching and interpolation problems are defined with respect to an extension of λ-calculus denoted as βη-calculus 7 , while the Inverse λ-Algorithms follow the theory of β-calculus, since it is the theory most commonly used in linguistics. Another important difference is that in the case of Inverse L and Inverse R , terms G,F and H are typed λ-calculus formulas that, by definition, have been set as closed and λI terms, and are also considered in β-normal form. The higher-order matching and interpolation problems do 6 A λ-expression is closed if no free variables occur in it 7 βη-calculus allows for η-conversions as well as β-reductions. An η-conversion converts between λx.f @x and f whenever x does not appear as a free variable in f .
Related Work
not enforce these restrictions in the terms involved. However, in essence, both approaches deal with the same problem. Thus, we argue that Inverse R and Inverse L can be considered special cases of the matching and interpolation problems , respectively (when we restrict the problem to β-calculus and only try to substitute for one variable in M ). However, the Inverse λ-Algorithms provide an important contribution. As it is stated in [15] , the higher-order matching problem, in the general case, is undecidable when using β-calculus, as shown in [17] . Inverse R is an algorithm for computing a subset of the third order matching problem under β-calculus. Also, the higher-order matching algorithm proposed in [16] , where a set of solutions to a third order matching problem are enumerated, will not terminate if the problem admits no such set. In the case of Inverse R , the algorithm will simply return a null value and terminate.
Related Work
Another related work, [18, 19] , discusses two algorithms that solve the problem of learning word-to-meaning mappings extended to the field of typed λ-calculus. In [19] , the algorithm introduced considers β-calculus and closed λI terms. This definition is very closely related to the Inverse R definition. However, the author refers to the problem that the algorithm presents with incompatibility between meaning of words already known and meaning of words obtained by the algorithm. Our approach does not present such problem. Another key difference refers to the assumptions made before executing the algorithm. In [18, 19] , there is a first phase where the learner, in some way, obtains the set of constants that form each word. In the case of the Inverse λ-Algorithms, the unknown representation of words in a sentence is obtained using the meaning of the sentence and the meaning of known words. There is no previous information needed about the unknown meaning.
Related Work
The comparison with the works [15, 16, 18] is leading us to research the possible benefits of defining the Inverse λ-Algorithms in terms of βη-calculus, in order to use useful related results. This step will be approached in future work.
Related Work
A more general notion of higher-order matching is the notion of "higher-order unification". The difficulty of higher-order unification is studied in [20, 21] . In [22] a restricted version of higher-order unification is defined and used. They describe an algorithm which given h, finds pairs of logical expressions (f, g) such that either f (g) = h or λx.f (g(x)) = h. Note that in our Inverse λ-Algorithms the input consists of two expressions and the output is a single expression.
Implementation Success and Evaluation
The usefulness of the two Inverse λ-Algorithms is validated in the natural language learning system [9] , which learns the semantic representations of words from sentences. The algorithms were implemented by those authors as part of that system. The results obtained by the system in [9] are quite promising. A summary is presented in Table 4 . The system outperforms earlier systems with respect to the F-measure for the two standard corpora GEOQUERY and CLANG. In the table, Inverse and Inverse+ are two different versions of the system. As explained in [9] , Inverse uses the two Inverse λ-Algorithms, Inverse L and Inverse R and a process called generalization, which generalizes the meaning of unknown words from known words based on the syntactic information received from the CCG parser. Inverse+ adds trivial inverse results for some words and "on demand" generalization. Inverse+i considers the semantic representations "definec" and "definer" of the training data as the same element, with respect to the CLANG corpus.
GEOQUERY Precision
The evaluation of the data was performed using 10 fold cross validation and the C&C parser from [6] . An equal number of train and test sentences were arbitrarily selected from the GEOQUERY and CLANG corpora. For more details about this system and its results, we refer the reader to [9] .
Conclusion
In this work, we have presented two Inverse λ-Algorithms and have shown their application to typed first-order logic λ-calculus. With this algorithm we are able to automatically obtain semantic representations of unknown words using the information already available from known sentences and words. These two algorithms not only work for first-order logic, but with minor changes work for a group of other Knowledge Representation languages such as Answer Set Programming, and Linear Temporal Logic and Dynamic Logic; but formal results with respect to those languages need to be proven. For the algorithms we have developed a completeness proof up to second order expressions. Blackburn and Bos in [2] mention that natural language semantics rarely requires types above order three. Completeness results for third order expressions is the next step to extend this work and is part of our immediate future plans.

{'paper_id': '18796057', 'title': 'The Inverse Lambda Calculus Algorithm for Typed First Order Logic Lambda Calculus and Its Application to Translating English to FOL', 's2_url': 'https://api.semanticscholar.org/CorpusID:18796057', 'source': 'S2ORC'}