The power of non-determinism in higher-order implicit complexity: characterising complexity classes using non-deterministic cons-free programming

TY - GEN

T1 - The power of non-determinism in higher-order implicit complexity

T2 - 26th European Symposium on Programming

AU - Kop, Cynthia Louisa Martina

AU - Simonsen, Jakob Grue

N1 - Conference code: 26

PY - 2017

Y1 - 2017

N2 - 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 consfree 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.

AB - 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 consfree 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.

KW - Cons-free programming

KW - EXPTIME hierarchy

KW - Implicit computational complexity

KW - Non-deterministic programming

KW - Unitary variables

UR - http://www.scopus.com/inward/record.url?scp=85018691937&partnerID=8YFLogxK

U2 - 10.1007/978-3-662-54434-1_25

DO - 10.1007/978-3-662-54434-1_25

M3 - Article in proceedings

AN - SCOPUS:85018691937

SN - 978-3-662-54433-4

T3 - Lecture notes in computer science

SP - 668

EP - 695

BT - Programming Languages and Systems

A2 - Yang, Hongseok

PB - Springer

Y2 - 22 April 2017 through 29 April 2017

ER -