karar verilebilir

Gelen teorik bilgisayar bilimleri , özellik denir Karar verilebilen bir sette (aynı zamanda yinelemeli , ardışık derive ) bir varsa karar usulü bunun için. Karar prosedürü, özelliği olsun veya olmasın kümenin her bir elemanı için cevap verebilen bir algoritmadır . Böyle bir karar verme süreci “hiç” yoksa, mülke karar verilemez denir . Bir karar problemi , belirli bir özellik için bir karar prosedürünün formüle edilip edilemeyeceği ve nasıl formüle edilebileceği sorusudur.

Programların en önemli sözdizimsel özellikleri kararlaştırılabilirken, genel olarak, Rice teoremine göre, programların herhangi bir (önemsiz olmayan) semantik özelliği kararlaştırılamaz, örneğin bir girdi üzerinde bir programın sonlandırılması ( tutma problemi ) veya eşitliğin eşitliği. iki programın işlevleri ( eşdeğerlik sorunu ).

Başlangıçta formüllerin geçerliliği için özel olarak kastedilen terim, şimdi sayılabilir kümelerdeki herhangi bir özellik için kullanılmaktadır . Algoritma kavramı bir hesaplama modeli gerektirir ; Aksi belirtilmedikçe, Turing makineleri veya eşdeğer bir model kastedilmektedir.

tanım

Sayılabilir bir kümenin bir alt kümesi , karakteristik fonksiyonu ile tanımlanırsa karar verilebilir olarak adlandırılır . ${\ görüntü stili T}$${\ görüntü stili M}$ ${\ displaystyle \ chi _ {T} \ iki nokta üst üste M \ ila \ {0,1 \}}$

${\ displaystyle \ chi _ {T} (t) = {\ başlangıç ​​{durumlar} 1, & {\ mbox {if t}} \ in T \\ 0, & {\ textrm {aksi halde}} \ bitiş {durumlar} }}$

tahmin edilebilir . Böylece karar verilebilirlik kavramının izi, hesaplanabilirlik kavramına kadar uzanır.

Bu tanım, kümenin tüm elemanlarının bilgisayarda temsil edilebileceğini varsayar . Miktar tanrılaştırılabilir olmalıdır . Teoride, daha kolay karşılaştırma için, doğrudan varsayılır veya varsayılır. İkinci durumda, sorun olarak sunulmuştur kelime sorununa bir resmi dili . ${\ görüntü stili M}$${\ görüntü stili M}$${\ displaystyle M = \ matbb {N}}$${\ görüntü stili M = \ {0.1 \} ^ {*}}$

Yalnızca sayılabilir kümeler tanrılaştırılabildiğinden, gerçek sayılar gibi sayılamayan kümeler için karar verilebilirlik kavramı tanımlanmamıştır. Ancak, genişletilmiş bir makine modeli (örneğin Blum-Shub-Smale modeli ) aracılığıyla hesaplanabilirlik kavramını gerçek sayılara genişletme girişimleri vardır .

sınır

Karar verilemezlik , bir ifadeye bir doğruluk değeri atamanın pratik veya temel imkansızlığı ile karıştırılmamalıdır . Ayrıntılı olarak, aşağıdaki terimler söz konusudur:

1. Tutarsızlık: Paradokslar veya çatışkılar , bir hesabın çelişkiler içerdiğini, yani çelişkilerden arınmış olmadığını gösterir . Russell'ın Paradoksu , örneğin, gösterdi naif küme teorisine çelişkileri içeren.
2. Bağımsızlık: Tutarlı bir hesaba bir çelişki oluşturmadan eklenebilen ifadelere, bu hesaba göre görece çelişkisiz denir . Olumsuzlaması nispeten çelişkilerden arınmışsa, ifade bağımsızdır . Örneğin, seçim aksiyomu Zermelo-Fraenkel küme teorisinden bağımsızdır .
3. Eksiklik: En azından aritmetiğin ifade gücüne sahip olan tutarlı hesaplarda, hesapta kanıtlanamayan doğru ifadeler vardır. Bu tür hesaplamalara eksik denir .

Karar verilebilirlik, ifadelerin değil, yüklemlerin bir özelliğidir . Yüklemin iyi tanımlı olduğu varsayılır, bu nedenle kümenin her öğesi için tanımlanmış bir doğruluk değeri verir. Karar verilemezlik, yalnızca yüklemin bir algoritma tarafından hesaplanamayacağı anlamına gelir.

Sıfır-yer yüklemleri olarak görülen ifadeler, doğruluk değerleri hala belirsiz olsa bile, her zaman karar verilebilir. Eğer ifade doğruysa, her zaman bir tane döndüren algoritma bir karar verme sürecidir. Aksi halde her zaman sıfır döndüren algoritma bir karar verme sürecidir.

Tarih

Karar problemi "ifadelerin genelliğini belirleme problemi"dir. "Belirli bir tümdengelim teorisi için, teorinin terimleriyle formüle edilmiş belirli bir cümlenin teori içinde kanıtlanıp kanıtlanamayacağına karar vermemize izin veren genel bir prosedür belirleme meselesidir."

