We investigate how formal concept analysis can be applied in a type-theoretic context, namely the context of λ-terms typed a` la Curry. We first show some general results, which reveal that concept lattices generally respect and reflect the type structure of terms. Then, we show an application of the results in formal language theory, where we vastly generalize existing approaches of capturing the distributional structure of languages by means of formal concept analysis. So type theory is interesting to formal concept analysis not only as a particular context, but also because it allows to generalize existing contexts.
Formal concept analysis (FCA) operates within what is called a context, that is typically a set of objects, a set of attributes and a relation between them. We will have a closer look at formal concept analysis over terms in a type theoretic context, and show how this can be applied to formal language theory. Our first contribution1 is that we consider the case not of an atomic typing, but rather recursive, Curry-style typing. Our objects are λ-terms, which have to be assigned types according to their syntactic structure. We show some interesting correlations between the type theoretic structure of sets of terms, their principal typing, and how this these interact with FCA and its lattice-theoretic operations. Our second main contribution is that we show an application to formal language theory. There exist interesting approaches to the distributional structure of languages using FCA over the relation of strings and the contexts in which they occur. However, all of these have some major limitations, as they only work with simple string concatenation, but cannot cope with, for example, the concept of string duplication in a language. We use a type theoretic encoding of strings as terms, and show that this allows us to vastly generalize existing approaches. Type theory starts with a (usually) finite set of basic types, and a finite, (usually) small set of type constructors. Types are usually interpreted as sets; we denote the c 2012 by the paper authors. CLA 2012, pp. 103–114. Copying permitted only for private and academic purposes. Volume published and copyrighted by its editors. Local Proceedings in ISBN 978–84–695–5252–0, Universidad de M´alaga (Dept. Matem´atica Aplicada), Spain. set of all objects of type τ by kτ k. We will consider only a single type constructor, the usual →, where for types σ, τ , σ → τ is the type of all functions from kσk to kτ k. Basic objects are assigned some type, and all new objects we can construct in our universe must be constructed in accordance with a typing procedure, that is, we have to make sure that they can be assigned at least one type. Objects which are not well-typed do not exist in the typed universe.
Given a non-empty set A of atomic types, the set of types T p(A) is defined as closure of A under type constructors: A ⊆ T p(A), and if σ, τ ∈ T p(A), then σ → τ ∈ T p(A). The order of a type is defined as ord(σ) = 0 for σ ∈ A, ord(σ → τ ) = max(ord(σ) + 1, ord(τ )).
We define a higher order signature as Σ := (A, C, φ), where A is a finite set of atomic types, C is a set of constants, and φ : C → T p(A) assigns types to constants. The order of Σ is max({ord(φ(c)) : c ∈ C}). Let X be a countable set of variables. The set Tm(Λ(Σ)), the set of all λ terms over Σ, is the closure of C ∪ X under the following rules: 1. C ∪ X ⊆ Tm(Λ(Σ)); 2. if m, n ∈ Tm(Λ(Σ)), then (mn) ∈ Tm(Λ(Σ)); 3. if x ∈ X, m ∈ Tm(Λ(Σ)), then (λx.m) ∈ Tm(Λ(Σ)).
We omit the outermost parentheses (, ) for λ terms, and write λx1...xn.m for λx1.(. . . (λxn.m)...); furthermore, we write m1m2 . . . mi for (. . . (m1m2) . . . mi). The set of free variables of a term m, F V (m), is defined by 1. F V (x) = {x} : x ∈ X, 2. F V (c) = ∅ : c ∈ C, 3. F V (mn) = F V (m)∪F V (n), and 4. F V (λx.m) = F V (m)−{x}. m is closed if F V (m) = ∅. We write m[n/x] for the result of substituting n for all free occurrences of x in m. α conversion is defined as λx.m α λy.m[y/x]. A β-redex is a term of the form (λx.m)n. We write β for β reduction, so we have (λx.m)n β m[n/x]. The inverse of β reduction is β expansion. Let [m]β denote the β normal form of m, that is, the term without any β redex. This term is unique up to α conversion for every term m. We denote by =αβ the smallest congruence which contains both α and β. We thus write m =αβ n, if n can be derived from m with any finite series of steps of β-reduction, expansion or α-conversion of any of its subterms.
We now come to the procedure of assigning types to terms.2 A type environment is a (possibly empty) set {x1 : α1, . . . xn : αn} of pairs of variables and types, where each variable occurs at most once. A λ-term m with F V (m) = {x1, . . . , xn} can be assigned a type α in the signature Σ = (A, C, φ) and type environment {x1 : α1, . . . xn : αn}, in symbols (1)
x1 : α1, . . . xn : αn ⊢Σ m : α, if it can be derived according to the following rules: (cons) ⊢Σ c : φ(c), for c ∈ C; (var) x : α ⊢Σ x : α, where x ∈ X and α ∈ T p(A); 2 We adopt what is known as Curry-style typing: in Church-style typing, terms cannot be constructed without types; in Curry-style typing, terms are first constructed and then assigned a type; so there might be the case that there is no possible assignment. Γ ⊢Σ m : β (abs) Γ − {x : α} ⊢Σ λx.m : α → β, provided Γ ∪ {x : α} is a type environment; (app) ∆ ⊢Σ n : α Γ ⊢Σ m : α → β Γ ∪ ∆ ⊢Σ mn : β
, provided Γ ∪ ∆ is a type environment.
An expression of the form Γ ⊢Σ m : α is called a judgment, and if it is derivable by the above rules, it is called the typing of m. A term m is called typable if it has a typing. If in a judgment we do not refer to any particular signature, we also write Γ ⊢ m : α. Regarding β reduction, we have the following well-known result: Theorem 1 (Subject Reduction Theorem) If Γ ⊢ m : α, m where Γ ′ is the restriction of Γ to F V (m′). β m′, then Γ ′ ⊢ m′ : α,
Let m β m′ be a contraction of a redex (λx.n)o. This reduction is non-erasing
if x ∈ F V (n), and non-duplicating if x occurs free in n at most once. A reduction
from m to m′ is non-erasing (non-duplicating) if all of its reduction steps are
nonerasing (non-duplicating). We say a term m is linear, if for each subterm λx.n of m,
x occurs free in n exactly once, and each free variable of m has just one occurrence
free in m. Linear λ-terms are thus the terms, for which each β-reduction is
nonerasing and non-duplicating. We will be mainly interested in a slightly larger class.
A term m is a λI term, if for each subterm λx.n of m, x occurs free in m at least
once. λI terms are thus the terms which do not allow for vacuous abstraction
(see [
Obviously, β is unique up to isomorphism; we will write pt(m) for the principal
type of m. The proof of the theorem is constructive, that is, β can be effectively
computed or shown to be nonexistent, see [
We now give a short introduction into formal concept analysis. A context is a triple (G, M, I), where G, M are sets and I ⊆ G × M. In FCA, the entities in G are thought of as objects, the objects in M as attributes, and for m ∈ M, g ∈ G, we have (g, m) ∈ I if the object g has the attribute m. This is all we need as basic structure to get the machine of FCA going. For A ⊆ G, B ⊆ M, we put A⊲ := {m ∈ M : ∀a ∈ A, (a, m) ∈ I}, and B⊳ := {g ∈ G : ∀m ∈ B, (a, m) ∈ I}. A concept is a pair (A, B) such that A⊲ = B, B⊳ = A. We call A the extent and B the intent. A is the extent of a concept iff A = A⊲⊳, dually for intents. The maps [−]⊲, [−]⊳ are called polar maps. We order concepts by inclusion of extents, that is, (A1, B1) ≤ (A2, B2) ⇔ A1 ⊆ A2.
Definition 3 Given a context B = (G, M, I), we define the concept lattice of B as L(B) = hC, ∧, ∨, ⊤, ⊥i, where ⊤ = (G, G⊲), ⊥= (M⊳, M), and for (Ai, Bi), (Aj, Bj) ∈ C, (Ai, Bi) ∧ (Aj, Bj) = (Ai ∩ Aj, (Bi ∪ Bj)⊳⊲), and (Ai, Bi) ∨ (Aj, Bj) = ((Ai ∪ Aj)⊲⊳, Bi ∩ Bj).
We define our type theoretic context as follows. Recall that Tm(Λ(Σ)) is the set of all λ-terms over Σ. We put Tmc(Λ(Σ)) := {m ∈ Tm(Λ(Σ)) : F V (m) = ∅}, the set of closed terms, and we call Tmc(ΛI(Σ)) the set of all closed λI terms. Furthermore, define WTT as the set of all closed and well-typed terms, that is, the set of all terms m such that ⊢ m : α is derivable for some α by our rules; WTTI = WTT ∩ Tm(ΛI(Σ)). Recall that =αβ is a congruence. Let σ be a given type, and L′ ⊆ kσk be a distinguished subset of the terms of type σ; we define L := {m : ∃n ∈ L′ : m =αβ n}, that is, as closure of L′ under =αβ. Put G = M = Tmc(Λ(Σ)), and define the relation I ⊆ Tmc(Λ(Σ)) × Tmc(Λ(Σ)) as follows: for m, n ∈ Tmc(Λ(Σ)), we have (m, n) ∈ I if nm ∈ L. So the relation of objects in M and G is that of function and argument, and the relation I tells us whether the two yield a desired value. Same can be done with Tmc(ΛI(Σ)).
Obviously, we have ⊥= (∅, Tmc(Λ(Σ))). Regarding upper bounds, we have to distinguish two important concepts: we first have a concept we denote ⊺ := (WTT, ΛV ), where ΛV (V for vacuous) is the set of all terms of the form λx.m, where m ∈ L and x ∈/ F V (m). There is however a larger concept ⊤ ≥ ⊺, which is defined as ⊤ := (Tmc(Λ(Σ)), ∅). The reason for this slight complication is as follows: we want our terms to be closed, because open terms are meaningless for us. Now, it holds that the concatenation of closed terms is again a closed term; but the concatenation of well-typed terms need not be well-typed: for m, n ∈ WTT, it might be that nm ∈/ WTT. Furthermore, there are λ-terms n with vacuous abstraction such that the set {nm : m ∈ ⊺} ⊺; we would however like our ⊤ to be absorbing; and in fact, if m ∈/ WTT, then for any term n, nm, mn ∈/ WTT. So for every term m ∈/ WTT, {m}⊲ = ∅. For all interesting results we have to restrict ourselves to WTT, but for completeness of some operations we have to consider Tmc(Λ(Σ)). Note however that if we restrict Tmc(Λ(Σ)) to Tmc(ΛI(Σ)), then ⊤ and ⊺ coincide.3 3.2
We have seen that each term can be assigned a most general type. Importantly, the same holds for sets of types: 3 This is actually not straightforward, but follows as a corollary from results we present later on. Lemma 4 Let T ⊆ WTT be a set of terms, such that the set of principal types {pt(m) : m ∈ T } is finite. If there is a set of types Θ, such that for each m ∈ T and all θ ∈ Θ, ⊢ m : θ is a derivable judgment, then there is a (up to isomorphism) unique type α, such that for every m ∈ T , ⊢ m : α is derivable, and every θ ∈ Θ can be obtained by α through a type substitution.
α is usually called the most general unifier of Θ; for a set of terms T , we
also directly call it pt(T ), the principal type of T ; for Θ a set of types, we denote
it by W Θ. A proof for this fundamental lemma can be found in [
This is of immediate importance for us, as it allows us both to speak of the principal type of a set of terms, as well as of the least upper bound of a set of types. From there we easily arrive at the greatest lower bound of two types α, β, which we denote by α ∧ β, and which intuitively is the amount of structure which α and β share. Write α ≤ β, if there is a substitution π such that π(α) = β. This is, up to isomorphism, a partial order. We now can simply define α ∧ β := W{γ : γ ≤ α, β}. It is clear that the set {γ : γ ≤ α, β} modulo isomorphism is finite, so the (finite) join exists in virtue of the above lemma. So T p(A) is lattice ordered up to isomorphism.
How does type structure behave wrt. concept structure? First of all, if A ⊆ B, then pt(A) ≤ pt(B). So the inclusion relation reflects type structure. This entails that pt(A) ≤ pt(B⊲⊳). Stronger results are hard to obtain; for example, if we know pt(A), there is nothing we can say in general about an upper bound for pt(A⊲⊳).
Fortunately, there is more we can say about the lattice order of concepts and type order. Define ∨ and ∧ on concepts as usual. For a concept (A, B) over the term context, we put pt1(A, B) = pt(A), pt2(A, B) = pt(B).
Lemma 5 For concepts C1, C2 of the term context, the following holds: (1) If C1 ≤ C2, then pt1(C1) ≤ pt1(C2), and pt2(C2) ≤ pt2(C1). (2) pt1(C1 ∧ C2) ≤ pt1(C1) ∧ pt1(C2), and (3) pt1(C1) ∨ pt1(C2) ≤ pt1(C1 ∨ C2).
Proof. The first claim is immediate by set inclusion. To see the second, consider that for every m ∈ A1 ∩ A2, we must have pt({m}) ≤ pt(A1), pt({m}) ≤ pt(A2) by set inclusion; and so pt({m}) ≤ pt1(C1) ∧ pt1(C2). To see the third claim, consider the following: we can easily show that pt(A1) ∨ pt(A2) = pt(A1 ∪ A2). Then the claim follows from considering that pt(A1 ∪ A2) ≤ pt((A1 ∪ A2)⊲⊳). Definition 6 A term m is a left equalizer, if we have ⊢ m : θ1 → α, ⊢ m : θ2 → α, and θ1 6= θ2. m is a right equalizer, if ⊢ m : α1, ⊢ m : α2, and α1 6= α2.
Easy examples of left equalizers are terms with vacuous abstraction; easy examples of right equalizers are terms which do not contain constants. A term which is both a left and right equalizer is λyx.x. The following results are a bit tedious to obtain, yet not very significant; we therefore omit the proof. Lemma 7 Let T ⊆ WTT, such that pt(T ) = ⊤. Then each m ∈ T ⊲ is a left equalizer.
We can thus also speak of equalizer concepts. If we restrict our context to λI terms, we get a stronger result: Lemma 8 Let m be a left equalizer and λI-term, such that ⊢Σ m : θ1 → α and ⊢Σ m : θ2 → α. Then both θ1, θ2 must be types inhabited by terms in Tm(ΛI(Σ)), that is, there are terms mi, for which ⊢Σ mi : θi is derivable for i ∈ {1, 2} and mi ∈ Tm(ΛI(Σ)).
So when we restrict ourselves to ΛI, we have proper restrictions on the class of possible equalizers, in the general case we do not. For example, assume there is a set T of terms, and pt(T ) 6= ⊤. Still, we might have pt(T ⊲) = ⊤. Conversely, from the fact that pt(T ) = ⊤, it does not follow that T ⊲ = ∅.
Of course, all general results of FCA also hold in this particular setting. For us, the question is not in how far is the type theoretic context interesting as a particular context, but rather: in how far can type theoretic contexts be used in order to generalize existing contexts? As is well-known, type theory is a very powerful tool; we will show this by way of example in formal language theory. 4 4.1
Syntactic concept lattices form a particular case of formal concept lattices. In
linguistics, they have been introduced in [
We now define our first language theoretic context. For L ⊆ T ∗, BC (L) = (T ∗, T ∗ × T ∗, I), where (b, (a, c)) ∈ I iff abc ∈ L. This gives rise to polar maps ⊲ : ℘(T ∗) → ℘(T ∗ × T ∗), and ⊳ : ℘(T ∗ × T ∗) → ℘(T ∗), where 1. for S ⊆ T ∗, S⊲ := {(x, y) : ∀w ∈ S, xwy ∈ L}; and dually 2. for C ⊆ T ∗ × T ∗, C⊳ := {x : ∀(v, w) ∈ C, vxw ∈ L}.
That is, a set of strings is mapped to the set of string contexts, in which all of its elements can occur. For a set of string contexts C, C⊳ can be thought of as an equivalence class with respect to the string contexts in C; but not in general: there might be elements in C⊳ which can occur in a string context (v, w) ∈/ C (and conversely).
Definition 9 A syntactic c-concept A is a pair, consisting of a set of strings, and a set of string contexts, written C = (SC, CC), such that SC⊲ = CC and CC⊳ = SC. The syntactic c-concept lattice of a language L is defined as L(BC (L)) := hCLC , ∧, ∨, ⊤, ⊥i, where CLC is the set of syntactic c-concepts of L, and with all constants and connectors defined in the usual way.
For example, given a language L, we have (ǫ, ǫ)⊳ = L, as all and only the strings in L can occur in L in the string context (ǫ, ǫ); so L is a closed set of strings. We can give the syntactic concept lattice some more structure. We define a monoid structure on concepts as follows: for concepts (S1, C1), (S2, C2), we define: (2)
(S1, C1) ◦ (S2, C2) = ((S1S2)⊲⊳, (S1S2)⊲),
where S1S2 = {xy : x ∈ S1, y ∈ S2}. Obviously, the result is a concept. ′◦′ is
associative on concepts, that is, for X, Y, Z ∈ B, X ◦ (Y ◦ Z) = (X ◦ Y ) ◦ Z
(see [
We define a similar operation • for the string contexts of concepts: (x, y) • (w, z) = (xw, zy). This way, we still have f • (g • h) = (f • g) • h for singleton string contexts f, g, h. The operation can be extended to sets in the natural way, preserving associativity. For example, C • (ǫ, S) = {(x, ay) : (x, y) ∈ C, a ∈ S}. We will use this as follows: Definition 10 Let X = (SX , CX ), Y = (SY , CY ) be concepts. We define the right residual X/Y := ((C1 • (ǫ, SY ))⊳, (C1 • (ǫ, SY ))⊳⊲), and the left residual Y \X := ((C1 • (SY , ǫ))⊳, (C1 • (SY , ǫ))⊳⊲).
For the closed sets of strings S, T , define S/T := {w : for all v ∈ T, wv ∈ S}. We then have SX /SY = SX/Y . So residuals are unique and satisfy the following lemma: Lemma 11 For X, Y, Z ∈ CLC , we have Y ≤ X\Z iff X ◦ Y ≤ Z iff X ≤ Z/Y .
For a proof, see [
Syntactic c-concepts form a very well-behaved structure, which even forms a
complete class of models for the Full Lambek calculus, an important substructural
logic (see [
As a second example, consider L3 := {a2n : n ∈ N}. Here we have the following problem: for each n ∈ N, an will have a distinguishing string context. Nonetheless, there is a very simple pattern in the language: taking a word of L3, we just have to concatenate it with itself, and we get a new word in L3. In our analysis, however, there are no concepts C1, C2, such that C1 ◦ (L3, L3⊲) ◦ C2 = (L3, L3⊲). So our concepts are uninformative on the pattern of this language. What we want to have in this case is a concept of duplication. We will remedy these shortcomings in what is to follow; we will need, however, some type-theoretic background. 5
The following, type theoretic encoding of language theoretic entities has been
developed in the framework on on abstract categorial grammars (introduced
in [
T signature. The term is linear and written as /a1 . . . an/ := λx.a1(. . . (anx) . . . ). Obviously, the variable x has to be type o, in order to make the term typable. We then have, for every string w ∈ T ∗, ⊢ΣTstring /w/ : o → o.
Under this representation, string concatenation is not entirely trivial, and cannot be done by juxtaposition, as the result would not be typable. We can concatenate strings by the combinator B := λxyz.x(yz), which concatenates its first argument to the left of its second argument, as can be easily checked.6 We can also represent tuples of strings by terms. Let /w1/, . . . , /wn/ represent strings. Then a tuple of these strings is written as /(w1, . . . , wn)/ := λx.((. . . (x/w1/) . . . )/wn/). The type of x here depends on the size of the tuple. We define α →n β by α →0 β = β, α →n+1 β = α → (α →n β). In general, for a term m encoding an n-tuple , we have ⊢ΣTstring m : ((o → o) →n (α))) → α. So the types get larger with the size of tuples; the order of the term however remains invariantly 2.
We indicate how to manipulate tuple components separately. The
function which concatenates the tuple components in their order is obtained as
6 See [
However, the general componentwise concatenation of tuples of arbitrary size (considering strings as 1-tuples) cannot be effected by a typed λ-term. The reason is: if we do not fix an upper bound on tuple size, the types of tuples get higher and higher, and there is no finite upper bound. So there is no finite term which could have the appropriate type.7 This means that in this setting, we must refrain from a notion of general concatenation of any type. This will however do little harm, as we will see. 6
Take a finite alphabet T , and fix a language L1 ⊆ T ∗. As we have seen in the last section, there is a bi-unique mapping i : T ∗ → WTT between strings in T ∗ and λ-terms of the signature Σstring. Note that i is properly bi-unique and not
T up to =αβ equivalence; we map strings only onto their standard encoding, using a standard variable. We thus obtain i[L1] ⊆ WTT, where i[−] is the pointwise extension of i to sets. We close i[L1] under =αβ, and obtain L := {m : there is n ∈ i[L] : n =αβ m}. This is the language we are working with, the type theoretic counterpart of L1. In the sequel, for any M ⊆ T ∗, we will denote the closure of i[M ] under =αβ by M λ; so we have L = (L1)λ.
We now define a context BT (L) = (G, M, I), where G = M = Tmc(Λ(ΣTstring)), that is the set of closed terms over the signature Σstring; and for m, n ∈ T Tmc(Λ(Σstring)), we have (m, n) ∈ I iff nm ∈ L. So for S a set of terms, we
T have S⊲ := {t : ∀s ∈ S : ts ∈ L}, and S⊳ := {t : ∀s ∈ S : st ∈ L}.
Definition 12 A t-concept is a concept (S, T ) over the context BT (L), where S = T ⊳, T = S⊲. The syntactic t-concept lattice of a language L is defined as LT (L) := L(BT (L)) = hCTL, ∧, ∨, ⊤, ⊥i, where CTL is the set of syntactic t-concepts of L, and with all constants and connectors defined in the usual way.
What we are still missing is an operator which allows us to define fusion and residuation. Recall that for terms, our primitive objects, juxtaposition is interpreted as function application. We extend this interpretation to sets of terms: for S1, S2 ⊆ Tmc(Λ(Σstring)), we define S1S2 := {mn : m ∈ S, n ∈ T }. Next, for t
T concepts (S1, T1), (S2, T2), we simply put (S1, T1)◦(S2, T2) := ((S1S2)⊲⊳, (S1S2)⊲). 7 On the other side, once we fix an upper bound k to tuple size, it is easy to see how to define ◦ as λ term: for i ≤ k, we simply encode all tuples as k-tuples with all jth components, i < j, containing the empty string. Then ◦ is simply componentwise concatenation of k-tuples, which is λ-definable, as we have seen. That is, as before we use the closure of concatenation of extents to define ◦. But there is an important restriction: concatenation of terms is not associative. Consequently, the operation ◦ is not associative on concepts, we have, for concepts M, N, O ∈ CTL, (M ◦ N ) ◦ O 6= M ◦ (N ◦ O). For example, M ◦ N might be ⊤, because M N contains a term mn ∈/ WTT, and consequently we have ⊤ ◦ O = ⊤. Still, M ◦ (N ◦ O) might be well-typed. So the structure of (B, ◦) is not a monoid, but rather a groupoid. We furthermore have a left identity element 1l, such that for every concept S, 1l ◦ S = S. This is the concept of the identity function ({λx.x}⊲⊳, {λx.x}⊲). (By the way, the identity function is also the encoding of the empty string /ǫ/). There is no general right identity, though: for assume we have a term m : α for a constant atomic type α; then there is no term n such that mn can be typed. Consequently, no n can be the right identity for m.
What are the residuals in this structure? Given the fusion operator, they are already implicitly defined by the law of residuation O ≤ M/N ⇔ O ◦ N ≤ M ⇔ N ≤ O\M ; what we have to show that they exist and are unique. In the sequel we will use residuals both on sets of terms and on concepts; this can be done without any harm, as the extent order and the concept order are isomorphic. To see more clearly what residuation means in our context, note that for S ⊆ Tmc(Λ(Σstring)), T we have S⊲ := L/S; because S⊲ is the set of all terms m, such that for all n ∈ S, mn ∈ L. Dually, we have S⊳ := S\L. Consequently, we have S⊲⊳ = (L/S)\L, and dually, we get S⊳⊲ = L/(S\L). So we see that the polar maps of our Galois connection form a particular case of the residuals, or conversely, the residuals form a generalization of the polar maps. The closure operators are equivalent to a particular case of what is known as type raising. More generally, we can explicitly define residuals over a ternary relation: put (m, n, o) ∈ R if and only if mn =αβ o. Then we define 1. O/N := {m : ∀n ∈ N, ∃o ∈ O : (m, n, o) ∈ R}; dually: 2. M \O := {n : ∀m ∈ M, ∃o ∈ O : (m, n, o) ∈ R}.
As is easy to see, M ⊲ := {n : ∀m ∈ M, ∃o ∈ L : (m, n, o) ∈ R}; and M ⊳ := {n : ∀m ∈ M, ∃o ∈ L : (m, n, o) ∈ R}. This way, we explicitly define residuals for sets of terms. Given this, it easily follows that residuals also exist and are unique for concepts: (S1, T1)/(S2, T2) = ((S1/S2), (S1/S2)⊲).
So residuals allow us to form the closure not only with respect to L, but with respect to any other concept. This provides us with a much more finegrained access to the hierarchical structure of languages. On the negative side, the ◦ operation and residuals do not tell us anything about directionality of concatenation on the string level. This however is unsurprising, as our treatment of strings as λ-terms serves precisely the purpose of abstracting away from this: concatenation is done by terms automatically, and we need no longer care for this. Obviously t-concepts provide a vast generalization of c-concepts. An immediate question is whether this extension is conservative, in the sense that each c-closed set is also t-closed. This is generally wrong, but holds with some restrictions: Theorem 13 Let M, L ⊆ T ∗; let M λ, Lλ be their type theoretic counterpart in the signature Σstring. If M = M ⊲⊳ is closed wrt. the language theoretic context
T BC (L), then we have M λ = (M λ)⊲⊳ ∩ (T ∗)λ, where (M λ)⊲⊳ is closed wrt. the type theoretic context BT (Lλ).
Proof. Let M be c-closed; every string context (w, v) ∈ M ⊲ corresponds to a function of the form λx.B(B/w/x)/v/, which takes a term /u/ as argument, concatenating it with a /w/ to its left and /v/ to its right, resulting in a term /wuv/. Call the set of these functions (M λ ◮ ) . We now take (M λ)◮⊳. Obviously we have M λ ⊆ (M λ)◮⊳. We show that M λ ⊇ (M λ)◮⊳ ∩ (T ∗)λ: if we have, for w ∈ T ∗, w ∈/ M , but /w/ ∈ (M λ)◮⊳ ∩ (T ∗)λ, then we have i−1(/w/) ∈ M ⊲⊳, because each type context in (M λ)◮ corresponds to a string context in M ⊲. This is a contradiction, as M is closed under [−]⊲⊳.
So we have M λ = (M λ)◮⊳∩(T ∗)λ, and (M λ)◮⊳ is a closed set. Furthermore, as (M λ)◮ ⊆ (M λ)⊲, we have (by the laws of Galois connections) (M λ)◮⊳ ⊇ (M λ)⊲⊳. So we get M λ ⊇ (M λ)⊲⊳ ∩ (T ∗)λ. To see that M λ ⊆ (M λ)⊲⊳ ∩ (T ∗)λ, consider that as M ⊆ T ∗, we have M λ ⊆ (T ∗)λ; furthermore, M λ ⊆ (M λ)⊲⊳. Therefore, M λ ⊆ (M λ)⊲⊳ ∩ (T ∗)λ. This completes the proof.
As expected, the converse does not hold, not even for terms which encode strings. In this sense t-concepts yield a proper generalization of c-concepts. This however does not obtain for the extension of the lattice with fusion and residuals: fusion in the t-concept lattice is completely incomparable to fusion in the c-concept lattice of a language. 7
One main objection to our type theoretic approach to language might be that we produce many concepts to which we might not be able to assign any intuitive meaning, and which tell us very little about the language in question. We easily see what is meant by the concept of a term /w/ in a language L. We can also make perfectly sense of the concept duplication. It is less easy to see what is meant by the concept of the term B, which we discussed above. What can the the distribution of such a concept in a language tell us about the language?8 So we do not have a problem with the formalism in the first place, but with its interpretation.
Therefore, it might be reasonable to restrict our approach. We propose here two main restrictions: First, as we already mentioned, we might restrict the universe of terms Tmc(Λ(Σstring)) to λI terms. A language-theoretic argument
T for this point is that we are interested in the distributional structure of languages. Vacuous abstraction, as yielding constant functions, allows us to delete arguments or certain parts thereof. This seems to us an “unlinguistic” procedure, as we cannot say we talk about the distribution of an object if we allow to delete parts of it. A further restriction to linear λ-terms, on the other side, does not 8 What is less unclear is its meaning as intent rather than extent: apart from some additional technical difficulties, it must take two arguments which, when concatenated, give a term in L. seem to be desirable, as then we get the same problems with our toy language {a2n : n ∈ N} as before.
A second restriction which might be reasonable is the restriction of type order. As we have seen, types of second order allow us to yield all strings and tuples of strings. If we restrict only G to second order types, we will have all functions from second order types to second order types in M. This seems to us a very reasonable restriction, the consequence of which we cannot discuss here for reasons of space.
In conclusion, there are many options in further pursuing our approach, and at this point it is unclear which direction is the most promising. But in either way our approach might provide some contribution to the old problem of learning infinite languages from the distributional structure of a finite fragment thereof.