Nicelik belirteci eliminasyonu - Quantifier elimination

Niceleyici eliminasyonu , matematiksel mantık , model teorisi ve teorik bilgisayar biliminde kullanılan bir basitleştirme kavramıdır . Gayri resmi olarak, " böyle " niceliksel bir ifade, "Ne zaman böyle bir şey var ?" Sorusu olarak görülebilir ve nicelik belirteçleri içermeyen ifade, bu sorunun cevabı olarak görülebilir. ${\ displaystyle \ var x}$ ${\ displaystyle \ ldots}$ ${\ displaystyle x}$ ${\ displaystyle \ ldots}$

Formülleri sınıflandırmanın bir yolu , miktar miktarına göredir . Daha az niceleyici değişimi derinliğine sahip formüllerin daha basit olduğu, niceleyici içermeyen formüllerin en basit olduğu düşünülür. Bir teorinin niceleyici eliminasyonu vardır, eğer her formül için ona eşdeğer niceleyici içermeyen başka bir formül varsa ( modulo bu teori). ${\görüntüleme stili \alfa }$ ${\ displaystyle \ alpha _ {QF}}$

Örnekler

Lise matematiğinden bir örnek, tek değişkenli ikinci dereceden bir polinomun , ancak ve ancak ayırıcı negatif değilse gerçek bir köke sahip olduğunu söylüyor :

