Re: Computability and logic

Tom wrote:
MoeBlee wrote:
Tom wrote:
Please, may I ask for a reading suggestion, as well as, perhaps, some
kind commentary, as regards a mathematical formulation of a substring
replacement?

Are you asking for a rigorous mathematical definition of replacing a
substring in a string with another substring?

Yes please, Moe.

It seems to me that there are at least two methods in the context I
just described.

One method is to use "dummy variables". For example, suppose we want to
replace the term t in the formula P with the term t' (P is a string and
t and t' are strings). Then we choose (with certain technical
restrictions) a dummy variable, say v (which is a string of exactly one
symbol). Meanwhile, by recursion, we will have already defined 'the
result of substituting a term for a variable in a formula'. That
recursive definition will be easy since we are substituting a term
(which is a string of possibly many symbols) for a variable (which is a
single symbol), and such "many for one" substitutions are easy to do
recursively. The notation for this will look like:

We set P to
P'[t|v]
where v is a variable not in P.

In other words, P has the term t in P all along, but we "mark" where t
occurs in P by "pretending" that t is substituted for v everywhere v
occurs in P'; so v marks where t occurs.

Then the result of substituting a term t' for term t in a formula P
will be be the formula:

P'[t'|v]

In other words, instead of v marking where t occurs, now v marks where
t' occurs, and t' occurs exactly where t occured, viz. where v
occurred.

I'm leaving out some of the technicalities, but this is the general
idea. I suggest Enderton's 'A Mathematical Introduction To Logic' for
background. As I recall, he doesn't get into replacing term for term,
but he does explain replacing term for variable, which is the first
step needed. And van Dalen's 'Logic And Structure' discusses the dummy
variable technique.

Another method is more general but more complicated (I haven't gone
through the details myself). Say we want to substitute a string t' for
a substring t in a string s (t, t', and s being any strings, not
necessarily terms and formulas). Then we note the positions that t
occupies in s (e.g., in the string 'xxyzuvwyzux', the substring 'yzu'
occupies positions 3-5 and positions 8-10). Then we note the length of
t'. Then we concatenate:
positions 1-2 of t with
t' with
positions 6-7 of t with
t' with
position 11 of t.

Formalizing a GENERAL definition of such a concatenation operation
would be somewhat complicated, but I am pretty sure that it can be
done, especially since computer programs such as word processors do
those kinds of concatenations (e.g., substituting a word for another
word throughout a document).

MoeBlee

.

Relevant Pages

  • Re: Computability and logic
    ... say v (which is a string of exactly one ... substring replacement) to be predefined. ... substituting a formula for a sentence letter in a formula; ... to come to grips with such technicalities as rigorous definitions for ...
    (sci.logic)
  • Re: Computability and logic
    ... say v (which is a string of exactly one ... substring replacement) to be predefined. ... substituting a formula for a sentence letter in a formula; ... to come to grips with such technicalities as rigorous definitions for ...
    (sci.logic)
  • Re: Computability and logic
    ... substituting a formula for a sentence letter in a formula; ... We substitute a string that may be ... occupies in s (e.g., in the string 'xxyzuvwyzux', the substring 'yzu' ... Still, no presupposition about subsitution. ...
    (sci.logic)
  • Re: Substring Substitution
    ... Rob Myers wrote: ... > I would like to replace a substring with a string of a different ... Can't re-substitute after substituting once. ...
    (comp.lang.prolog)
  • Re: Replacing subsequences
    ... Chris Capel wrote: ... > different substring, of a different length ... quick and simple replacing of text in a string: ...
    (comp.lang.lisp)