[TYPES] FP and the Chomsky hierarchy

Frank Pfenning fp at cs.cmu.edu
Thu Dec 18 21:29:59 EST 2014

Hi Benjamin,

Categorial grammars are defined via the Lambek Calculus, which
is an intuitionistic substructural logic.  They generate the same languages
context-free grammars.  A proof term assignment to the Lambek
Calculus yields a type system for a lambda-calculus with interesting
properties which is coherent with linear and intuitionistic logic.  See
[Polakow01] which also includes some interesting applications.
Dependent ordered types allow one to model a strong form of
context-sensitivity.  Regular grammars are a natural sublanguage,
although I don't know of a reference where this has been characterized

Another connection is by looking at type systems.  For example,
regular tree grammars are the foundations of datasort refinements
of functional languages [Davies05], which originated much earlier
in the logic programming community.  You probably know better than
me the extensions to type languages for XML schemas, which come
in some ways closer to classes of string languages rather than tree
languages.  Unfortunately, when you try to generalize to context-free
grammars, too many basic questions about typing become undecidable.

Jeff Polakow.  Ordered Linear Logic and Applications.  PhD Thesis,
Carnegie Mellon University, August 2001.  Available as Technical
Report CMU-CS-01-152

Rowan Davies.  Practical Refinement-Type Checking.  PhD Thesis,
Carnegie Mellon University, May 2005.  Available as Technical
Report CMU-CS-05-110

On Thu, Dec 18, 2014 at 11:22 AM, Benjamin C. Pierce <bcpierce at cis.upenn.edu
> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
> A colleague asked me an interesting question recently:
> Can the Chomsky hierarchy (regular grammars, context-free,
> context-sensitive, Turing-complete) be phrased in terms that functional
> programmers would find natural, e.g. in terms of typed or syntactically
> restricted lambda-calculi?
> Pointers appreciated...
>      - Benjamin

Frank Pfenning, Professor and Head
Department of Computer Science
Carnegie Mellon University
Pittsburgh, PA 15213-3891

+1 412 268-6343
GHC 7019

More information about the Types-list mailing list