The Power of Non-Determinism in Higher-Order Implicit Complexity

TL;DR

This paper explores how non-determinism enhances the computational power of higher-order cons-free functional programs, enabling them to characterize all elementary-time decidable sets, unlike the limited case at data order 0.

Contribution

It demonstrates that non-determinism increases expressivity in higher-order cons-free programs, allowing characterization of elementary-time decidable sets, and shows how to restore hierarchy with restrictions.

Findings

Non-determinism does not increase expressivity at data order 0.

At data order ≥1, non-determinism characterizes elementary-time decidable sets.

Restrictions can restore the original hierarchy of characterizations.

Abstract

We investigate the power of non-determinism in purely functional programming languages with higher-order types. Specifically, we consider cons-free programs of varying data orders, equipped with explicit non-deterministic choice. Cons-freeness roughly means that data constructors cannot occur in function bodies and all manipulation of storage space thus has to happen indirectly using the call stack. While cons-free programs have previously been used by several authors to characterise complexity classes, the work on non-deterministic programs has almost exclusively considered programs of data order 0. Previous work has shown that adding explicit non-determinism to cons-free programs taking data of order 0 does not increase expressivity; we prove that this - dramatically - is not the case for higher data orders: adding non-determinism to programs with data order at least 1 allows for a characterisation of the entire class of elementary-time decidable sets. Finally we show how, even with non-deterministic choice, the original hierarchy of characterisations is restored by imposing different restrictions.