[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
In The safe lambda-calculus, Blum and Ong, 2009 http://arxiv.org/abs/0901.2399 a restriction of the simply-typed lambda calculus is presented as an adaptation of an existing restriction on *higher-order* grammars. The corresponding subset of lambda-calculus has the interesting property that one can define reduction without having to take care of variable capture at all -- it can be ruled out statically thanks to the order restriction. On Thu, Dec 18, 2014 at 5:22 PM, Benjamin C. Pierce <bcpie...@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
