<p>I'd also like to mention Implicit Complexity Theory as an approach to this, since I've seen it come up in several somewhat-related questions.  To quote <a href="https://cstheory.stackexchange.com/a/3422/12747">this answer by Neel Krishnaswami</a>:</p>

<blockquote>
  <p>The basic technique is to relate complexity classes to subsystems of linear logic (the so-called "light linear logics"), with the idea that the cut-elimination for the logical system should be complete for the given complexity class (such as LOGSPACE, PTIME, etc). Then via Curry-Howard you get out a programming language in which precisely the programs in the given class are expressible.</p>
</blockquote>

CC BY-SA 3.0
2012-12-07T13:09:05.710Z
2012-12-07T13:09:05.710Z
2017-04-13T12:32:28.117Z
Chris Pressey
<p>Have a look at Guillaume Bonfante paper who proposed two characterizations for Logspace and polynomial time using programming languages.</p>

<p><a href="http://books.google.com/books?id=QbI4EVGTox8C&amp;pg=PA66&amp;dq=Some+programming+languages+Bonfante&amp;hl=en&amp;ei=52hmTcG1MczcsgaCxa3aDA&amp;sa=X&amp;oi=book_result&amp;ct=result&amp;resnum=1&amp;ved=0CCwQ6AEwAA&amp;safe=active#v=onepage&amp;q=Some%20programming%20languages%20Bonfante&amp;f=false">Guillaume Bonfante, Some programming languages for Logspace and
Ptime , AMAST 2006, LNCS 4019, pp. 66-80, 2006</a></p>

CC BY-SA 2.5
2011-02-24T14:20:28.970Z
2011-02-24T14:20:28.970Z
Mohammad Al-Turkistany
<p>I am surprised no one has mentioned primitive recursion. By restricting to bounded loops (i.e. the number of iterations for each loop must be calculated before the loop commences) the resulting program is primitive recursive, and hence total. Douglas Hofstadter proposed a programming language, BLOOP, that allowed all and only primitive recursive functions.</p>

CC BY-SA 3.0
2011-11-25T22:00:49.080Z
It's a proper subclass of all functions, but calling it a class of "efficient" functions might be a bit of a stretch.
Raphael
CC BY-SA 3.0
2011-11-26T07:00:29.893Z
I guess you can modify it to capture $\mathsf{P}$ using Cobham's characterization of $\mathsf{P}$ as polynomially bounded recursion.
Kaveh
CC BY-SA 3.0
2013-05-20T22:49:12.533Z
Others mentioned System F and other strongly normalizing languages, which in a sense only support "primitive recursion". However, since they support first-class functions, they allow writing more programs (like the Ackermann function).
Blaisorblade
CC BY-SA 3.0
2011-11-25T18:45:35.687Z
2011-11-25T18:45:35.687Z
David Harris
<p>See also <a href="http://projects.wizardlike.ca/projects/pola" rel="nofollow">Pola a language for PTIME programming</a> and works of Japaridze on PTIME arithmetic e.g. <a href="http://arxiv.org/abs/0902.2969" rel="nofollow">http://arxiv.org/abs/0902.2969</a></p>

CC BY-SA 3.0
2011-11-25T17:55:34.393Z
2011-11-25T17:55:34.393Z
nponeccop
<p>One language attempting to express only polynomial time computations is the <a href="http://www-lipn.univ-paris13.fr/~baillot/Publications/MESPAPIERS/fossacs072.pdf" rel="nofollow">soft lambda calculus</a>. It's type system is rooted in linear logic. A recent <a href="http://edoc.ub.uni-muenchen.de/9910/1/Schimanski_Stefan.pdf" rel="nofollow">thesis</a> addresses polynomial time calculi, and provides a good summary of recent developments based on this approach. Martin Hofmann has been working on the topic for quite some time. An older list of relevant papers can be found <a href="http://www.dcs.ed.ac.uk/home/resbnd/" rel="nofollow">here</a>; Many of his <a href="http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/h/Hofmann:Martin.html" rel="nofollow">papers</a>'s continue in this direction.</p>

