[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi Benjamin, Categorial grammars are defined via the Lambek Calculus, which is an intuitionistic substructural logic. They generate the same languages as 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 precisely. 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 <http://reports-archive.adm.cs.cmu.edu/anon/2001/CMU-CS-01-152.pdf>. Rowan Davies. Practical Refinement-Type Checking. PhD Thesis, Carnegie Mellon University, May 2005. Available as Technical Report CMU-CS-05-110 <http://reports-archive.adm.cs.cmu.edu/anon/2005/CMU-CS-05-110.pdf>. On Thu, Dec 18, 2014 at 11:22 AM, Benjamin C. Pierce <[email protected] > 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 http://www.cs.cmu.edu/~fp +1 412 268-6343 GHC 7019
