Formal languages and lambda-calculus
- Speaker: Dr Sylvain Sylvati (INRIA)
- Host: Ian Pratt-Hartmann
- 7th October 2009 at 14:15 in Lecture Theatre 1.4, Kilburn Building
In this talk I will introduce a notion of recognizability for the simply typed lambda-calculus that extends the well-known notions of recognizability for trees and strings. The definition of this notion originates in the algebraic characterizations of recognizability, and I will give an automata-like presentation of it in terms of typing. Then I will explain how the usual closure properties of recognizable sets can be proved for recognizable sets of lambda-terms. I will then turn to some applications of this notion of recognizability to computational linguistic, formal language theory and logic. Concerning computational linguistics, I will show that the usual interface between syntax and semantics for natural languages as defined by Montague and Gallin leads to a decidable generation problem; i.e., given a representation of some meaning and a Montagovian grammar, it is possible to construct every sentences having this meaning representation according to the grammar. A closely related result about context free grammars of lambda-terms, the closure under intersection with recognizable sets, can be easily proved with similar techniques. Finally, I will show how this technique can prove in a simple manner that fourth order matching is decidable, higher order matching being a problem related to theorem instantiation in proof assistant.