On the building of affine retractions

摘要

A simple type σ is retractable to a simple type x if there are two terms C~(σ→τ) and D~(τ→σ) such that D ο C =β_η λx.x. The retractability of types is affine if the terms C and D are affine, that is, when every bound variable occurs in them at most once in the scope of its declaration. This paper presents a system that derives affine retractability for simple types. It also studies the complexity of constructing these affine retractions. The problem of affine retractability is NP-complete even for the class of types over a single type atom and having limited functional order. In addition, a polynomial algorithm for types of orders less than three is presented.