An Elementary Fragment of Second-Order Lambda Calculus
计算机科学中的逻辑
2007-05-23 v3
摘要
A fragment of second-order lambda calculus (System F) is defined that characterizes the elementary recursive functions. Type quantification is restricted to be non-interleaved and stratified, i.e., the types are assigned levels, and a quantified variable can only be instantiated by a type of smaller level, with a slightly liberalized treatment of the level zero.
引用
@article{arxiv.cs/0210022,
title = {An Elementary Fragment of Second-Order Lambda Calculus},
author = {Klaus Aehlig and Jan Johannsen},
journal= {arXiv preprint arXiv:cs/0210022},
year = {2007}
}
备注
16 pages; corrections