Our seminar series is free and available for anyone to attend. Unless otherwise stated, seminars take place on Wednesday afternoons at 2pm in the Kilburn Building during teaching season.

If you wish to propose a seminar speaker please contact Antoniu Pop.


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.
▲ Up to the top