Belirleyici faktör, bir sistemde bir ifadenin, bir formülün geçerli olup olmadığını sonlu sayıda adımda netleştiren , tamamen mekanik olarak uygulanabilir bir prosedürün, bir algoritmanın olup olmadığıdır.

Göre Frege , Whitehead ve Russell , logicians ve matematik "Merkezi söz oldu: bir algoritma var [...], belirli verilen aksiyomlarından aşağıdaki olsun veya olmasın, bir mantıksal taşı herhangi formülden belirler (sözde karar sorunu)?"

Kurt Gödel , 1931'de karar problemi üzerine bir çalışma yayınladı; İngiliz Alan Turing (1912–1954), Gödel'in 1931'deki Hesaplanabilir Sayılar Üzerine adlı çalışmasında, matematiğin bu dalı için temel olan “Karar Problemine” (28 Mayıs 1936) bir Uygulama ile sonuçlarını yeniden formüle etti . Gödel'in evrensel, aritmetik tabanlı biçimsel dilini, Turing makinesi olarak bilinen basit, biçimsel aygıtlarla değiştirdi .

Mantıkçı Heinrich Scholz (1884–1956) 1936'da bu çalışmanın bir kopyasını Turing'den istedi (ve aldı). Bu çalışma temelinde, Scholz (Achim Clausing'e göre) "bilgisayar bilimi üzerine dünyanın ilk seminerini" düzenledi.

Örnekler

Tüm sonlu kümeler, tüm çift sayılar kümesi ve tüm asal sayılar kümesi karar verilebilir. Karar verilebilir her küme için, tamamlayıcısı da karar verilebilir olabilir. Karar verilebilir iki kümenin kesişimi ve birleşimi karar verilebilir.

Tutma sorunları

Durdurmak sorun , bir olmadığı sorusuna tarif algoritma sona bir giriş ile . Alan Turing , bu sorunun kararsızlığını gösterdi. Daha resmi olarak, tutma problemi, algoritmanın girdi için sonlandırdığı , yani yalnızca sonlu uzunlukta hesapladığı algoritma ve girdi çiftlerinin özelliğidir . Eşit tutma problemi, yani algoritmaların her girdi için nihai olarak tutma özelliği de kararsızdır.

Bununla birlikte, doğrusal olarak sınırlandırılmış Turing makineleri gibi birçok zayıf hesaplama modeli için durma sorununa karar verilebilir.

Önerme mantığında geçerlilik

Önermeler hesabındaki geçerliliğe karar verilebilir. Bunun tamamlayıcısı , önermeler mantığının karşılanabilirlik sorunu olarak bilinir . Bir karar verme süreci doğruluk tablosu yöntemidir .

Yüklem mantığında geçerlilik

Yüklem mantığı için özel karar problemi , 1928'de David Hilbert tarafından ortaya atıldı (bkz. Hilbert programı ). Alan Turing ve Alonzo Church , 1936'da sorunu çözülemez buldular (bkz. tutma sorunu ).

Karar problemi genel yüklem mantığı için çözülmez, ancak yalnızca tek basamaklı birinci dereceden yüklemlerle yüklem mantığı gibi yüklem mantığının alt alanları için çözülür.

Diofant denklemlerinin çözülebilirliği

Tüm katsayılar tamsayıysa ve yalnızca tamsayı çözümleri aranıyorsa, bir polinom denklemine Diophantine denir. Diophantine denklemlerinin bir çözüme sahip olma özelliği ( Hilbert'in onuncu problemi ) karar verilemez. Lineer Diophantine denklemlerinin çözülebilirliği ise kararlaştırılabilir.

Post'un yazışma sorunu

Sonlu bir alfabe üzerinde boş olmayan kelime çiftlerinin sonlu listesine problem durumu denir. Bir problemin bir çözümü, listedeki kelime çiftleri için boş olmayan, sonlu bir sayı dizisidir, böylece kelime çiftlerinin ilk bileşenleri bir araya getirildiğinde, kelime çiftlerinin ikinci bileşenleri ile aynı kelimeyi verir.

Örnek: çözümü vardır o geçerli olmasıdır . ${\ displaystyle \ sol (a, aba \ sağ), (ab, bb), (baa, aa)}$${\ displaystyle \ sol (1,3,2,3 \ sağ)}$${\ displaystyle a \ cdot baa \ cdot ab \ cdot baa = abaaabbaa = aba \ cdot aa \ cdot bb \ cdot aa}$

Postsche yazışma sorun sorun vakaların malıdır, undecidable bir çözüm olması.

fizik

Toby Cubitt, David Perez-Garcia, Michael Wolf'a göre, kuantum mekaniksel çok cisim teorisinden gelen aşağıdaki problem karar verilemez. Kuantum mekanik çok cisim probleminin Hamilton fonksiyonu verilmiştir. Spektrumun ilk uyarılmış durumdan temel duruma bir boşluğu var mı, yok mu? Yazarlar, spektral boşluk sorusunun kararsız olduğu, translasyonla değişmeyen en yakın komşu etkileşimi ile iki boyutlu bir kafes üzerinde açıkça bir kuantum spin sistemleri ailesi inşa ettiler. Hamilton operatörlerinin karmaşıklık teorisini periyodik olmayan döşeme teknikleriyle birleştirdiler ve sorunu bir Turing makinesinin tutma sorununa çevirdiler. Sistemin diğer düşük enerji özelliklerine de karar verilemez.

İlgili terimler

Karar verilebilir kümelerden daha genel bir sınıf, yinelemeli olarak numaralandırılabilir veya yarı karar verilebilir kümelerdir ; burada "evet" için tek gereklilik, hesaplamanın sonlu bir zamanda durması gerektiğidir. Hem bir küme hem de onun tümleyeni yarı karar verilebilir ise, o zaman küme karar verilebilirdir. Durdurma problemi yarı kesindir çünkü “evet” cevabı her zaman programı çalıştırarak verilebilir. Ancak, elde tutma probleminin tamamlayıcısı yarı-kararlı değildir.

Ayrıca bakınız

• denklik sorunu
• öngörülebilirlik
• sonluluk sorunu
• Boşluk sorunu
• Yazışma sonrası sorun
• Yarı karar verilebilir set

Edebiyat

• Lothar Czayka : Biçimsel mantık ve bilim felsefesi. Ekonomistler için giriş. Oldenbourg, Münih ve diğerleri 1991, ISBN 3-486-20987-6 , sayfa 45 ff.
• Willard Van Orman Quine : Mantığın İlkeleri. 8. baskı. Suhrkamp, ​​​​Frankfurt am Main 1993, ISBN 3-518-27665-4 , sayfa 142 ve devamı ( Suhrkamp-Taschenbuch Wissenschaft 65), ayrıntılı olarak.
• Paul Hoyningen-Huene : Biçimsel Mantık. Felsefi bir giriş. Reclam, Stuttgart 1998, ISBN 3-15-009692-8 , s. 226 devamı ( Reclam's Universal Library 9692)
• Hartley Rogers: Özyinelemeli fonksiyonlar teorisi ve etkin hesaplanabilirlik . McGraw-Hill, 1967. 
• Uwe Schöning : Teorik Bilgisayar Bilimi - kısaca . 4. baskı. Spektrum, 2000, ISBN 3-8274-1099-1 , s. 122 ff . 

Bireysel kanıt

1. ↑ Arnim Regenbogen, Uwe Meyer (Ed.): Felsefi terimler sözlüğü. Özel sayı. Meiner, Hamburg 2006, ISBN 3-7873-1761-9 , “karar verilebilir”.
2. ↑ David Hilbert , W. Ackermann : Teorik mantığın temelleri. 6. baskı. Springer, Berlin ve ark. 1972, ISBN 0-387-05843-5 , s. 119 ( Matematiksel bilimlerin temel öğretileri 27).
3. ↑ Alfred Tarski : Matematiksel Mantığa Giriş. 5. baskı, "Gerçek ve Kanıt" makalesini içerecek şekilde genişletildi. Vandenhoeck & Ruprecht, Göttingen 1977, ISBN 3-525-40540-5 , s.145 ( Temel temsilde modern matematik 5).
4. ↑ Patrick Brandt, Rolf-Albert Dietrich, Georg Schön: Dilbilim. Almanca öğrenmek için ortak bir konu. 2. gözden geçirilmiş ve güncellenmiş baskı. Böhlau, Köln ve diğerleri 2006, ISBN 3-412-00606-8 , sayfa 14 ( UTB 8331).
5. ↑ kopya edilmiştir Achim CLAUSING tarafından bulunan en az Bilgisayar Bilimleri Enstitüsü Vestfalya Wilhelm Üniversitesi de Münster ( Westfälische Nachrichten . 28 Ocak 2013: Bir öncü izinde: Bilgisayar bilimcisi Alan Turing tarafından Orijinal baskılar vardır içinde Münster Üniversitesi Kütüphanesi ; çevrimiçi ).
6. ↑ Hilbert / Ackermann: Temel özellikler. 6. baskı. (1972), s. 119.
7. ↑ Willard Van Orman Quine : Mantık İlkeleri. 8. baskı. Suhrkamp, ​​​​Frankfurt am Main 1993, ISBN 3-518-27665-4 , s. 247.
8. ^ Lothar Czayka: Biçimsel mantık ve bilim felsefesi. Ekonomistler için giriş. Oldenbourg, Münih ve diğerleri 1991, ISBN 3-486-20987-6 , sayfa 45.
9. ↑ Cubitt, Perez-Garcia, Wolf, Undecidability of the spectral gap, Nature, Cilt 528, 2015, s. 207, Arxiv Ön Baskı