7
$\begingroup$

Does there exist a programming language which is homoiconic (in the sense that any code can be represented as a data structure, can be altered, and can be run after being altered) but not Turing complete?

For instance, one may avoid "for loops" by preventing data (which could represent code) from being copied.

$\endgroup$
  • 1
    $\begingroup$ For a more informal discussion of why "homoiconic" isn't a terribly interesting category of languages (and what it often really means: that the tree structure of a language can be observed without complete parsing), see Dave Herman's essay: calculist.org/blog/2012/04/17/homoiconicity-isnt-the-point $\endgroup$ – Paul Stansifer Mar 22 '16 at 14:55
9
$\begingroup$

You can turn every programming language $L$ into a homoiconic language $L_{hom}$ by adding a suitable representation of programs, such as ASTs (abstract syntax trees) or quasi-quoted programs, together with some operations that mediate between $L$ and the representation of $L$-syntax (e.g. evaluation or splicing instructions). The details of this depend on your precise rendering of homoiconicity (e.g. compile-time as in Template Haskell vs run-time as in the MetaML family of languages or Javascript).

One extreme example is the empty language $L^{\emptyset}$ that has no programs. Clearly its homoiconic variant $L^{\emptyset}_{hom}$ isn't Turing complete. For more interesting examples, you can take any of the usual type theories such as the simply typed $\lambda$-calculus, System F or the Calculus of Constructions. Of course one would have to prove that the homoiconified version of such type-theories doesn't allow us to encode recursion somehow. I doubt that this has been done. Cody's comment below suggests that this might not be possible.

| cite | improve this answer | |
$\endgroup$
  • 1
    $\begingroup$ I don't believe that the claimed result holds, or at least that "reasonable" definitions are less trivial than expected. For example, imagine that your language contains a Syntax type and an eval construct that returns the "un-quoted" version of a quoted term, if it is well-typed of type Syntax -> Syntax, as well as a quote term. Then one can define loop x = (eval x) x and finally call loop (quote loop). Connor McBride explains this perfectly here: mail.haskell.org/pipermail/haskell-cafe/2003-May/004343.html $\endgroup$ – cody Mar 23 '16 at 20:21
  • $\begingroup$ I'm confused: are you agreeing that the result you claim in your last sentence is false? $\endgroup$ – cody Mar 24 '16 at 15:44
  • 1
    $\begingroup$ @cody Sorry, I misunderstood what you meant. I should have re-read the second part of my answer. I've edited it accordingly. $\endgroup$ – Martin Berger Mar 24 '16 at 16:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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