<p>Other work takes the approach of verifying that the program uses a certain amount of resources, using <a href="http://www.cs.st-andrews.ac.uk/~eb/drafts/icfp09.pdf" rel="nofollow">Dependent Types</a> or <a href="http://www.cs.cornell.edu/talc/papers/resource_bound/res.pdf" rel="nofollow">Typed Assembly Language</a>.</p>

<p>Yet other approaches are based on <a href="http://www.di.unito.it/~dezani/papers/asian03.pdf" rel="nofollow">resource bounded formal calculi</a>, such as variants of the ambient calculus.</p>

<p>These approaches have the property that well-typed programs satisfy some pre-specified resource bounds. The resource bound could be time or space, and generally can depend upon the size of the inputs.</p>

<p>Early work in this area is on strongly normalising calculi, meaning that all well-typed programs halt. <a href="http://en.wikipedia.org/wiki/System_F" rel="nofollow">System F</a>, aka the polymorphic lambda calculus, is strongly normalising.  It has no fixed point operator, but is nonetheless quite expressive, though I don't think it is known what complexity class it corresponds to. By definition, any strongly normalising calculus expresses some class of terminating computations.</p>

<p>The programming language <a href="http://en.wikipedia.org/wiki/Charity_(programming_language)" rel="nofollow">Charity</a> is a quite expressive functional language that halts on all inputs. I don't know what complexity class it can expression, but the Ackermann function can be written in Charity.</p>

CC BY-SA 3.0
2011-11-28T14:45:10.707Z
What do you mean by 'at least' here?
nponeccop
CC BY-SA 3.0
2011-11-28T14:52:16.787Z
'At least' here means 'some'. I'll change my answer to make it a little more precise.
Dave Clarke
CC BY-SA 3.0
2012-12-07T16:28:30.953Z
I'm pretty sure that the complexity of functions definable in system F is the class of functions which terminate in time "some provably total function of 2nd order arithmetic" of the input. Not a very conventional complexity class, but still...
cody
CC BY-SA 3.0
2013-05-20T22:46:29.087Z
cody: according to Wadler's "Theorems for free", System F can express "every recursive function which can be proved total in second-order Peano arithmetic", and that "includes [...] Ackermann's function". I'm not sure if that's the same you're describing.
Charity's main feature is its support for codata, while I think Agda's termination checking allows more expressivity than both Coq and System F while guaranteeing termination.
Blaisorblade
CC BY-SA 3.0
2011-02-24T12:03:23.483Z
2016-03-22T16:18:36.423Z
2016-03-22T16:18:36.423Z
Dave Clarke
<p>It is impossible to write a programming language that allows all machines that halt on all inputs and no others. However, it seems to be easy to define such a programming language for any standard complexity class. In particular, we can define a language in which we can express all efficient computations and only efficient computations. </p>

<p>For instance, for something like $P$: take your favorite programming language, and after you write your program (corresponding to Turing Machine $M'$), add three values to the header: an integer $c$, and integer $k$, and a default output $d$. When the program is compiled, output a Turing machine $M$ that given input $x$ of size $n$ runs $M&#39;$ on $x$ for $c n^k$ steps. If $M&#39;$ does not halt before the $c n^k$ steps are up, output the default output $d$. Unless I am mistaken, this programming languages will allow us to express all computations in $P$ and nothing more. However, this proposed language is inherently non-interesting.</p>

<p>My question: are there programming languages that capture subsets of computable functions (such as all efficiently computable function) in a non-trivial way? If there are not, is there a reason for this?</p>

CC BY-SA 2.5
2011-02-24T14:06:27.870Z
Some simple examples of programming languages that capture subsets of computable functions: regular expressions and context-free grammars.
Jukka Suomela
CC BY-SA 2.5
2011-02-25T05:16:15.910Z
Actually the languages that captures complexity class $\mathbf{P}$ like $\mathbf{PV}$ (which is defined in a similar way to primitive recursive functions with recursion replaced by bounded recursion) are quite interesting (at least from theoretical point of view). :)
Kaveh
CC BY-SA 3.0
2011-11-30T16:22:45.243Z
Linear and Integer Programming capture interesting subsets of computable functions.
didest
CC BY-SA 3.0
2012-01-16T12:36:39.980Z
Datalog can only express polynomial time algorithms, but I don't know if it can express all polynomial time algorithms.
Jules
CC BY-SA 3.0
2012-12-12T18:53:43.247Z
The well known paper "Total functional programming" makes the argument that programming languages that don't have an undecidable halting problem are actually practical and useful. http://www.jucs.org/jucs_10_7/total_functional_programming
none
CC BY-SA 3.0
2012-12-14T18:15:35.097Z
"It is impossible to write a programming language that allows all machines that halt on all inputs and no others." think what you mean to say is "it is impossible to write an _unlimited_ [defined as Turing complete] programming language that _only_ allows machines that halt on all inputs and no others". there are _limited_ programming languages associated with complexity classes as you note...
vzn
CC BY-SA 3.0
2013-05-20T22:40:20.767Z
none: languages like Agda or Epigram implement that idea (together with dependent typing).
Blaisorblade
<cc.complexity-theory><computability><pl.programming-languages>
Programming languages for efficient computation
Artem Kaznatcheev
# Programming languages for efficient computation

