Re: 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 straight-forward approach.

A back-of-the-envelope 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 honest-to-goodness regular expressions?

Probably not. You should be able to evaluate an SK-expression from the bottom up (instead of top-down) if it is fully parenthesized. Something like this:

s/\(S([^()])([^()])([^()])\)/($1($3($2$3)))/;
s/\(K([^()])([^()])\)/$1/;
s/\(I([^()])\)/$1/;
[download]

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 SK-expression simulate a Turing machine M on input x. Is it equivalent to the SK-expression that always returns true?

blokhead

Comment on Re: Turing completeness and regular expressions Download Code

Replies are listed 'Best First'.
Re^2: Turing completeness and regular expressions by JadeNB (Chaplain) on Nov 28, 2009 at 17:41 UTC
Probably not. You should be able to evaluate an SK-expression from the bottom up (instead of top-down) if it is fully parenthesized. Something like this: `s/$S([^()])([^()])([^()])$/($1($3($2$3)))/; s/$K([^()])([^()])$/$1/; s/$I([^()])$/$1/;` [download] 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. I think that this does not work. For example, it does not reduce `((K((SK)K))K)` to `(SK)K` (UPDATE: or, better, `(((K((SK)K))K)x)` to `x`). 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 SK-expression simulate a Turing machine M on input x. Is it equivalent to the SK-expression that always returns true? Yes, that's what I thought; but Stenlund provides a finite system of equations for deciding—well, something. I thought that it was functional equivalence, but I must have misunderstood. I'll look it up when I've got my copy. (Incidentally, the combinator is `KK`.)	[reply] [d/l] [select]
Re^3: Turing completeness and regular expressions by blokhead (Monsignor) on Nov 28, 2009 at 17:52 UTC
You may be right about bottom-up evaluation of SK expressions. Larger terms must be treated as first-class objects to be passed around, etc. But we both missed the obvious way to just use "plain" regex substitutions to simulate Turing-completeness: unrestricted (type-0) grammars. They are basically defined as the repeated evaluation of plain regex substitutions, and are Turing-complete. A universal TM converted to a type-0 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). blokhead	[reply]
Re^4: Turing completeness and regular expressions by JadeNB (Chaplain) on Nov 28, 2009 at 18:00 UTC
But we both missed the obvious way to just use "plain" regex substitutions to simulate Turing-completeness: unrestricted (type-0) grammars. They are basically defined as the repeated evaluation of plain regex substitutions, and are Turing-complete. A universal TM converted to a type-0 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 re-writing 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 look-up table (built into the string on which the substitution acts). Am I missing your point?	[reply]
Re^5: Turing completeness and regular expressions by blokhead (Monsignor) on Nov 28, 2009 at 18:20 UTC
Re^6: Turing completeness and regular expressions by JadeNB (Chaplain) on Nov 28, 2009 at 18:34 UTC
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 SK-expression simulate a Turing machine M on input x. Is it equivalent to the SK-expression 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 higher-order 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]


Welcome to the Monastery
	PerlMonks