Abstract

In previous work the author has introduced a lambda calculus SLR with modal and linear types which serves as an extension of Bellantoni–Cook's function algebra BC to higher types. It is a step towards a functional programming language in which all programs run in polynomial time. In this paper we develop a semantics of SLR using BCK -algebras consisting of certain polynomial-time algorithms. It will follow from this semantics that safe recursion with arbitrary result type built up from N and ⊸ as well as recursion over trees and other data structures remains within polynomial time. In its original formulation SLR supported only natural numbers and recursion on notation with first-order functional result type