Safe recursion with higher types and BCK-algebra Original Research Article

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 View the MathML source 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.