S ong No maliza ion o he Sa e F agmen o a Minimal Rew i e
Sys em:
A T iple-Lexicog aphic P oo and a Conjec u e on he
Unp o abili y o Full Te mina ion o Any Rela ional
Ope a o -Only TRS
Moses Rahnama
No embe 24, 2025
Abs ac
We p esen a minimal ope a o -only e m ew i ing sys em wi h se en cons uc o s and
eigh educ ion ules. Ou main con ibu ion is a mechanically- e i ied p oo o s ong
no maliza ion o a gua ded agmen using a no el iple-lexicog aphic measu e combining
a phase bi , mul ise o de ing (De showi z-Manna), and o dinal anking. F om s ong
no maliza ion, we de i e a ce i ied no malize wi h p o en o ali y and soundness. Assuming
local con luence ( e i ied h ough c i ical pai analysis), Newman’s Lemma yields con luence
and he e o e unique no mal o ms o he sa e agmen . We es ablish impossibili y esul s
showing ha simple measu es, such as addi i e coun e s, polynomial in e p e a ions, and
single-bi lags, p o ably ail o ules wi h e m duplica ion. The wo k demons a es
undamen al limi a ions in e mina ion p o ing o sel - e e en ial sys ems. We s a e a
conjec u e: no ela ional ope a o -only TRS can ha e i s ull-sys em e mina ion p o ed
by in e nally de inable me hods. He e “ ela ional” is equi alen o “capable o o de ed
compu a ion”: sys ems wi h a ecu so enabling i e a ion o e successo s, compa ison, o
sequen ial coun ing. Such ecu so s necessa ily edis ibu e s ep a gumen s ac oss ecu si e
calls, de ea ing all addi i e e mina ion measu es. This s uc u al limi a ion applies o any
TRS exp essi e enough o encode o de ed da a. All heo ems ha e been o mally e i ied in
a p oo assis an . The o mal de elopmen is a ailable o p og am commi ee membe s and
e e ees upon eques o pu poses o pee e iew.
1 In oduc ion
We de elop a minimal ope a o -only ew i e calculus (KO7): he objec language con ains only
cons uc o s and ope a o s wi h ew i e ules; he e a e no binde s, ypes, ex e nal axioms, o
seman ic p edica es. The ules a e he seman ics. Ou goals a e: (i) a clean, duplica ion- obus
p oo o s ong no maliza ion (SN); (ii) a ce i ied no malize ha always e u ns a no mal
o m; (iii) (op ionally) unique no mal o ms ia Newman’s Lemma unde a local-con luence
assump ion; and (i ) a conjec u e ha no ope a o -only TRS capable o o de ed compu a ion
can ha e i s ull-sys em e mina ion p o ed by in e nally de inable me hods.
Scope. All o mal esul s a e es ablished o a gua ded sa e sub ela ion. We do no claim a
single global measu e o he ull ungua ded ela ion. Mo eo e , we exhibi a p ecise nega i e:
a he oo peak
eqW a a
wi h
κM
(
a
) = 0, local join ails in he ull ela ion. The e o e he ull
ela ion is no locally con luen a ha peak, hence no con luen . The designed emedy is o
wo k in he sa e agmen wi h gua ded/con ex joine s (
§
6).
A second concep ual goal is o si ua e KO7 agains esul s abou ixed- a ge eachabili y
in e mina ing TRSs. I we de ine an in e nal p o abili y p edica e by “
educes o
⊤
”, hen
1
unde SN he se
{ | ⇒∗⊤}
is decidable by no maliza ion/back acking. Wi h con luence,
decision educes o no mal- o m equali y. This explains why single-le el G¨odel encodings canno
coexis wi h globally e mina ing p oo sea ch; he igh mo e is s a i ica ion.
Con ibu ions. (1) A duplica ion- obus SN p oo o KO7 using a iple-lex measu e wi h
a mul ise (DM) componen and an MPO-s yle head p ecedence; (2) a o al, p o ed-co ec
no malize ; (3) a gua ded Newman module o he sa e ela ion ha yields con luence (hence
unique no mal o ms) om SN + local con luence; (4) a decidabili y esul o eachabili y
unde SN; (5) a ca alog o impossibili y esul s o addi i e and polynomial measu es unde
duplica ion; (6) a o mal e i ica ion o all esul s; (7) a conjec u e on undecidable e mina ion
o ope a o -only sys ems wi hin a ixed base heo y.
Highligh s ( o maliza ion summa y).
SN (Sa eS ep) ia iple lex: Fo mally p o en using a lexicog aphic measu e combining a
δ-phase bi , a De showi z–Manna mul ise ank, and an o dinal.
Ce i ied no malize : A o al and sound no maliza ion unc ion is de ined by well- ounded
ecu sion.
Newman (Sa eS ep): Con luence is es ablished ia Newman’s Lemma using a e i ied local
con luence p ope y o he sa e agmen .
Full S ep ca ea : We exhibi a speci ic peak (
eqW a a
wi h
κM
(
a
) = 0) whe e local join
ails, jus i ying he es ic ion o he sa e sub ela ion.
Impossibili y esul s: The ailu e o simple addi i e and polynomial measu es is o mally
wi nessed by coun e examples.
2 Backg ound: TRSs, SN, eachabili y, and Newman
We assume s anda d abs ac educ ion and e m ew i ing no ions [
2
,
11
]. A e m is in no mal
o m i no ule applies. A TRS is s ongly no malizing (SN) i he e a e no in ini e educ ions.
A ela ion is con luen i o any
⇒∗u
and
⇒∗
he e exis s
w
wi h
u⇒∗w
and
⇒∗w
.
Local con luence equi es his only o single-s ep o ks. Newman’s Lemma asse s SN + local
con luence ⇒con luence [10], yielding unique no mal o ms.
Fixed- a ge (“small- e m”) eachabili y in e mina ing TRSs has well-cha ed complexi y:
NP-comple e o leng h- educing sys ems (d opping o P unde con luence), NExpTime/N2ExpTime
o (linea ) polynomial in e p e a ions, and PSPACE o KBO- e mina ing TRSs [
1
]. Modula i y
holds in ce ain linea , non-collapsing combina ions [
4
], while e en la non-linea sys ems exhibi
undecidable eachabili y and con luence [
9
]. Te mina ion unde duplica ion ypically equi es
o de s beyond plain sizes; a nai e size can inc ease unde duplica ing ules. The cu e is a mul ise
ex ension o a base o de [6] o ( ecu si e) pa h o de s [5].
3 The KO7 calculus
KO7 is a ini e TRS o e a small signa u e (7 cons uc o s) wi h 8 ules (including an explici
case spli on eqW). Fo conc e eness we lis he ule shapes below.
2
Rule Head A i y Shape Dup?
R1 me ge 2 me ge oid → No
R2 me ge 2 me ge oid → No
R3 me ge 2 me ge → No
R4 ec∆ 3 ec ∆ bs oid →bNo
R5 ec∆ 3 ec ∆ bs(del a n)→app s( ec ∆ b s n) No∗
R6 in eg a e 1 in eg a e (del a )→ oid No
R7 eqW 2 eqW aa→ oid No
R8 eqW 2 eqW ab→in eg a e (me ge a b) (i a=b) No
Table 1: KO7’s 8 ules. R7/R8 p o ide a comple e case spli on equali y. R3 is collapsing.
∗
R5
edis ibu es s o wo RHS posi ions.
Tiny example ( ace consequences). Using he e i ied no malize , we obse e:
In eg a e/del a: in eg a e(δ )⇒∗ oid ( e i ied).
Equali y (me a-le el consequence unde con luence):
–I n (a) = n (b) hen eqW a b ⇒∗ oid.
–O he wise eqW a b ⇒∗in eg a e(me ge a b).
No e: In he sa e agmen , con luence ensu es hese ou comes a e unique.
No e. We p o e SN and Newman-based con luence o he sa e agmen .
4 S ong no maliza ion
We de ine a iple-lexicog aphic measu e
µ3( ) := (δ- lag( ), κM( ), µo d( ))
o de ed by he lex p oduc o : (i) a phase bi d opping on he successo ecu sion; (ii) a mul ise
o anks
κM
(De showi z–Manna) wi h an explici p ecedence/s a us o ien ing edex
>
pieces;
and (iii) an o dinal payload
µo d
o non-duplica ing ies. O dinal haza ds a e s a ed explici ly
( igh -addi ion is no s ic ly mono one; abso p ion
α
+
β
=
β
equi es
ω≤β
). In duplica ing
b anches (i ex ended o b oade sys ems) we would use a compac MPO-s yle head p ecedence.
S ep s Sa eS ep (measu e uni ica ion). Fo he Sa eS ep ela ion we use a single uni ied
iple lex o de (
δ, κM, µo d
). Fo he ull ela ion we only p o ide a disjunc i e dec ease
ce i ica e: each s ep is co e ed by ei he a KO7 lex d op o an MPO iple d op. We do no
claim a single global well- ounded measu e o all ull s eps.
Theo em 1 (Pe -s ep dec ease (Sa eS ep)).Fo e e y ule ins ance
⇒ ′
in he gua ded
Sa eS ep ela ion, we ha e µ3( ′)<Lex µ3( ).
P oo idea. By ule head. Fo collapsing ules (e.g., me ge-cancel) we use he mul ise componen
wi h he chosen p ecedence so ha e e y RHS piece is s ic ly smalle han he emo ed LHS
edex in he base o de . Fo ec-succ he
δ
bi d ops (1
→
0). In he o maliza ion, each b anch is
a one-line dispa ched by a w appe lemma.
3
DM s MPO on ules (explici ). Fo me ge-cancel, we use a DM mul ise li o e a base
o de whe e
me ge
s ic ly domina es
. Fo eqW, we use a compac MPO-leaning measu e
whe e he head p ecedence o ien s eqW a b s ic ly abo e in eg a e(me ge a b).
Base-o de p emise (me ge-cancel): in
me ge →
, he RHS is s ic ly smalle han he
LHS.
Base-o de p emise (eqW): in
eqW a b →in eg a e
(
me ge a b
), he RHS is s ic ly smalle
unde head p ecedence.
No-Go o cons an bumps on κ(gene ic duplica o ).
Lemma 1 (No ixed +
k
o boolean lag o ien s a gene ic duplica o ).Le
κ
be a max-dep h-s yle
coun e and ix any
k∈N
. Fo a duplica ing ule o he shape
(
S
)
→C
[
S, S
](one edex eplaced
by wo occu ences o a sub e m
S
), he e exis s an ins ance whe e
κ
(
LHS
)
+k
=
κ
(
RHS
)
+k
, so
no s ic lex d op occu s. The same holds o a boolean phase lag alone.
P oo ske ch. Choose
S
wi h
κ
(
S
)
≥
1 and le
base
bound he con ex . Then
κ
(
LHS
) =
base+
1 while
κ
(
RHS
) =
max
(
κ
(
C
[
S
])
, κ
(
C
[
S
])) =
base+
1. Adding a ixed
k
p ese es equali y;
a single lag does no al e he ie. □
Rema k 1.In R5 ( ec-succ), he s ep a gumen
s
appea s once on he LHS and wice on he RHS:
once as he a gumen o
app
and once inside he ecu si e call. This s uc u al edis ibu ion
de ea s addi i e measu es when
s
con ains edexes. O ien a ion elies on he
δ
phase bi (1
→
0),
which d ops because he del a w appe is consumed.
Duplica ion s ess iden i y. Fo any addi i e coun e
ρ
ha coun s a single emo ed edex
and sums subpieces, gene ic duplica o s sa is y
ρ(a e ) = ρ(be o e) −1+ρ(S),
so he e is no s ic d op when
ρ
(
S
)
≥
1. The obus ix uses DM/MPO: eplace one elemen by
a mul ise o s ic ly smalle elemen s (DM), o use RPO/MPO wi h a p ecedence/s a us such
ha he LHS edex s ic ly domina es each RHS piece.
Co olla y 1 (S ong no maliza ion).The gua ded ela ion
Sa eS ep
o KO7 is s ongly
no malizing.
Genealogy o ailu es (why DM/MPO). We eco d minimal coun e pa e ns ha mo i a e
he mul ise /pa h componen s:
Pu e o dinal (µ) only: shape-blind bounds ail o sepa a e nes ed δ om i s con ex .
Addi i e bumps on κ: ies pe sis on duplica o s (Lemma 1).
Addi i e coun e s
ρ
: by he iden i y
ρ
(
a e
) =
ρ
(
be o e
)
−
1 +
ρ
(
S
) he e is no s ic d op
when ρ(S)≥1.
Polynomial in e p e a ions ha ely on impo ed a i hme ic o ha d-coded cons an s: he
duplica ing ules o ce case spli s ha canno be o ien ed wi hou s epping ou side he
ope a o language, so hese me hods ail wi hin he allowed in e nal oolbox.
The ix is DM/MPO: ensu e each RHS piece is s ic ly smalle han he emo ed edex in a base
o de and li ia a mul ise /pa h ex ension.
4
5 A ce i ied no malize
By well- ounded ecu sion on
µ3
we de ine a no maliza ion unc ion. We p o e he ollowing
p ope ies (sepa a ed o a oid o e ull lines):
(To ali y) ∀ ∃n. No malize( )=n
(Soundness) ∀ . no mal(No malize( )) ∧ ⇒∗No malize( ).
These a e exposed in he o maliza ion. We make no e iciency claim: wo s -case no maliza ion
cos ollows he e mina ion wi ness in play (c . he small- e m eachabili y bounds in [
1
]). In
con luen sys ems, decision educes o one no maliza ion and an equali y check.
6 Local con luence and Newman (gua ded sa e ela ion)
We discha ge local con luence by joining he ini e se o c i ical pai s (when p esen ). Combining
Co . 1 wi h Newman’s Lemma [10] yields:
Theo em 2 (Con luence and unique no mal o ms).I a ela ion is s ongly no malizing and
locally con luen , hen i is con luen . Hence e e y e m educes o a unique no mal o m.
Ins an ia ion (Sa eS ep). Combining Co . 1 (SN o
Sa eS ep
) wi h local-join lemmas yields
con luence and unique no mal o ms o he sa e agmen by Newman’s Lemma. In con as ,
he ull ela ion is no locally con luen a he oo peak
eqW a a
unde
κM
(
a
) = 0; hus ull
con luence does no hold. The
Sa eS ep
ela ion es ic s
eqW
o cases whe e a gumen s a e
gua ded, p e en ing his di e gence.
The s a -s a join p oo ollows he s anda d accessibili y (Acc) ecu sion a he sou ce, wi h
a case spli o e s a shapes (“head s ep + ail”) and composi ion ia ansi i i y. The module
also p o ides co olla ies o uniqueness o no mal o ms and equali y o no malize s unde s a .
Scope and Gua an ees ( o maliza ion-accu a e). We wo k wi h a gua ded sa e sub ela ion
Sa eS ep o which we p o e:
SN (Sa eS ep). The KO7 iple measu e
µ3
s ic ly d ops on e e y
Sa eS ep
. This yields
ace i ied no malize ha is o al and sound o he sa e agmen .
Local Con luence (Sa eS ep). We p o ide local-join lemmas pe oo shape and con ex
w appe s. Newman hen yields con luence and unique NFs o he sa e agmen .
Full S ep pe - ule dec eases (Hyb id). Fo each ke nel ule, he e is a pe -s ep dec ease
wi nessed ei he by KO7’s
δ/κM/µ
lex o by an MPO-leaning
µ
- i s iple. A uni o m global
agg ega o o all o S ep is le as u u e wo k.
C i ical-pai co e age. The ollowing able co e s he sa e oo con igu a ions wi h explici
local-join lemmas. This is exhaus i e o
Sa eS ep
excep he e lexi e
eqW a a
peak unde
κM
(
a
) = 0, which we show is no locally joinable a he oo . We discha ge many
eqW
cases ia
gua ded/con ex w appe s.
5
Sou ce Lemma
in eg a e(δ )localJoin in del a (unique a ge oid)
me ge oid localJoin me ge oid le (unique a ge )
me ge oid localJoin me ge oid igh (unique a ge )
me ge localJoin me ge (unique a ge )
ec ∆ bs oid localJoin ec ze o (unique a ge b)
ec ∆ bs(δ n)localJoin ec succ (unique a ge app s( ec ∆ bsn))
eqW a b, a =blocalJoin eqW ne (unique a ge in eg a e(me ge a b))
eqW a a, κM(a) = 0 no locally joinable a oo
Gua ded a ian s exclude spu ious b anches. Con ex ual w appe s li oo joins o con ex .
δ
-gua d: de ini ion and decidabili y. De ine he sa e-phase p edica e by
δ-gua d
(
)
⇐⇒
δFlag
(
) = 0. He e
δFlag
:
Te m →N
is a s uc u ally ecu si e unc ion de ined on e ms in
he a i ac ( acking spli pa i y), so he p edica e is decidable. Fac s:
δFlag
(
eqW a b
) = 0;
me ge- oid ules equi e δFlag( ) = 0.
Tiny δ- lag walk- h ough (1→0).
ec ∆ b s (δ n) app s( ec ∆ b s n)
δ- lag d op
7 Impossibili y esul s
We o mally es ablish he ailu e o se e al simple measu e s a egies, which necessi a e he use
o DM mul ise o de s o MPO. These nega i e esul s a e e i ied in he o mal de elopmen .
Addi i e bumps ail: No measu e o he o m
κ
(
) +
k
s ic ly dec eases on gene ic
duplica ing ules.
Ba e lags ail: A single boolean lag is insu icien o o ien ules ha li dep h.
Polynomial in e p e a ions ail: Any polynomial in e p e a ion in ol ing ixed cons an s
equi es ex e nal a i hme ic axioms o “o ien ” he ule, iola ing he ope a o -only cons ain .
Polynomial Impossibili y. Conside polynomial in e p e a ions o he o m
M
(
)
∈N
o a
duplica ing ule
(
x
)
→g
(
x, x
). A polynomial measu e assigning
M
(
(
x
)) =
M
(
x
) +
p
equi es
M(x)+p>2M(x) o s ic dec ease, implying p > M(x). This ails o unbounded M(x).
Mo e gene ally: any polynomial p oo o a sys em wi h duplica ing ules mus ha dcode
speci ic cons an s (e.g.,
M
(
oid
) = 2) o sa is y inequali ies like 2
M
(
s
)
> M
(
s
) + 1. Such
p oo s impo ex e nal a i hme ic p ope ies and impose a bi a y alues on ope a o s, iola ing
he p inciple ha ope a o s’ seman ics should be de ined solely by ew i e ules. Changing
he ha dcoded cons an (e.g.,
M
(
oid
) = 1) collapses he p oo . This s uc u al ailu e is why
polynomial in e p e a ions canno o ien gene ic duplica ing ules wi hou ex e nal axioms.
In e nally de inable measu es. We use a simple con ac o in e nally de ined e mina ion
measu es o s uc u e hese nega i e esul s:
De ini ion 1 (In e nally de inable measu e).An in e nally de inable measu e o a ype
α
consis s o (
β, < β, w ,m,c xMono,piecesL
)whe e:
β
is a base o de ca ie ;
< β
is a
well- ounded ela ion wi h wi ness
w
;
m
:
α→β
is he measu e;
c xMono
exp esses con ex
compa ibili y; and
piecesL
asse s ha in each ule ins ance, e e y RHS piece is s ic ly smalle
han he emo ed LHS edex w. . . < β.
6
8 Decidabili y o Reachabili y
Theo em 3 (Fixed- a ge eachabili y).In a s ongly no malizing TRS, he se
{ | ⇒∗c}
o
any cons an cis decidable ia no maliza ion.
This connec s ou wo k o classical esul s: i we could encode undecidable p ope ies
h ough educ ion o cons an s, we would iola e known heo e ical limi s. This mo i a es
s a i ied app oaches in p oo assis an s, whe e objec -le el and me a-le el easoning a e ca e ully
sepa a ed.
Assump ions (model). We wo k wi h a ini e i s -o de TRS o e ini e e ms. The decision
me hod is: compu e a no mal o m (by SN) and check whe he i is
⊤
; wi h local con luence,
his educes o one no maliza ion and an equali y es .
Complexi y con ex . Small- e m eachabili y in e mina ing TRSs anges om NP (leng h-
educing) o NExpTime/N2ExpTime (polynomial in e p e a ions) and PSPACE (KBO), wi h
con luence lowe ing he leng h- educing class o P [
1
]. This si ua es ou “no malize and compa e”
decision p ocedu e o KO7 wi hin he es ablished landscape.
Mo eo e , decidabili y can be modula o disjoin unions unde le -linea i y/non-collapsing
assump ions [
4
], while e mina ion alone does no gua an ee decidabili y: e en la non-linea
TRSs ha e undecidable eachabili y/joinabili y/con luence [9].
9
Conjec u e: Full Te mina ion o Any Rela ional Ope a o -
Only TRS
Wha “ ela ional” means. A ela ional ope a o -only TRS is, by de ini ion, one capable o
o de ed compu a ion. The e ms a e equi alen : “ ela ional” = “capable o o de ed compu a ion.”
Such sys ems can exp ess i e a ion o e successo s, compa ison o s uc u e dep hs, o any o m
o sequen ial coun ing. The minimal signa u e o such capabili y includes a ecu so , an ope a o
ha applies a s ep unc ion i e a i ely ac oss a successo -s uc u ed a gumen . Examples include
p imi i e ecu sion o e na u al numbe s, old o e lis s, and any cons uc ha s eps h ough an
o de ed index. A TRS ha canno exp ess such i e a ion (e.g., a la pa e n-ma ching sys em
wi h no ecu si e s uc u e) is no ela ional in his sense.
The c i ical p ope y o ela ional sys ems is ha hei ecu so edis ibu es i s s ep a gumen
ac oss ecu si e calls. This edis ibu ion is no op ional: i is wha makes o de ed compu a ion
possible. Bu i also de ea s all addi i e e mina ion measu es.
The s uc u al ba ie . Any ope a o sys em capable o o de ed compu a ion equi es a
ecu so . A ecu so edis ibu es i s s ep a gumen ac oss ecu si e calls. This edis ibu ion
de ea s addi i e e mina ion measu es:
M
(
a e
) =
M
(
be o e
)
−
1 +
M
(
s
), yielding no s ic
d op when M(s)≥1.
De ini ion 2 (In e nally de inable measu e).An in e nally de inable e mina ion me hod o
signa u e Σuses only: simpli ica ion o de s wi h ixed p ecedence/s a us on Σ(LPO/RPO/MPO),
DM-mul ise li s o
N
- alued anks, and algeb aic in e p e a ions de inable wi hou impo ing
ex e nal axioms. No encodings in o ex e nal a i hme ic, no bo owed logic, and no ha d-coded
cons an s ou side he ope a o language.
Conjec u e 1 (Full Te mina ion Conjec u e o Rela ional TRSs).No ela ional ope a o -only
TRS can ha e i s ull-sys em e mina ion p o ed by in e nally de inable me hods. Speci ically: le
Rbe an ope a o -only TRS wi h a ecu so ule o he o m
ec(b, s, σ(n)) → (s, ec(b, s, n)).
7
No in e nally de inable measu e (De ini ion 2) p o es e mina ion o
R
when he s ep a gumen
s
is
un es ic ed. The s uc u al edis ibu ion o
s
in o bo h he unc ion applica ion and he ecu si e
call de ea s e e y addi i e, polynomial, o pa h-o de measu e ha does no impo ex e nal
a i hme ic o o dinal axioms. Any p oo ha elies on ex e nal axioms, impo ed a i hme ic, o
me a-le el encodings is ou side scope and does no coun as an in e nal e mina ion a gumen .
Scope o he conjec u e. The conjec u e applies o any TRS exp essi e enough o encode
o de ed da a (na u al numbe s, lis s, ees wi h successo s uc u e, o any ype suppo ing
i e a ion). Sys ems wi hou such s uc u e (pu ely g ound, non- ecu si e, o lacking a s ep-
i e a ion pa e n) all ou side he conjec u e’s scope. The claim is ha once a sys em has enough
s uc u e o o de ed compu a ion, i s ull e mina ion escapes in e nal p oo me hods.
E idence. In KO7, he
ec-succ
ule has he c i ical shape: he s ep a gumen
s
appea s
wice on he RHS, and when
s
con ains nes ed edexes, e e y addi i e measu e ails o dec ease
s ic ly. The edis ibu ion iden i y
M
(
a e
) =
M
(
be o e
)
−
1 +
M
(
s
) yields no s ic d op
when
M
(
s
)
≥
1. The gua ded Sa eS ep agmen e mina es because he
δ
-phase bi es ic s
allowable s ep a gumen s; wi hou such es ic ion, he ull sys em admi s unbounded ecu si e
dep h. The gap be ween in e nally de inable anking unc ions and wha would be equi ed
canno be closed wi hou ex e nal me hods (axioms, encodings, o bo owed a i hme ic).
10 Fo maliza ion s uc u e
The o mal e i ica ion is implemen ed in a p oo assis an . The p ojec s uc u e sepa a es he
ke nel de ini ions, me a- heo y p oo s, and impossibili y esul s:
Te mina ion p oo s: Es ablishes he pe - ule dec eases and s ong no maliza ion o he
sa e agmen using he iple-lexicog aphic measu e.
No maliza ion: De ines he no maliza ion unc ion and p o es i s o ali y and soundness.
Con luence: Implemen s he Newman engine and he s a -s a join, elying on local join
lemmas.
Impossibili y esul s: Con ains he e i ied coun e examples o addi i e measu es and he
p oo s ha simple measu es ail unde duplica ion.
All claimed esul s a e o mally p o en wi hou eliance on unp o en pos ula es in he cu en
build. The o mal de elopmen is a ailable o e iewe s unde app op ia e con iden iali y
ag eemen s.
Re e ences
[1]
F anz Baade and J”u gen Giesl. On he complexi y o he small e m eachabili y p oblem o
e mina ing ss. In FSCD 2024, olume 299 o LIPIcs, pages 16:1–16:18, 2024.
[2]
F anz Baade and Tobias Nipkow. Te m Rew i ing and All Tha . Camb idge Uni e si y P ess, 1998.
[3]
Wil ied Buchholz. A new sys em o p oo - heo e ic o dinal unc ions. Annals o Pu e and Applied
Logic, 32(3):195–207, 1986.
[4]
Anne-Ca he ine Ca on and Jean-Louis Coquid´e. Decidabili y o eachabili y o disjoin union o
e m ew i ing sys ems. Theo e ical Compu e Science, 126(1):31–52, 1994.
8
[5]
Nachum De showi z. Te mina ion o ew i ing. Jou nal o Symbolic Compu a ion, 3(1–2):69–116,
1987.
[6]
Nachum De showi z and Zoha Manna. P o ing e mina ion wi h mul ise o de ings. Communica ions
o he ACM, 22(8):465–476, 1979.
[7] R. L. Goods ein. On he es ic ed o dinal heo em. Jou nal o Symbolic Logic, 9(2):33–41, 1944.
[8]
Lau ence Ki by and Je Pa is. Accessible independence esul s o peano a i hme ic. Bulle in o he
London Ma hema ical Socie y, 14(4):285–293, 1982.
[9]
Isao Mi suhashi, Masahi o Oyamaguchi, and Flo en Jacquema d. The con luence p oblem o la
ss. In AISC 2006, olume 4120 o LNCS, pages 73–84, 2006.
[10]
M. H. A. Newman. On heo ies wi h a combina o ial de ini ion o “equi alence”. Annals o
Ma hema ics, 43(2):223–243, 1942.
[11] Te ese. Te m Rew i ing Sys ems. Camb idge Uni e si y P ess, 2003.
Appendix: Addendum
KO7 Rules Table (7 cons uc o s, 8 ules)
Rule Head A i y Shape Dup?
R1 me ge 2 me ge oid → No
R2 me ge 2 me ge oid → No
R3 me ge 2 me ge → No
R4 ec∆ 3 ec ∆ bs oid →bNo
R5 ec∆ 3 ec ∆ bs(del a n)→app s( ec ∆ b s n) No∗
R6 in eg a e 1 in eg a e (del a )→ oid No
R7 eqW 2 eqW aa→ oid No
R8 eqW 2 eqW ab→in eg a e (me ge a b) (i a=b) No
Table 2: KO7’s 8 ules. R7/R8 p o ide a comple e case spli on equali y. R3 is collapsing (e ases
one copy). ∗R5 edis ibu es s o wo posi ions on he RHS; see Rema k below.
T iple-lexicog aphic measu e and duplica ion handling (DM/MPO)
We o de µ3( ) = (δ- lag( ), κM( ), µo d( )) by lex:
δ- lag: phase bi d opping on he successo ecu sion b anch.
Mul ise
κM
: a De showi z–Manna mul ise ex ension o e a base p ecedence/s a us (o
MPO head p ecedence) o ien ing edexes s ic ly abo e pieces; co e s duplica o s.
O dinal
µo d
: esol es non-duplica ing ies; igh -addi ion is no s ic ly mono one; abso p ion
α+β=βneeds ω≤β.
Pe - ule lemmas show e e y RHS componen is s ic ly smalle han he emo ed edex in he
base o de .
9
