寻找类型系统的两种算法
计算机科学中的逻辑
2008-04-18 v2 编程语言
摘要
作者的 ATR 编程形式主义是在复杂度理论驱动的类型系统下的按值调用 PCF 版本。ATR 程序在 2 型多项式时间内运行，且所有标准的 2 型基本可行泛函均可由 ATR 定义（ATR 类型局限于 0、1 和 2 层）。原始 ATR 版本的一个局限性是仅能直接表达尾递归。在此，我们扩展了 ATR，使其能够直接表达广泛的仿射递归。特别是，修订后的 ATR 能够相当自然地表达经典的插入排序和选择排序算法，从而克服了大多数先前基于隐式复杂度的形式主义的瓶颈。本文的主要工作在于完善 ATR 的原始时间复杂度语义，以证明这些新的递归方案不会超出可行性的范畴。
引用
@article{arxiv.0710.0824,
title = {Two algorithms in search of a type system},
author = {Norman Danner and James S. Royer},
journal= {arXiv preprint arXiv:0710.0824},
year = {2008}
}
评论
30 pages. Final version to appear in Theory of Computing Systems