ALTLab will be hosting Dr. Måns Huldén from the Department of Linguistics in the University of Colorado, who will be delivering a presentation in the Linguistics Colloquium on Friday entitled Formal verification in phonology.
Abstract: Constructing linguistic models is a complex task, and one of the main roles of computational linguistics is to aid the linguist in performing that task. In this talk I will focus on some advanced recent techniques that provide useful theory-neutral mechanisms for analyzing and developing phonological generalizations in various contexts. These techniques draw on finite state technology, which is widely used for modeling phonological and morphological phenomena computationally and also finds many applications in speech technology. The popularity of finite state machines – automata and transducers – rests on a few main attributes: they provide a theory-neutral platform for encoding linguistic generalizations, they are inherently bidirectional (a model defined in the direction of generation can also perform parsing), they can accommodate gradience effects and probabilistic generalizations, and they enjoy substantial practical support in the form of software and development tools. For our purposes, the most important feature is the set of computational methods available for formal verification and investigation of finite state models. One technique particularly useful to the linguist is equivalence testing of grammars. While testing the equivalence of finite transducers is computationally undecidable in the general case, I show that efficient methods exists for doing so in the case of linguistically interesting contexts. When combined with techniques to model richer phonological structures such as autosegments or constraint-driven formalisms like Optimality Theory, such equivalence testing permits the automation of various difficult tasks in phonology. Among other things, it enables one to formally ascertain the correctness of generalizations expressed in a particular formalism, investigate competing theories of historical-comparative reconstruction, and perform more general comparisons of phonological and morphological models.