1

The question by curiousdannii and the extensive answer by lemontree here address the basic workings, advantages, and disadvantages of type theory. I have a related question in this area. As I understand type theory and as described by lemontree, type theory necessarily construes syntactic structures as being generated in terms of one input and one output. This suggests that the syntactic structures generated necessitate binary branching; ternary branching does not seem possible, at least not in the illustrations of type theory that I have encountered.

My question in this regard concerns the potential that this aspect of type theory can be chalked up to the disadvantages. For me, there is substantial empirical evidence in favor of n-ary branching in syntactic structures. If type theory is incompatible with this evidence, then what good is it? It results in a semantics that is incompatible with the syntax.

If there are versions of type theory that are compatible with n-ary branching, then what are they, and how widespread and accepted are those versions?

Improve this question
9
  • I can only speak as a computer scientist here, but you can always just extend the simply typed lambda calculus with a family of product types (such that for all x1 : t1, ..., xn : tn, prod(x1, ..., xn) : t1 * ... * tn, plus projections pi_n_i : (t1 * ... * tn) -> ti).
    – phipsgabler
    Apr 30, 2020 at 9:20
  • Oh, and have you heard about currying?
    – phipsgabler
    Apr 30, 2020 at 9:22
  • @phipsgabler Product types won’t help here because they’re ordered (otherwise there would be no isomorphism in the first place). In CS parlance, semanticists use associative arrays which give them named arguments. This is what’s used in LFG and other formalisms based on feature structures (AVMs), as explained in the answer below.
    – Atamiri
    Apr 30, 2020 at 9:59
  • Hm. I'd really like to sit together with a couple of these semanticists once and query from them what they actually mean in terms of concepts I can think in... for now it seems I don't even know how to start asking what I misunderstand :)
    – phipsgabler
    Apr 30, 2020 at 14:46
  • 1
    @phipsgabler You might want to read the original papers on Montague’s grammar (the wiki page has references). Then I’d recommend looking at glue semantics which combines λ-calculus and linear logic (and syntactic structures based on dependencies), there are a few good papers by Mary Dalrymple et al.
    – Atamiri
    Apr 30, 2020 at 15:50

3 Answers 3

Reset to default
2

Church's original formulation of type theory (based on λ-calculus) suggests binary branching. One way of dealing with this limitation is the use of linear logic, whose connective for tensor conjunction makes it possible to swap the arguments of linear implication. This is used in LFG, mainly because f-structures are isomorphic to dependency structures so the logical representations can be directly derived from them.

Yet another alternative is the formalism developed by Jerry Hobbs, who uses FOL with reification. His theory focuses on the level of pragmatics but he also has a syntactic component based on HPSG that meshes well with his logical forms. His theory is remarkable in that it is tractable using a technique of mathematical optimisation originally developed within operational research (and from a psycholinguistic perspective it's based on how the human mind works but that's another story).

P.S. I know both formalisms inside out so any detailed questions are welcome.

As as side note, type theory has nothing to do with branching so the question, as it's worded now, doesn't make sense. However (the original formulation of) type theory is based on λ-calculus which is incompatible with ternary branching so my answer addresses this discrepancy.

Improve this answer
9
  • Thanks for the answer. There is much I do not understand in what you write. Could you perhaps provide an example, for instance, an illustration of a logical structure of LFG and how it is isomorphic to an n-ary structure.
    – Tim Osborne
    Apr 30, 2020 at 7:53
  • @TimOsborne If you take an exocentric structure for “students read books” in Russian, which is simply S:[NP V NP], the link to glue semantics is via the f-structure: [PRED read, SUBJ [“students”], OBJ [“books”]]. In glue semantics the corresponding rule would be λX.λY.read(X,Y):(↑SUBJ)σ ⊸ (↑OBJ)σ ⊸ ↑σ. So they just use f-structures and linear implication to work around the limitation of λ-calculus. Note that the arity of the root node of the phrase structure is irrelevant. This method would work for any dep. formalism. Hobbs’ approach is much more flexible but this is how it works in LFG.
    – Atamiri
    Apr 30, 2020 at 8:47
  • @TimOsborne I've added a note on the wording of the question, I hope I deciphered it correctly. In any case any additional questions are welcome.
    – Atamiri
    Apr 30, 2020 at 10:11
  • Even in the lambda-calculus, the branching is not solely binary. The lambda-calculus has two operators: application (which is binary, as you point out), and abstraction (which is a binding unary operator). This means the trees terms form are not binary trees (and in fact have to be represented more sophisticatedly using structures like graphs with binding). I would also object to reducing "type theory" to the lambda-calculus, which is an extremely primitive notion and unlikely to very practical for linguistic purposes.
    – varkor
    Apr 30, 2020 at 11:21
  • @varkor It’s about branching in phrase structure trees. The λ-calculus is used in formal semantics and it’s actually very powerful.
    – Atamiri
    Apr 30, 2020 at 11:30
