Decision procedure - sufficient condition and decidability #
We give a sufficient condition for a string to be derivable in the MIU language. Together with the
necessary condition, we use this to prove that
Derivable is an instance of
count I st and
count U st denote the number of
st : Miustr.
We'll show that
st is derivable if it has the form
x is a string of
count I x is congruent to 1 or 2 modulo 3.
To prove this, it suffices to show
Derivable M::y where
y is any
Miustr consisting only of
Is such that the number of
a = count I x and
b = count U x.
This suffices because Rule 3 permits us to change any string of three consecutive
Is into a
count I y = (count I x) + 3*(count U x) ≡ (count I x) [MOD 3], it suffices to show
Derivable M::z where
z is an
Is such that
count I z is congruent to
1 or 2 modulo 3.
z be such an
Miustr and let
count I z, so
c ≡ 1 or 2 [MOD 3].
To derive such an
Miustr, it suffices to derive an
M::w, where again
w is an
Miustr of only
Is with the additional conditions that
count I w is a power of 2, that
count I w ≥ c and that
count I w ≡ c [MOD 3].
To see that this suffices, note that we can remove triples of
Is from the end of
Us as we go along. Once the number of
m, we remove
Us two at a time
until we have no
Us. The only issue is that we may begin the removal process with an odd number
d = count I w, we see that this happens if and only if
(d-c)/3 is odd.
In this case, we must apply Rule 1 to
z, prior to removing triples of
Is. We thereby
introduce an additional
U and ensure that the final number of
Us will be even.
miu, decision procedure, decidability, decidable_pred, decidable
For any given natural number
c ≡ 1 or 2 [MOD 3], we need to show that can derive an
w consists only of
d = count I w is a power of 2, where
d ≥ c and
d ≡ c [MOD 3].
Given the above lemmas, the desired result reduces to an arithmetic result, given in the file
We'll use this result to show we can derive an
Miustr of the form
z is a string
consisting only of
Is such that
count I z ≡ 1 or 2 [MOD 3].
As an intermediate step, we show that derive
t is an
Miustr consisting of
an even number of
z is any
In fine-tuning my application of
simp, I issued the following commend to determine which lemmas
set_option trace.simplify.rewrite true
We may replace several consecutive occurrences of
"III" with the same number of
In application of the following lemma,
xs will either be
Decstr is a sufficient condition #
The remainder of this file sets up the proof that
Decstr en is sufficent to ensure
Derivable en. Decidability of
Derivable en is an easy consequence.
The proof proceeds by induction on the
count U of
We tackle first the base case of the induction. This requires auxiliary results giving
conditions under which
count I ys = length ys.
Before continuing to the proof of the induction step, we need other auxiliary results that
ind_hyp_suf is the inductive step of the sufficiency result.
By decidability, we can automatically determine whether any given