Language and Thought

The tongue gives voice, the mind begins to shape,

What unseen bridge connects these realms so near?

From inner spark to uttered verbal scape,

Through patterns spun before the words appear.

We strive to know how concepts first ignite

And find their form in language's design;

What hidden structures grant a thought its might?

What grammar deep does human sense define?

This subtle dance lets understanding bloom,

As mind constructs the world it comes to hold.

Through chosen words we banish mental gloom,

Or weave the very narratives we're told.

This mystery invites the keen pursuit:

To map the space where word and reason root.

- Yifan Zhang, IIIS, Tsinghua Univ.

Our research investigates the fundamental principles governing the relationship between language and thought.

Categorical Framework of Language Semantics

A significant approach within formal semantics utilizes frameworks derived from category theory, notably pioneered by Joachim Lambek. Lambek's categorial grammars, particularly the Lambek Calculus (LC), provide a mathematically precise way to model the syntax-semantics interface.

In LC, syntactic categories (types) are assigned to words. We start with a set of basic types, typically \( n \) (for noun or noun phrase) and \( s \) (for sentence). Complex types are built using binary connectives:

  • \( A / B \) (over): A category that seeks a category \( B \) to its right to form category \( A \).
  • \( B \backslash A \) (under): A category that seeks a category \( B \) to its left to form category \( A \).
  • \( A \bullet B \) (product): Represents a sequence of \( A \) followed by \( B \) (less commonly used in basic parsing).

Words in the lexicon are assigned one or more types. For example:

  • John :: \( n \)
  • walks :: \( n \backslash s \) (an intransitive verb: needs a noun \(n\) to its left to form a sentence \(s\))
  • likes :: \( (n \backslash s) / n \) (a transitive verb: needs a noun \(n\) to its right to form \(n \backslash s\), which then needs a noun \(n\) to its left to form \(s\))
  • the :: \( n / n \) (a determiner: needs a common noun \(n\) to its right to form a noun phrase \(n\))

Grammaticality is determined by provability within a sequent calculus. A sequent is an expression of the form \( \Gamma \vdash A \), where \( \Gamma \) is a sequence of types \( C_1, \dots, C_k \) and \( A \) is a type. This asserts that the sequence of types \( \Gamma \) can combine to form the type \( A \). Determining if a sequence of words forms a sentence corresponds to proving a sequent like \( \text{type}_1, \dots, \text{type}_k \vdash s \).

The core of the calculus lies in its inference rules. The application rules (corresponding to function application) are fundamental for parsing:
Forward Application (\( /L \)): \[ \frac{\Gamma \vdash B \quad \Delta, A, \Theta \vdash C} {\Delta, \Gamma, A / B, \Theta \vdash C} \] This rule states that if \( \Gamma \) yields a \( B \), and \( A/B \) occurs immediately to the right of \( \Gamma \) in a sequence that yields \( C \), then the \( A/B \) consumes the \( B \) derived from \( \Gamma \), leaving an \( A \) in its place within the sequence.
Backward Application (\( \backslash L \)): \[ \frac{\Gamma \vdash B \quad \Delta, A, \Theta \vdash C} {\Delta, B \backslash A, \Gamma, \Theta \vdash C} \] This rule states that if \( \Gamma \) yields a \( B \), and \( B \backslash A \) occurs immediately to the left of \( \Gamma \) in a sequence that yields \( C \), then the \( B \backslash A \) consumes the \( B \) derived from \( \Gamma \), leaving an \( A \) in its place.

For instance, to parse "John walks", we assign types \( n \) and \( n \backslash s \) respectively. We want to prove the sequent \( n, n \backslash s \vdash s \). Using the Backward Application rule (\( \backslash L \)), we can see this holds: \[ \frac{ n \vdash n \quad s \vdash s } { n, n \backslash s \vdash s } (\backslash L) \] (Here, \( \Gamma = n \), \( B = n \), \( A = s \), \( \Delta \) and \( \Theta \) are empty sequences, and \( C = s \). The premise \( s \vdash s \) is an axiom \(A \vdash A\)).

This framework implements a principle of strict type-driven compositionality. The syntactic derivation (proof in the calculus) directly corresponds to the semantic composition, often linked via the Curry-Howard isomorphism to lambda calculus terms representing meanings. This provides a robust foundation for analyzing the syntax-semantics interface and has influenced research areas demanding precise meaning representations.