{\ displaystyle \ mathbb {R} 'de x \ var. (a \ neq 0 \ kama balta ^ {2} + bx + c = 0) \ \ \ Longleftrightarrow \ \ a \ neq 0 \ kama b ^ {2} -4ac \ geq 0}

Burada sol taraftaki cümle bir nicelik belirteci içerirken, sağdaki eşdeğer cümle içermez. ${\ displaystyle \, \ mathbb {R} 'de x \ var}}$

Nicelik belirleyici eliminasyonu kullanılarak karar verilebilir gösterilen teorilerin örnekleri, Presburger aritmetiği , cebirsel olarak kapalı alanlar , gerçek kapalı alanlar , atomsuz Boole cebirleri , terim cebirleri , yoğun doğrusal sıralar , değişmeli gruplar , rastgele grafikler ve bunların Boolean gibi birçok kombinasyonudur. Presburger aritmetik ve ile vadeli cebirlerin ile cebir kuyruklar .

Sıralı bir toplama grubu olarak gerçek sayılar teorisi için niceleyici eleyici , Fourier – Motzkin eliminasyonudur ; gerçek sayılar alanı teorisi için Tarski-Seidenberg teoremidir .

Nicelik belirleyici eliminasyonu, karar verilebilir teorilerin "birleştirilmesinin" yeni karar verilebilir teorilere yol açtığını göstermek için de kullanılabilir .

Algoritmalar ve karar verilebilirlik

Bir teorinin nicelleştirici eliminasyonu varsa, o zaman belirli bir soru ele alınabilir: Her biri için bir belirleme yöntemi var mı ? Böyle bir yöntem varsa, biz buna niceliksel eleme algoritması diyoruz . Böyle bir algoritma varsa , teorinin karar verilebilirliği , niceleyici içermeyen cümlelerin doğruluğuna karar vermeye indirgenir . Niceleyici içermeyen cümlelerin değişkenleri yoktur, bu nedenle belirli bir teorideki geçerlilikleri genellikle hesaplanabilir, bu da cümlelerin geçerliliğine karar vermek için niceleyici eleme algoritmalarının kullanılmasını sağlar. ${\ displaystyle \ alpha _ {QF}}$ ${\görüntüleme stili \alfa }$

Ilgili kavramlar

Çeşitli model-teorik fikirler nicelleştirici eliminasyonuyla ilgilidir ve çeşitli eşdeğer koşullar vardır.

Niceleyici eliminasyonuna sahip her birinci dereceden teori model tamamlandı . Tersine, evrensel sonuçlar teorisinin birleştirme özelliğine sahip olduğu bir model tam teorisi, niceleyici eliminasyonuna sahiptir.

Bir teorinin evrensel sonuçları teorisinin modelleri, tam olarak modellerinin alt yapılarıdır . Doğrusal düzenler teorisinin niceliksel eliminasyonu yoktur. Bununla birlikte, evrensel sonuçlarının teorisi, birleştirme özelliğine sahiptir. ${\ displaystyle T}$ ${\ displaystyle T}$

Temel fikirler

Bir teorinin niceleyici eleme özelliğine sahip olduğunu yapıcı bir şekilde göstermek için, değişmezlerin bir birleşimine uygulanan varoluşsal bir niceleyiciyi ortadan kaldırabileceğimizi göstermek, yani formun her bir formülünün şu şekilde olduğunu göstermek yeterlidir:

{\ displaystyle \ var x. \ bigwedge _ {i = 1} ^ {n} L_ {i}}

her birinin değişmez olduğu yerde , niceleyici içermeyen bir formüle eşdeğerdir. Nitekim, niceleyicileri değişmezlerin bağlaçlarından nasıl çıkaracağımızı bildiğimizi varsayalım, o zaman niceleyici içermeyen bir formül ise, onu ayırıcı normal biçimde yazabiliriz. ${\ displaystyle L_ {i}}$ ${\görüntüleme stili F}$

{\ displaystyle \ bigvee _ {j = 1} ^ {m} \ bigwedge _ {i = 1} ^ {n} L_ {ij},}

ve şu gerçeği kullanın

{\ displaystyle \ var x. \ bigvee _ {j = 1} ^ {m} \ bigwedge _ {i = 1} ^ {n} L_ {ij}}

eşdeğerdir

\bigvee _{j=1}^{m}\vardır x.\bigwedge _{i=1}^{n}L_{ij}.

Son olarak, evrensel bir niceleyiciyi ortadan kaldırmak için

{\ displaystyle \ forall xF}

nerede niceleyici yok ise, ayrık normal forma dönüşüyoruz ve eşdeğer olan gerçeği kullanıyoruz ${\görüntüleme stili F}$ ${\ displaystyle \ l not F}$ ${\ displaystyle \ forall xF}$ ${\görüntüleme stili \l değil\x var.\F değil.}$

Karar verilebilirlik ile ilişki

Erken model teorisinde, niceleyici eliminasyonu, çeşitli teorilerin karar verilebilirlik ve tamlık gibi özelliklere sahip olduğunu göstermek için kullanıldı . Yaygın bir teknik, önce bir teorinin niceleyicilerin ortadan kaldırılmasını kabul ettiğini ve daha sonra yalnızca niceleyici içermeyen formülleri dikkate alarak karar verilebilirliği veya tamlığı kanıtladığını göstermekti. Bu teknik, Presburger aritmetiğinin karar verilebilir olduğunu göstermek için kullanılabilir .

Teoriler karar verilebilir olabilir, ancak niceleyici eliminasyonunu kabul etmeyebilir. Açıkça konuşursak, toplam doğal sayılar teorisi niceleyicinin ortadan kaldırılmasını kabul etmedi, ancak karar verilebilir olduğu gösterilen ilave doğal sayıların bir genişlemesiydi. Bir teori karar verilebilir olduğunda ve geçerli formüllerinin dili sayılabilir olduğunda, teoriyi , niceleyici ortadan kaldırmaya sahip olmak üzere sayısız ilişkiyle genişletmek mümkündür (örneğin, teorinin her formülü için, bir ilişki sembolü eklenebilir. formülün serbest değişkenlerini ilişkilendirir ).

Örnek: Nullstellensatz için cebirsel olarak kapalı alanlar ve için farklı şekilde kapalı alanlar .

Ayrıca bakınız

Notlar

Referanslar

Viktor Kuncak ve Martin Rinard. " Yinelemeli Olmayan Türlerin Yapısal Alt Tiplendirilmesi Karar Verilebilir ". In Bilgisayar Bilimleri, Mantık üzerine On sekizinci Yıllık IEEE Sempozyumu 2003.

Languages

In other projects