(Asked by: username_0 on 2011-02-24)

It is impossible to write a programming language that allows all machines that halt on all inputs and no others. However, it seems to be easy to define such a programming language for any standard complexity class. In particular, we can define a language in which we can express all efficient computations and only efficient computations.

For instance, for something like $P$: take your favorite programming language, and after you write your program (corresponding to Turing Machine $M'$), add three values to the header: an integer $c$, and integer $k$, and a default output $d$. When the program is compiled, output a Turing machine $M$ that given input $x$ of size $n$ runs $M'$ on $x$ for $c n^k$ steps. If $M'$ does not halt before the $c n^k$ steps are up, output the default output $d$. Unless I am mistaken, this programming languages will allow us to express all computations in $P$ and nothing more. However, this proposed language is inherently non-interesting.

My question: are there programming languages that capture subsets of computable functions (such as all efficiently computable function) in a non-trivial way? If there are not, is there a reason for this?

**Tags:** cc.complexity-theory, computability, pl.programming-languages

> **Comments:**
> **username_1**: Some simple examples of programming languages that capture subsets of computable functions: regular expressions and context-free grammars.  
> **username_2**: Actually the languages that captures complexity class $\mathbf{P}$ like $\mathbf{PV}$ (which is defined in a similar way to primitive recursive functions with recursion replaced by bounded recursion) are quite interesting (at least from theoretical point of view). :)  
> **username_3**: Linear and Integer Programming capture interesting subsets of computable functions.  
> **username_4**: Datalog can only express polynomial time algorithms, but I don't know if it can express all polynomial time algorithms.  
> **username_5**: The well known paper "Total functional programming" makes the argument that programming languages that don't have an undecidable halting problem are actually practical and useful. http://www.jucs.org/jucs_10_7/total_functional_programming  
> **username_6**: "It is impossible to write a programming language that allows all machines that halt on all inputs and no others." think what you mean to say is "it is impossible to write an _unlimited_ [defined as Turing complete] programming language that _only_ allows machines that halt on all inputs and no others". there are _limited_ programming languages associated with complexity classes as you note...  
> **username_7**: username_5: languages like Agda or Epigram implement that idea (together with dependent typing).  

---

## 5 answers

### Answer by username_13 on 2011-02-24. Score: 32 | Accepted answer

