in reply to Turing completeness and regular expressions
Formalise the idea that, even with recursion, regexes aren't Turing complete.
I think your approach of looking at the space required to simulate recursive regexes is the most straightforward approach.
A backoftheenvelope calculation is as follows: the "state" that describes the regex evaluation consists of a stack. Each level in the stack corresponds to a nonterminal (i.e., regex to match at this recursive level), a position in the original string, and any captures and alternations already made by the regex. You can stop simulating this branch of the regex match every time the stack contains a repeated configuration, since if the regex will eventually match, then it must also match using a stack with no repeats. So you are only bound by the number of distinct stack configurations. Say, (# of nonterminals * length of string * 2^(# alternations in the regex) * (length of string)^(2 * # of captures)). The last term is to store a "start" and "end" pointer for each capture.
Whatever this comes out to be, it is some fixed function of the input size (I guess in the EXPSPACE family), so there is some fixed space bound.
By the Space hierarchy theorem, there are always languages that require more space.
Do we need anything more than honesttogoodness regular expressions?
Probably not. You should be able to evaluate an SKexpression from the bottom up (instead of topdown) if it is fully parenthesized. Something like this:
s/\(S([^()])([^()])([^()])\)/($1($3($2$3)))/;
s/\(K([^()])([^()])\)/$1/;
s/\(I([^()])\)/$1/;
i.e., always evaluate the "innermost" expression, which will be the one without parentheses. I think something like this may work though I've not tested it.
Set up a recursive substitution to recognise functional equivalence of combinators (so that it could identify ``SKK and ``SKS as functionally equivalent).
Equivalent to the halting problem in the general case. Let an SKexpression simulate a Turing machine M on input x. Is it equivalent to the SKexpression that always returns true?
Re^2: Turing completeness and regular expressions by JadeNB (Chaplain) on Nov 28, 2009 at 17:41 UTC 
 [reply] [d/l] [select] 

You may be right about bottomup evaluation of SK expressions. Larger terms must be treated as firstclass objects to be passed around, etc.
But we both missed the obvious way to just use "plain" regex substitutions to simulate Turingcompleteness: unrestricted (type0) grammars. They are basically defined as the repeated evaluation of plain regex substitutions, and are Turingcomplete. A universal TM converted to a type0 grammar will only have a finite number of substitution rules, and you can simulate it with a substitution + finite lookup table (or a finite # of separate s/// statements).
 [reply] 

But we both missed the obvious way to just use "plain" regex substitutions to simulate Turingcompleteness: unrestricted (type0) grammars. They are basically defined as the repeated evaluation of plain regex substitutions, and are Turingcomplete. A universal TM converted to a type0 grammar will only have a finite number of substitution rules, and you can simulate it with a substitution + finite lookup table (or a finite # of separate s/// statements).
I didn't know about this, but I'm not sure that it's quite right to say that I missed it completely; indeed, the two wodges of code I wrote are just implementing systems of rewriting rules, which it seems to me are the same as unrestricted grammars, and the way that I did it is with a substitution plus a finite lookup table (built into the string on which the substitution acts). Am I missing your point?
 [reply] 


Re^2: Turing completeness and regular expressions by JadeNB (Chaplain) on Dec 03, 2009 at 16:13 UTC 
Set up a recursive substitution to recognise functional equivalence of combinators (so that it could identify ``SKK and ``SKS as functionally equivalent).
Equivalent to the halting problem in the general case. Let an SKexpression simulate a Turing machine M on input x. Is it equivalent to the SKexpression that always returns true?
Ah, now I see what I had wrong.
Stenlund mentions in “Combinators, λterms, and proof theory” (and I get the impression from the historical section of Introduction to higherorder categorical logic that this dates back to Curry) a finite equational axiomatisation of what I'm calling functional equivalence (and he calls extensional, or η, equality), namely:
 S
 ```Sxyz = ``xz`yz
 K
 ``Kxy = x
 I
 `Ix = x
 c1
 `S`KI = I
 c2
 ``BS`S`KK = K
 c3
 ```B`B``B`BSSBS = ``P```B`BSBSS
 c4
 ``B``S``BBS`KKK = `BK
 c4
 `S`KI = ``SB`KI
where he takes I as a primitive combinator, B = ``S`KSK is as above, and ````Pfgxy = ``f`gx`gy. (One usually writes Ψ instead of P, but I don't know how to get entities inside code tags. :) )
However: Having a finite axiomatisation of a theory is not the same as being able to decide the truth of an arbitrary proposition in that theory—witness Peano arithmetic—and that, of course, is where my ambition smacks against your refusal to solve the halting problem. :)
 [reply] [d/l] [select] 

