Subject: Many-one reducible notes
Date: Thu, 09 Nov 1995 21:17:37 EST
From: J Corrales <jaybyrd@MIT.EDU>

(notes from lecture Oct 25, 1995)

Many-One Reducibility 
---------------------

Definition:

	A set A of expressions is called many-one reducible (also called
mapping reducible) to a set B of expressions, denoted

	A <=m B, 

iff there is a computable, total function f such that a e A iff f(a) e B
for all expressions a.
	The function f is called the reduction of A to B.

This is a very restrictive notion of reducibility. There are broader
notions of reducibility, in which, for instance, multiple expressions in
A are mapped to a single expression in B. ??

Note that set-theoretic containment doesn't have much to do with
reducibility/decidability.

Consider, for instance, the set of all legal Scheme expressions. This
set is decidable, since any legal Scheme expression can be parsed by a
Scheme interpreter/compiler; many of its subsets (e.g. Halts, or any
other nontrivial, evaluation-invariant property) are not decidable,
however.

Example of a many-one reduction:

The following Scheme procedure f is (computes?) a reduction from ~Halts
= NotHalts to True:

	(define (f exp)
	   (list exp '= `(spin)))

For any expression M, f(M) e True iff exp e ~Halt (i.e., iff evaluation
of M is non-halting):

	If exp e NotHalts, exp is observationally congruent to (spin),
so that the expression (f exp) ::= "exp = (spin)" is true in the proof
system =func.  Conversely, if "exp = (spin)" is true, i.e., in True,
then exp must be in NotHalts.

Remark:

	A is not many-one reducible to ~A (complement of A).


(notes from lecture Nov 1, 1995)

~Halts = NotHalts <=m True:

We showed that NotHalts is many-one reducible to True via the following
reduction procedure f:

	(define (f exp)
	   (list exp '= `(spin)))
	
	In equational notation, f("M") ::= "M = '(spin)"   ??


Halts <=m True:

Halts is many-one reducible to True. A many-one reduction f from Halts
to True can be defined as follows:

	f("M") ::= "(if M 3 3) = 3"
	
	In Scheme, / The following Scheme procedure computes (is?) f:

	(define (f exp)
	   (list (list 'if exp 3 3) '= 3))


True is not half-decidable; this follows, according to the following
lemma, from the fact that NotHalts is not half-decidable and the
many-one reducibility of NotHalts to True.

Lemma: 

	If S1 <=m S2 and S2 is half-decidable, then S1 is half-decidable.

In colloquial terms, we might say that half-decidability inherits
"downward" through reducibility from "harder" sets to "easier" sets; in
other words, if we can half-decide a "hard" set, we can half-decide an
"easier" set, i.e., one that (many-one) reduces to the "hard" set.
  
Proof:

know: M e S1 iff f(M) e S2.
have: half-decide-S2, a half-decider for S2
have: procedure f-proc which computes f

want: half-decide-S1, a half-decider for S1

Here it is:

	(define (half-decide-S1 exp)
	   (half-decide-S2 (f-proc exp)))

Put in contrapositive form, the lemma reads

	If S1 <= S2 and S1 is not half-decidable, then neither is S2.

We can establish an analogous lemma for the inheritance of decidability,
i.e. if S1 <=m S2 and S2 is decidable, then S1 is decidable. The proof
is analogous to that of the preceding lemma, with deciders instead of
half-deciders.

Lemma: 

	S1 <=m S2 iff  ~S1 <=m ~S2

Proof: 

By definition, S1 <=m S2 means that M e S1 iff f(M) e S2, for all M.  In
contrapositive form with clauses swapped across the iff: M ~e S1 iff
f(M) ~e S2, for all M. Equivalently, "M e ~S1 iff f(M) e ~S2, for all
M."  Thus, by definition of many-one reducibility. ~S1 <=m ~S2.

Thus, NotHalts = ~Halts <=m ~True since Halts <=m True.
Similarly, Halts = ~NotHalts <=m ~True  since Nothalts <=m True.


Corollary:	Halts <m True (meaning Halts <=m True and True ~<=m Halts) 
Proof:  

We have established that Halts <=m True. To show that True ~<=m Halts,
we assume for the purpose of obtaining a contradiction that True <=m
Halts. Since Halts is half-decidable, the hypotheses of the lemma above
are satisfied and we have, according to that lemma, that True is
half-decidable. But we have shown that True is not half-decidable. This
is a contradiction. Our assumption, therefore, was false, i.e. True ~<=m
Halts.

Corollary:

	NotHalts <m True (meaning NotHalts <=m True and True ~<=m
NotHalts)

Proof:

	We have established that NotHalts <=m True. To show that True
~<=m NotHalts, we assume for the purpose of obtaining of contradiction
that True <=m NotHalts. Since complementation preserves reducibility, it
follow that ~True <=m ~NotHalts = Halts. The half-decidability of Halts
implies via the lemma above that ~True is half-decidbale, a
contradiction, since ~True is not half-decidable, as the following
argument shows: We have established that Halts <=m True. Complementing
both Halts and True we obtain NotHalts <=m ~True. NotHalts is not
half-decidable. It follows from the lemma above that ~True is not
half-decidable.


We have seen that neither True nor ~True = False is half-decidable, in
other words, that True is neither half-decidable (recursively
enumberable) nor co-half-decidable (recursively co-enumberable).  (cf.
Halts. Halts is half-decidable but not co-half-decidable).


Undecidable problems (which don't pertain directly to the behavior of
programs)

1.	Hilbert's 10th problem

2.	Given a finite set of 3x3 interger matrices, is there a product
of them (with repetitions allowed) equal to the 0 matrix? (this problem
is half-decidable)

3.	Does a BNF grammar define the set of all strings over its
alphabet?

4.	Is a BNF grammar ambiguous?

5.	Given a finite number of axioms of string equation form , e.g.
abac = cab, cca = ccb, and another string equation, does the new string
equation follow(in the sense of either truth or provability, which are
equivalent for string equations) from the original set of axioms?

abac = cab  } geometric properties
 cca = ccb  }

a, b, c = symbols


Truth == Provable in the case of string equations.

 s = t
-------
as = at ?  == undecidable

-------

Halts <=m True
~Halts <=m ~True

Equation Between Strings

Alphabet = {a, b, c}

axiom:	ab = ba
        -------
     aabca ?= baaca
      ^^
     called redex

     abaca => baaca

Thus, aabca = baacb

Def: Invariant is a property of strings that doesn't change after
rewriting. 

The invariant for the above writing is that, "the position of the 'c'
character does not change after a rewriting application".  In other
words the number of c's does not change.

{ ((= s1 s2) E) | s1 ->(E*) s2, s1 ->(E*) s2 } is half-decidable.  

Uniform String Rewriting Problem is undecidable

E ::= {(= s1 s2) | s1 ->(E*) s2}

String rewriting problem for {ab = ba} is decidable.

....c....
 ^^   ^^^^
 same number of a's b'c and c's => not possible to turn into different
numbers of c's.

Canonical Form for String Equations

a*b*(ca*b*)* = set of strings that match this pattern.

i.e. a^0b^0c^1a^3c^1a^2b^7c^1b^1

Never see an "a" following a "b".

Sub Lemma's:

1.	For every string s, there is a canonical form, s^, such that s =
s^, under the axiom (ab = ba)*.
2.	Syntatically distinct canonical forms are not (ab = ba)*. I.e.
s1  =/= s2  => Canonical form 1 =/= Canonical form 2. 


To prove two canonical forms are equivalent: (not sure which ones)

1.	Apply equation until there are no more (ba)'s.
2.	A size => which measures # of b's left of a.  
3.	Show that this size decreases with the number of inversions
made. 

String (Group) Theory

Over + (group)
------
x + y = y + x		Commutative
....			Associative
x + 0 = x		Identity
x - x = 0		Inverse

Over * (semi - group)
------
x * y = y * x		Commutative
....			Associative
x * 1 = x		Identity

x * (y + z) = x * y + x * z

-1 * x = -x		Theorem of negatives and identity

Examples: 

7 + 1 = 8
11 * (-3) = -33

All primative rules for addition is an infinite set, but decidable.

Claim:
	
	There is a decidable set of axioms.

Write sum, monomials.  Define a canonical form for monomials
(polynomials).  

----------
  _            _                _    _w_
 <_> ___  _ _ | |_  _ _  _ _  _| |  (o o)
 | |<_> || | || . \| | || '_>/ . | (  `  )
 | |<___|`_. ||___/`_. ||_|  \___|/--m-m-
<_ '     <__ '     <__ '             \W/