One language attempting to express only polynomial time computations is the [soft lambda calculus](http://www-lipn.univ-paris13.fr/~baillot/Publications/MESPAPIERS/fossacs072.pdf). It's type system is rooted in linear logic. A recent [thesis](http://edoc.ub.uni-muenchen.de/9910/1/Schimanski_Stefan.pdf) addresses polynomial time calculi, and provides a good summary of recent developments based on this approach. Martin Hofmann has been working on the topic for quite some time. An older list of relevant papers can be found [here](http://www.dcs.ed.ac.uk/home/resbnd/); Many of his [papers](http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/h/Hofmann:Martin.html)'s continue in this direction.

Other work takes the approach of verifying that the program uses a certain amount of resources, using [Dependent Types](http://www.cs.st-andrews.ac.uk/~eb/drafts/icfp09.pdf) or [Typed Assembly Language](http://www.cs.cornell.edu/talc/papers/resource_bound/res.pdf).

Yet other approaches are based on [resource bounded formal calculi](http://www.di.unito.it/~dezani/papers/asian03.pdf), such as variants of the ambient calculus.

These approaches have the property that well-typed programs satisfy some pre-specified resource bounds. The resource bound could be time or space, and generally can depend upon the size of the inputs.

Early work in this area is on strongly normalising calculi, meaning that all well-typed programs halt. [System F](http://en.wikipedia.org/wiki/System_F), aka the polymorphic lambda calculus, is strongly normalising. It has no fixed point operator, but is username_5theless quite expressive, though I don't think it is known what complexity class it corresponds to. By definition, any strongly normalising calculus expresses some class of terminating computations.

The programming language [Charity](http://en.wikipedia.org/wiki/Charity_(programming_language)) is a quite expressive functional language that halts on all inputs. I don't know what complexity class it can expression, but the Ackermann function can be written in Charity.

> **Comments:**
> **username_12**: What do you mean by 'at least' here?  
> **username_13**: 'At least' here means 'some'. I'll change my answer to make it a little more precise.  
> **username_14**: I'm pretty sure that the complexity of functions definable in system F is the class of functions which terminate in time "some provably total function of 2nd order arithmetic" of the input. Not a very conventional complexity class, but still...  
> **username_7**: username_14: according to Wadler's "Theorems for free", System F can express "every recursive function which can be proved total in second-order Peano arithmetic", and that "includes [...] Ackermann's function". I'm not sure if that's the same you're describing. Charity's main feature is its support for codata, while I think Agda's termination checking allows more expressivity than both Coq and System F while guaranteeing termination.  

---

### Answer by username_9 on 2011-02-24. Score: 10

Have a look at Guillaume Bonfante paper who proposed two characterizations for Logspace and polynomial time using programming languages.

[Guillaume Bonfante, Some programming languages for Logspace and
Ptime , AMAST 2006, LNCS 4019, pp. 66-80, 2006](http://books.google.com/books?id=QbI4EVGTox8C&pg=PA66&dq=Some+programming+languages+Bonfante&hl=en&ei=52hmTcG1MczcsgaCxa3aDA&sa=X&oi=book_result&ct=result&resnum=1&ved=0CCwQ6AEwAA&safe=active#v=onepage&q=Some%20programming%20languages%20Bonfante&f=false)


---

### Answer by username_8 on 2012-12-07. Score: 8

I'd also like to mention Implicit Complexity Theory as an approach to this, since I've seen it come up in several somewhat-related questions. To quote [this answer by Neel Krishnaswami](https://cstheory.stackexchange.com/a/3422/12747):

> The basic technique is to relate complexity classes to subsystems of linear logic (the so-called "light linear logics"), with the idea that the cut-elimination for the logical system should be complete for the given complexity class (such as LOGSPACE, PTIME, etc). Then via Curry-Howard you get out a programming language in which precisely the programs in the given class are expressible.


---

### Answer by username_10 on 2011-11-25. Score: 5

I am surprised no one has mentioned primitive recursion. By restricting to bounded loops (i.e. the number of iterations for each loop must be calculated before the loop commences) the resulting program is primitive recursive, and hence total. Douglas Hofstadter proposed a programming language, BLOOP, that allowed all and only primitive recursive functions.

> **Comments:**
> **username_11**: It's a proper subclass of all functions, but calling it a class of "efficient" functions might be a bit of a stretch.  
> **username_2**: I guess you can modify it to capture $\mathsf{P}$ using Cobham's characterization of $\mathsf{P}$ as polynomially bounded recursion.  
> **username_7**: Others mentioned System F and other strongly normalizing languages, which in a sense only support "primitive recursion". However, since they support first-class functions, they allow writing more programs (like the Ackermann function).  

---

### Answer by username_12 on 2011-11-25. Score: 3

See also [Pola a language for PTIME programming](http://projects.wizardlike.ca/projects/pola) and works of Japaridze on PTIME arithmetic e.g. <http://arxiv.org/abs/0902.2969>


---