1

My answer is no, not n-ary branching, but rather binary branching. As Atamiri's answer might suggest, the basic notion of type theory is that of a function -- the types are just means to that end. If grammar is functional, complex expressions are built up by applying functions to arguments to obtain the values of functions at those arguments. Two things, function and argument, combine to form a third thing: the (single) value. That's binary branching.

One could, I suppose, allow grammatical functions to have more than one argument, but type theory seems to assume just one argument, and that's enough for me.

I have a way of introducing one-place functions into CFG (Context Free Grammar) which avoids the artificiality of type theory and introduces no additional computational complexity into grammar, but I'm afraid it's rather long-winded, and I'm not sure anyone would be interested.

Improve this answer
9
  • I’d be interested ;) BTW I don’t think type theory is artificial (at least not more artificial than CFG or DG or any other formalism used in linguistics).
    – Atamiri
    Apr 30, 2020 at 10:32
  • @Atamiri, Then please ask an appropriate question. I can't write about it here, because it is not a type theory, so it would not be responsive to the question.
    – Greg Lee
    Apr 30, 2020 at 10:38
  • Done. I’m all ears.
    – Atamiri
    Apr 30, 2020 at 11:06
  • Type theories are not just about operators (what you call functions). Considering operators alone ignores much of the other important structure: typing, variable binding, equations or reductions, polymorphism, dependency and so on. Likewise, the types are an intrinsic part of the structure: without them, you're simply talking about universal algebra.
    – varkor
    Apr 30, 2020 at 11:17
  • 1
    @varkor, Then why does a type, such as <e t>, have at most two parts?
    – Greg Lee
    Apr 30, 2020 at 12:45
1

As I understand type theory and as described by lemontree, type theory necessarily construes syntactic structures as being generated in terms of one input and one output.

This is a misunderstanding. "Type theory" refers to a very general class of structures. Loosely, operators in type theory may be thought of as "n-ary functions". That is, they may take a fixed number of inputs and return a single output. The terms in a type theory thus have a tree structure. They are not limited to binary branching.

An example of a binary operator is app : Fun(A, B) x B -> B, which takes a term of type Fun(A, B) and a term of type B and returns a term of type B. An example of a ternay operator is if : Bool x A x A -> A, which takes a truth value, and two cases of the same type, and returns a term of the same type A. There are many examples of operators with different arities.

One confusion may be that there are many structures computer scientists classify as "type theories". The simply-typed lambda-calculus is a canonical example, but by no means the only one. (Though, even the simply-typed lambda-calculus has non-binary operators!)

If there are versions of type theory that are compatible with n-ary branching, then what are they, and how widespread and accepted are those versions?

Most type theories have operators with a range of arities. Common theories include the simply-typed lambda-calculus, System F, Martin-Löf Type Theory, and others. All the type theories listed here are examples.

Possibly the most helpful way of thinking about the structure of terms in a type theory is as "structured trees with binding". Each term has a (n-ary branching) tree structure, but the form of the tree is restricted to those that are well-formed according to the rules of the type theory. Additionally, some vertices of the tree are "variables", which link back to a branch that binds them. I would recommend taking a look at a standard text book on Type theory, which will help give you an idea of the sort of structure that appears. Types and Programming Languages is often one that is recommended for newcomers.

Improve this answer
6
  • I think the question is about branching in phrase structures.
    – Atamiri
    Apr 30, 2020 at 11:25
  • @Atamiri: I accept that I may have approached this at the wrong angle, but it still appears to me that the branching of phase structures is related to the branching factor of term trees in a type theory. If you want to use type theory to represent n-ary phase structures, then it certainly seems like you could make use a type theory with n-ary operators. Perhaps I am misunderstanding, though?
    – varkor
    Apr 30, 2020 at 11:51
  • I don’t think it’s related, if only for the fact that it’s language-specific in CFG. That said, it’s related at the level of dependencies (dep. trees vs terms), but dependency trees have no constraints on arity. Maybe that’s what you meant.
    – Atamiri
    Apr 30, 2020 at 12:23
  • I was thinking of representing the phase structure structure (of a given language) via the terms of a type theory (in which case, as I understand it, the given language would determine the arities of the branches, though some may be variadic). If you want to represent arbitrary languages using a single type theory, you would need to encode the structure of a grammar somehow, though then the branching factor is irrelevant.
    – varkor
    Apr 30, 2020 at 12:48
  • 1
    @varkor Thanks for your answer. I of course believe that many versions of type theory are compatible with n-ary branching. I should have qualified my question, though, so that it focuses on versions of type theory that are actually used by syntacticians as they try to establish a one-to-one matching of semantic units to syntactic constituents. There seem to be few instances of linguists actually doing this. Binary branching everywhere is what one encounters instead. For that reason, I have always seen little value in type theory for natural language syntax.
    – Tim Osborne
    May 1, 2020 at 2:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.