Primitive recursion seems to be related to bounded quantification. It is easier to make sense of bounded quantification with respect to natural numbers than to make sense of bounded quantification with respect to finite strings.

  • A relatively clean way out of this dilemma could be a two sorted language with both natural numbers and finite strings, and some basic functions between the two sorts, like the lengths of a string, or the string where one symbol is repeated n times.

  • A nicer solution could be to avoid the need for natural numbers, and work with some more native finite string related concepts, like head/tail, substring, ... instead.

I wonder whether there exist a robust computational model (on finite strings) corresponding to primitive recursion, just like Turing machines represents a robust computational model (on finite strings) corresponding to general ($\mu$-) recursion.

  • $\begingroup$ Strings are (isomorphic to) lists of characters. Lists (and more generally algebraic data types) come with a recursion principle that can be seen as a form of primitive recursion. Is this what you have in mind? $\endgroup$ – Martin Berger Feb 28 '17 at 10:37
  • $\begingroup$ @MartinBerger If worked out explicitly together with sufficiently convincing proofs that it gives essententially the same computational power as primitive recursion gives with respect to the natural numbers, then yes. One point where I was unsure about the recursion principle for algebraic datatypes is "BinaryTree( LeftTerm, RightTerm )", because the "for loop" would execute "LeftTerm" and "RightTerm" in some unspecified order. It is some "parallel for loop", and the required indepence of the different parts of the computation makes working it out explicitly more challenging (and interesting). $\endgroup$ – Thomas Klimpel Feb 28 '17 at 12:03
  • $\begingroup$ You can define the natural numbers as ADTs, and check that the induction/recursion principles specialise to what you are looking for. E.g. the induct_tac in Isabelle/HOL gives you that IIRC. I'm not sure what parallelism has to do with it, since in order to be able to observe parallelism, you need some kind of effect such as non-termination. But from what you write, that doesn't apply in your case. $\endgroup$ – Martin Berger Feb 28 '17 at 13:28
  • $\begingroup$ The question of parallelism is highly interesting, and the standard domain-theoretic models fail to be fully abstract because of this, e.g. should $false \wedge \Omega$ result in $false$ or $\Omega$? (Here $\Omega$ is a non-terminating program) but that's not directly related. $\endgroup$ – Martin Berger Feb 28 '17 at 13:30

You don't really need to do anything. Without loss of generality, let $\Sigma = \{0, \dots, d-1\}$. A string in $\Sigma^*$ is (almost) just a natural number written in base-$d$. The only problem is that leading zeroes are significant in strings but not natural numbers so we instead associate the string $w_1\dots w_k\in\Sigma^k$ with the base-$d$ natural number that's written $1w_1\dots w_k$. The length function is just a suitably rounded logarithm, which is primitive-recursive anyway.

(The first way you'd try to compute a base-$d$ logarithm would probably be to use a while loop to repeatedly divide by $d$. But you can replace that with a for loop, since we know that $\log_d n\leq n$.)

  • $\begingroup$ Some scheme like this should be useful for defining what primitive recursive functions with respect to natural numbers can compute with respect to finite strings. But I think one should consider more than just a single translation scheme, but instead consider some set of reasonable translation schemes, and show that they all give the same set of functions on finite strings. Alternatively, your scheme can also be considered as a way to define an order on the finite strings. And again, one would have to consider some set of reasonable order definitions, and show that they all give the same fkts. $\endgroup$ – Thomas Klimpel Feb 28 '17 at 12:32

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.