33
$\begingroup$

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?

Improve this question
$\endgroup$
7
  • 7
    $\begingroup$ Some simple examples of programming languages that capture subsets of computable functions: regular expressions and context-free grammars. $\endgroup$
    – Jukka Suomela
    Feb 24, 2011 at 14:06
  • 2
    $\begingroup$ 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). :) $\endgroup$
    – Kaveh
    Feb 25, 2011 at 5:16
  • $\begingroup$ Linear and Integer Programming capture interesting subsets of computable functions. $\endgroup$
    – didest
    Nov 30, 2011 at 16:22
  • $\begingroup$ Datalog can only express polynomial time algorithms, but I don't know if it can express all polynomial time algorithms. $\endgroup$
    – Jules
    Jan 16, 2012 at 12:36
  • $\begingroup$ 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. jucs.org/jucs_10_7/total_functional_programming $\endgroup$
    – none
    Dec 12, 2012 at 18:53

5 Answers 5

Reset to default
32
$\begingroup$

One language attempting to express only polynomial time computations is the soft lambda calculus. It's type system is rooted in linear logic. A recent thesis 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; Many of his papers's continue in this direction.

Other work takes the approach of verifying that the program uses a certain amount of resources, using Dependent Types or Typed Assembly Language.

Yet other approaches are based on resource bounded formal calculi, 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, 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.

The programming language Charity 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.

Improve this answer
$\endgroup$
4
  • $\begingroup$ What do you mean by 'at least' here? $\endgroup$
    – nponeccop
    Nov 28, 2011 at 14:45
  • $\begingroup$ 'At least' here means 'some'. I'll change my answer to make it a little more precise. $\endgroup$
    – Dave Clarke
    Nov 28, 2011 at 14:52
  • $\begingroup$ 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... $\endgroup$
    – cody
    Dec 7, 2012 at 16:28
  • $\begingroup$ 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. $\endgroup$
    – Blaisorblade
    May 20, 2013 at 22:46
10
$\begingroup$

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

Improve this answer
$\endgroup$
8
$\begingroup$

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:

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.

Improve this answer
$\endgroup$
5
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ It's a proper subclass of all functions, but calling it a class of "efficient" functions might be a bit of a stretch. $\endgroup$
    – Raphael
    Nov 25, 2011 at 22:00
  • $\begingroup$ I guess you can modify it to capture $\mathsf{P}$ using Cobham's characterization of $\mathsf{P}$ as polynomially bounded recursion. $\endgroup$
    – Kaveh
    Nov 26, 2011 at 7:00
  • $\begingroup$ 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). $\endgroup$
    – Blaisorblade
    May 20, 2013 at 22:49
3
$\begingroup$

See also Pola a language for PTIME programming and works of Japaridze on PTIME arithmetic e.g. http://arxiv.org/abs/0902.2969

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.