This paper is a pre-print of the paper The Power of Non-Determinism in Higher-Order Implicit Complexity which has been accepted for publication at the European Symposium for Programming (ESOP 2017). The text is (almost) identical to the published version, but the presentworkincludesanappendixcontainingfullproofsofalltheresults in the paper. 7 1 0 2 n a J 0 3 ] C C . s c [ 2 v 2 8 3 5 0 . 1 0 7 1 : v i X r a The Power of Non-Determinism in Higher-Order Implicit Complexity (cid:63) Characterising Complexity Classes using Non-deterministic Cons-free Programming Cynthia Kop and Jakob Grue Simonsen Department of Computer Science, University of Copenhagen (DIKU) [email protected] [email protected] Abstract. We investigate the power of non-determinism in purely func- tional programming languages with higher-order types. Specifically, we consider cons-free programs of varying data orders, equipped with ex- plicit 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 au- thors 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: addingnon-determinismtoprogramswithdataorderatleast1allowsfor a characterisation of the entire class of elementary-time decidable sets. Finally we show how, even with non-deterministic choice, the original hierarchyofcharacterisationsisrestoredbyimposingdifferentrestrictions. Keywords: implicit computational complexity, cons-free programming, EXPTIME hierarchy, non-deterministic programming, unitary variables 1 Introduction Implicit complexity is, roughly, the study of how to create bespoke programming languages that allow the programmer to write programs which are guaranteed to (a) only solve problems within a certain complexity class (e.g., the class of polynomial-time decidable sets of binary strings), and (b) to be able to solve all problems in this class. When equipped with an efficient execution engine, the programs of such a language may themselves be guaranteed to run within the complexity bounds of the class (e.g., run in polynomial time), and the plethora of means available for analysing programs devised by the programming language (cid:63) TheauthorsaresupportedbytheMarieSkl(cid:32)odowska-Curieaction“HORIP”,program H2020-MSCA-IF-2014, 658162 and by the Danish Council for Independent Research Sapere Aude grant “Complexity via Logic and Algebra” (COLA). 2 C. Kop and J. Simonsen community means that methods from outside traditional complexity theory can conceivably be brought to bear on open problems in computational complexity. One successful approach to implicit complexity is to syntactically constrain theprogrammer’sabilitytocreatenewdatastructures.Intheseminalpaper[12], Jones introduces cons-free programming. Working with a small functional pro- gramming language, cons-free programs are read-only: recursive data cannot be created or altered (beyond taking sub-expressions), only read from input. By im- posing further restrictions on data order (i.e., order 0 = integers, strings; order 1 =functionsondataoforder0;etc.)andrecursionscheme(e.g.,full/tail/primitive recursion), classes of cons-free programs turn out to characterise various deter- ministic classes in the time and space hierarchies of computational complexity. However, Jones’ language is deterministic and, perhaps as a result, his char- acterisations concern only deterministic complexity classes. It is tantalising to considerthemethodinanon-deterministicsetting:couldaddingnon-deterministic choice to Jones’ language increase its expressivity; for example, from P to NP? Theimmediateanswerisno:followingBonfante[4],addinganon-deterministic choice operator to cons-free programs with data order 0 makes no difference in expressivity—deterministic or not, they characterise P. However, the details are subtle and depend on other features of the language; when only primitive recursion is allowed, non-determinism does increase expressivity from L to NL [4]. Whilemanyauthorsconsidertheexpressivityofhighertypes,theinterplayof higher types and non-determinism is not fully understood. Jones obtains several hierarchies of deterministic complexity classes by increasing data orders [12], but these hierarchies have at most an exponential increase between levels. Given the expressivity added by non-determinism, it is a priori not evident that similarly “tame” hierarchies would arise in the non-deterministic setting. The purpose of the present paper is to investigate the power of higher-order (cons-free) programming to characterise complexity classes. The main surprise is that while non-determinism does not add expressivity for first-order programs, the combination of second-order (or higher) programs and non-determinism characterises the full class of elementary-time decidable sets—and increasing the order beyond second-order programs does not further increase expressivity. However, we will also show that there are simple changes to the restrictions that allow us to obtain a hierarchy of characterisations as in the deterministic setting. Proofs for the results in this paper are all available in the appendix. 1.1 Overview and contributions We define a purely functional programming language with non-deterministic choice and, following Jones [12], consider the restriction to cons-free programs. Our results are summarised in Figure 1. For completeness, we have also included the results from [12]; although the language used there is slightly more syntactically restrictive than ours, the results easily generalise provided we limit interest to deterministic programs, where the choose operator is not used. As the technical machinations involved to procure the results for a language with The Power of Non-Determinism in Higher-Order Implicit Complexity 3 data order 0 data order 1 data order 2 data order 3 cons-free P= EXP= EXP2TIME EXP3TIME deterministic EXP0TIME EXP1TIME cons-free L PSPACE tail-recursive = = EXP1SPACE EXP2SPACE deterministic EXP−1SPACE EXP0SPACE cons-free L P PSPACE EXP primitive recursive = = = = deterministic EXP−1SPACE EXP0TIME EXP0SPACE EXP1TIME The characterisations obtained in [12], transposed to the more permissive language used here. This list (and the one below) should be imagined as extending infinitely to the right. The “limit” for all rows (i.e., all finite data orders allowed) characterises ELEMENTARY, the class of elementary-time decidable sets. data order 0 data order 1 data order 2 data order 3 cons-free P ELEMENTARY ELEMENTARY ELEMENTARY cons-free P= EXP= EXP2TIME EXP3TIME unitary variables EXP0TIME EXP1TIME The characterisations obtained by allowing non-deterministic choice. As above, the “limit” where all data orders are allowed characterises ELEMENTARY (for both rows). arrow depth 0 arrow depth 1 arrow depth 2 arrow depth 3 cons-free P ELEMENTARY ELEMENTARY ELEMENTARY The characterisations obtained by allowing non-deterministic choice and considering arrow depth as the variable factor rather than data order Fig.1. Overview of the results discussed or obtained in this paper. full recursion are already intricate and lengthy, we have not yet considered the restriction to tail- or primitive recursion in the non-deterministic setting. Essentially, our paper has two major contributions: (a) we show that previous observations about the increase in expressiveness when adding non-determinism change dramatically at higher types, and (b) we provide two characterisations of the EXPTIME hierarchy using a non-deterministic language—which may provide a basis for future characterisation of common non-deterministic classes as well. Note that (a) is highly surprising: As evidenced by early work of Cook [6] merely adding full non-determinism to a restricted (i.e., non-Turing complete) computation model may result in it still characterising a deterministic class of problems. This also holds true for cons-free programs with non-determinism, as shownindifferentsettingsbyBonfante[4],bydeCarvalhoandSimonsen[7],and by Kop and Simonsen [14], all resulting only in characterisations of deterministic classes such as P. With the exception of [14], all of the above attempts at adding non-determinismconsiderdataorderatmost0,andonewouldexpectfewchanges when passing to higher data orders. This turns out to be patently false as simply increasing to data order 1 already results in an explosion of expressive power. 4 C. Kop and J. Simonsen 1.2 Overview of the ideas in the paper Cons-free programs (Definition 5) are, roughly, functional programs where func- tionbodiesareallowedtocontainconstantdataandsubstructuresofthefunction arguments, but no data constructors—e.g., clauses tl (x::xs)=xs and tl []=[] are both allowed, but append (x::xs) ys = x::(append xs ys) is not.1 This restriction severely limits expressivity, as it means no new data can be created. A key idea in Jones’ original work on cons-free programming is counting: expressions which represent numbers and functions to calculate with them. It is not in general possible to represent numbers in the usual unary way as 0, s 0, s (s 0), etc., or as lists of bits—since in a cons-free program these expressions cannotbebuiltunlesstheyalreadyoccurintheinput—butcountinguptolimited bounds can be achieved by other tricks. By repeatedly simulating a single step of a Turing Machine up to such bounds, Jones shows that any decision problem in EXPKTIME can be decided using a cons-free program ([12] and Lemma 6). Thecoreinsightinthepresentpaperisthatinthepresenceofnon-determinism, an expression of type σ ⇒τ represents a relation between expressions of type σ and expressions of type τ rather than a function. While the number of functions foragiventypeisexponentialintheorderofthattype,thenumberofrelationsis exponential in the depth of arrows occurring in it. We exploit this (in Lemma 11) by counting up to arbitrarily high numbers using only first-order data. This observation also suggest that by limiting the arrow depth rather than the order of types, the increase in expressive power disappears (Theorem 3). Conversely, we also provide an algorithm to compute the output of cons-free programs potentially much faster than the program’s own running time, by using a tableaux to store results. Although similar to Jones’ ideas, our proof style deviates to easily support both non-deterministic and deterministic programs. 1.3 Related work The creation of programming languages that characterise complexity classes has been a research area since Cobham’s work in the 1960ies, but saw rapid develop- mentonlyaftersimilaradvancesintherelatedareaofdescriptive complexity (see, e.g.,[10])inthe1980iesandBellantoniandCook’sworkoncharacterisationsofP [2] using constraints on recursion in a purely functional language with programs reminiscent of classic recursion theoretic functions. Following Bellantoni and Cook, a number of authors obtained programming languages by constraints on recursion, and under a plethora of names (e.g., safe, tiered or ramified recursion, see[5,18]foroverviews),andthisareacontinuestobeactive.Themaindifference withourworkisthatweconsiderfullrecursioninallvariables,butplacesyntactic constraints on the function bodies (both cons-freeness and unitary variables). Also,asintraditionalcomplexitytheoryweconsiderdecisionproblems(i.e.,what sets can be decided by programs), whereas much research in implicit complexity considers functional complexity (i.e., what functions can be computed). 1 Theformaldefinitionisslightlymoreliberaltosupporteasierimplementationsusing pattern-matching, but the ideas remain the same. The Power of Non-Determinism in Higher-Order Implicit Complexity 5 Cons-free programs, combined with various limitations on recursion, were introduced by Jones [12], building on ground-breaking work by Goerdt [9,8], and have been studied by a number of authors (see, e.g., [3,4,17,16]). The main difference with our work is that we consider full recursion with full non- determinism, but impose constraints not present in the previous literature. Characterisation of non-deterministic complexity classes via programming languages remains a largely unexplored area. Bellantoni obtained a characterisa- tion of NP in his dissertation [1] using similar approaches as [2], but at the cost of having a minimisation operator (as in recursion theory), a restriction later removed by Oitavem [19]. A general framework for implicitly characterising a larger hierarchy of non-deterministic classes remains an open problem. 2 A purely functional, non-deterministic, call-by-value programming language We define a simple call-by-value programming language with explicit non- deterministic choice. This generalises Jones’ toy language in [12] by supporting different types and pattern-matching as well as non-determinism. The more permissive language actually simplifies proofs and examples, since we do not need to encode all data as boolean lists, and have fewer special cases. 2.1 Syntax We consider programs defined by the syntax in Figure 2 p∈Program::=ρ ρ ... ρ 1 2 N ρ∈Clause::=f (cid:96) ···(cid:96) =s 1 k (cid:96)∈Pattern::=x|c (cid:96) ···(cid:96) 1 m s,t∈Expr::=x|c|f|ifs thens elses |choose s ···s |(s,t)|s t 1 2 3 1 n x,y∈V ::=identifier c∈C ::=identifier disjoint from V (we assume {true,false}⊆C) f,g∈D ::=identifier disjoint from V and C Fig.2. Syntax We call elements of V variables, elements of C data constructors and elements of D defined symbols. The root of a clause f (cid:96) ···(cid:96) =s is the defined symbol 1 k f. The main function f of the program is the root of ρ . We denote Var(s) for 1 1 the set of variables occurring in an expression s. An expression s is ground if Var(s)=∅. Application is left-associative, i.e., s t u should be read (s t) u. Definition 1. Forexpressionss,t,wesaythat tisasub-expressionofs,notation s(cid:4)t, if this can be derived using the clauses: s(cid:4)tifs=t or s(cid:3)t (s ,s )(cid:3)tifs (cid:4)t or s (cid:4)t ifs thens elses (cid:3)tifs (cid:4)t for some i 1 2 1 2 1 2 3 i s s (cid:3)tifs (cid:3)t or s (cid:4)t choose s ···s (cid:3)tifs (cid:4)t for some i 1 2 1 2 1 n i Note: the head s of an application s t is not considered a sub-expression of s t. 6 C. Kop and J. Simonsen Note that the programs we consider have no pre-defined data structures like integers: these may be encoded using inductive data structures in the usual way. Example 1. Integers can be encoded as bitstrings of unbounded length: C ⊇ {false,true,::,[]}.Here,::isconsideredinfixandright-associative,and[]denotes theendofthestring.Usinglittleendian,6isencodedbyfalse::true::true::[]as wellasfalse::true::true::false::false::[].Weforinstancehavetrue::(succxs) (cid:4)xs (for xs∈V). The program below imposes D ={succ}: succ []=true::[] succ (false::xs)=true::xs succ (true::xs)=false::(succ xs) 2.2 Typing Programs have explicit simple types without polymorphism, with the usual definition of type order ord(σ); this is formally given in Figure 3. ι∈S ::=sort identifier ord(ι)=0 for ι∈S σ,τ ∈Type::=ι|σ×τ |σ⇒τ ord(σ×τ)=max(ord(σ),ord(τ)) ord(σ⇒τ)=max(ord(σ)+1,ord(τ)) Fig.3. Types and type orders The (finite) set S of sorts is used to type atomic data such as bits; we assume bool∈S. The function arrow ⇒ is considered right-associative. Writing κ for a sort or a pair type σ ×τ, any type can be uniquely presented in the form σ ⇒...⇒σ ⇒κ. We will limit interest to well-typed, well-formed programs: 1 m Definition 2. A program p is well-typed if there is an assignment F from C∪D to the set of simple types such that: – themainfunctionf isassignedatypeκ ⇒...⇒κ ⇒κ,withord(κ )=0 1 1 M i for 1≤i≤M and also ord(κ)=0 – data constructors c∈C are assigned a type κ ⇒...⇒κ ⇒ι with ι∈S 1 m and ord(κ )=0 for 1≤i≤m i – for all clauses f (cid:96) ···(cid:96) =s∈p, the following hold: 1 k • Var(s)⊆Var(f(cid:96) ···(cid:96) )andeachvariableoccursonlyonceinf(cid:96) ···(cid:96) ; 1 k 1 k • there exist a type environment Γ mapping Var(f (cid:96) ···(cid:96) ) to simple types, 1 k and a simple type σ, such that both f (cid:96) ···(cid:96) : σ and s : σ using the 1 k rules in Figure 4; we call σ the type of the clause. s:σ t:τ s:σ⇒τ t:σ if a:σ∈Γ ∪F a:σ (s,t):σ×τ s t:τ s1 :bool s2 :σ s3 :σ s1 :σ ... sn :σ ifs1thens2elses3 :σ choose s1···sn :σ Fig.4. Typing (for fixed F and Γ, see Definition 2) The Power of Non-Determinism in Higher-Order Implicit Complexity 7 Note that this definition does not allow for polymorphism: there is a single type assignment F for the full program. The assignment F also forces a unique choice for the type environment Γ of variables in each clause. Thus, we may speak of the type of an expression in a clause without risk of confusion. Example 2. The program of Example 1 is typed using F ={false:bool,true: bool,[]:list,:::bool⇒list⇒list,succ:list⇒list}. As all argument and output types have order 0, the variable restrictions are satisfied and all clauses can be typed using Γ ={xs:list}, the program is well-typed. Definition 3. A program p is well-formed if it is well-typed, and moreover: – data constructors are always fully applied: for all c∈C with c:κ ⇒...⇒ 1 κ ⇒ι∈F: if a sub-expression c t ···t occurs in any clause, then n=m; m 1 n – the number of arguments to a given defined symbol is fixed: if f (cid:96) ···(cid:96) =s 1 k and f (cid:96)(cid:48) ···(cid:96)(cid:48) =t are both in p, then k =n; we let arity (f) denote k. 1 n p Example 3. The program of Example 1 is well-formed, and arity (succ)=1. p However, the program would not be well-formed if the clauses below were added, as here the defined symbol or does not have a consistent arity. id x=x or true x=true or false=id Remark 1. Dataconstructorsmust(a)haveasortasoutputtype(not apair),and (b)occuronlyfullyapplied.Thisisconsistentwithtypicalfunctionalprogramming languages, where sorts and constructors are declared with a grammar such as: sdec ∈SortDec::=data ι=cdec |···|cdec 1 n cdec ∈ConstructorDec::=c σ ··· σ 1 m In addition, we require that the arguments to data constructors have type order 0. This is not standard in functional programming, but is the case in [12]. We limit interest to such constructors because, practically, these are the only ones which can be used in a cons-free program (as we will discuss in Section 3). Definition 4. A program has data order K if all clauses can be typed using type environments Γ such that, for all x:σ ∈Γ: ord(σ)≤K. Example 4. We consider a higher-order program, operating on the same data constructors as Example 1; however, now we encode numbers using functions: fsucc F []=if F [] then set F [] false else set F [] true fsucc F xs=if F xs then fsucc (set F xs false) (tl xs) else set F xs true set F val xs ys=if eqlen xs ys then val else F ys tl (x::xs)=xs eqlen (x::xs) (y::ys)=eqlen xs ys eqlen [] []=true eqlen xs ys=false Only one typing is possible, with fsucc:(list⇒bool)⇒list⇒list⇒ bool; therefore, F is always typed list⇒bool—which has type order 1—and all other variables with a type of order 0. Thus, this program has data order 1. To explain the program: we use boolean lists as unary numbers of a limited size; assuming that (a) F represents a bitstring of length N +1, and (b) lst has length N, the successor of F (modulo wrapping) is obtained by fsucc F lst. 8 C. Kop and J. Simonsen 2.3 Semantics Like Jones, our language has a closure-based call-by-value semantics. We let data expressions, values and environments be defined by the grammar in Figure 5. d,b∈Data::=c d ···d |(d,b) Instantiation: 1 m v,w∈Value::=d|(v,w)|f v ···v xγ :=γ(x) 1 n (n<arity (f)) (c (cid:96) ···(cid:96) )γ :=c ((cid:96) γ)···((cid:96) γ) p 1 n 1 n γ,δ∈Env::=V →Value Fig.5. Data expressions, values and environments Let dom(γ) denote the domain of an environment (partial function) γ. Note that values are ground expressions, and we only use well-typed values with fully applied data constructors. To every pattern (cid:96) and environment γ with dom(γ)⊇ Var((cid:96)), we associate a value (cid:96)γ by instantiation in the obvious way, see Figure 5. Notethat,foreveryvaluev andpattern(cid:96),thereisatmostoneenvironmentγ with (cid:96)γ =v. We say that an expression f s ···s instantiates the left-hand side 1 n of a clause f (cid:96) ···(cid:96) if n=k and there is an environment γ with each s =(cid:96) γ. 1 k i i Both input and output to the program are data expressions. If f has type 1 κ ⇒ ... ⇒ κ ⇒ κ, we can think of the program as calculating a function 1 M p (d ,...,d ) from M input data arguments to an output data expression. 1 M (cid:74) (cid:75)Expression and program evaluation are given by the rules in Figure 6. Since, in [Call], there is at most one suitable γ, the only source of non-determinism is the choose operator. Programs without this operator are called deterministic. By contrast, we may refer to a non-deterministic program as one which is not explicitly required to be deterministic, so which may or may not contain choose. Example 5. For the program from Example 1, p (true::false::true::[]) (cid:55)→ false::true::true::[], giving 5+1=6. In the prog(cid:74)ra(cid:75)m f x y =choose x y, we 1 can both derive p (true,false)(cid:55)→true and p (true,false)(cid:55)→false. (cid:74) (cid:75) (cid:74) (cid:75) The language is easily seen to be Turing-complete unless further restrictions are imposed. In order to assuage any fears on whether the complexity-theoretic characterisationsweobtainareduetobrittledesignchoices,weaddsomeremarks. Remark 2. We have omitted some constructs common to even some toy pure functional languages, but these are in general simple syntactic sugar that can be readily expressed by the existing constructs in the language, even in the presence of non-determinism. For instance, a let-binding letx = s ins can 1 2 be straightforwardly encoded by a function call in a pure call-by-value setting (replacing letx=s ins by helper s and adding a clause helper x=s ). 1 2 1 2 Remark 3. We do not require the clauses of a function definition to exhaust all possible patterns. For instance, it is possible to have a clause ftrue = ··· without a clause for ffalse. Thus, a program has zero or more values. The Power of Non-Determinism in Higher-Order Implicit Complexity 9 Expression evaluation: [Instance]: p(cid:96)call f→w p,γ (cid:96)x→γ(x) [Function]: for f∈D p,γ (cid:96)f→w p,γ (cid:96)s →b ··· p,γ (cid:96)s →b [Constructor]: 1 1 m m p,γ (cid:96)c s ···s →c b ···b 1 m 1 m p,γ (cid:96)s→v p,γ (cid:96)t→w [Pair]: p,γ (cid:96)(s,t)→(v,w) p,γ (cid:96)s →w [Choice]: i for 1≤i≤n p,γ (cid:96)choose s ···s →w 1 n p,γ (cid:96)s →d p,γ (cid:96)if d,s ,s →w [Conditional]: 1 2 3 p,γ (cid:96)ifs thens elses →w 1 2 3 p,γ (cid:96)s →w p,γ (cid:96)s →w [If-True]: 2 [If-False]: 3 p,γ (cid:96)if true,s ,s →w p,γ (cid:96)if false,s ,s →w 2 3 2 3 p,γ (cid:96)s→f v ···v p,γ (cid:96)t→v p(cid:96)call f v ···v →w [Appl]: 1 n n+1 1 n+1 p,γ (cid:96)s t→w [Closure]: if n<arity (f) p(cid:96)call f v ···v →f v ···v p 1 n 1 n if f (cid:96) ···(cid:96) =s is the first clause in p such p,γ (cid:96)s→w 1 k [Call]: that f v ···v instantiates f (cid:96) ···(cid:96) , and p(cid:96)call f v ···v →w 1 k 1 k 1 k dom(γ)=Var(f (cid:96) ···(cid:96) ) and each v =(cid:96) γ 1 k i i Program execution: p,[x :=d ,...,x :=d ](cid:96)f x ···x →b 1 1 M M 1 1 M p (d ,...,d )(cid:55)→b 1 M (cid:74) (cid:75) Fig.6. Call-by-value semantics Data order versus program order. We have followed Jones in considering data order as the variable for increasing complexity. However, an alternative choice —whichturnsouttostreamlineourproofs—isprogram order,whichconsidersthe type order of the function symbols. Fortunately, these notions are closely related; barring unused symbols, (cid:104)program order(cid:105) = (cid:104)data order(cid:105) + 1. More specifically, we have the following result: Lemma 1. For every well-formed program p with data order K, there is a well- formed program p(cid:48) such that p (d ,...,d )(cid:55)→b iff p(cid:48) (d ,...,d )(cid:55)→b for any 1 M 1 M b ,...,b ,d and: (a) all defi(cid:74)n(cid:75)ed symbols in p(cid:48) have(cid:74)a(cid:75)type σ ⇒...⇒σ ⇒κ 1 M 1 m such that both ord(σ )≤K for all i and ord(κ)≤K, and (b) in all clauses, all i sub-expressions of the right-hand side have a type of order ≤K as well.