[TYPES] FP and the Chomsky hierarchy

[Frank Pfenning]

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 <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

http://www.cs.cmu.edu/~fp
+1 412 268-6343
GHC 7019