Gelen teorik bilgisayar bilimleri , daha doğrusu içinde Hesaplama teorisi , Rice'ın teoremi herhangi belirtiyor önemsiz olmayan semantik özellik a programa olan undecidable . Rice'ın teoremi , durdurma probleminin karar verilemezliğini genelleştirir . Teorem klasiktir ve hesaplanabilirlik teorisinin belirli çalışmalarındaki alıştırmaların konusudur. Hesaplanabilirlik açısından belirli bir felsefi önemi vardır ve mantıkçı Henry Gordon Rice'a bağlıdır .
Anlamsal özellikler bir programın davranışıyla ilgilidir ve programın kaynak kodundaki sözdizimsel özelliklerin tersidir . Bir özellik, herhangi bir hesaplanabilir işlev için doğru veya herhangi bir hesaplanabilir işlev için yanlış değilse önemsiz değildir. Aşağıdaki tablo, sözdizimsel önemsiz olmayan özelliklere ve anlamsal önemsiz olmayan özelliklere örnekler verir. Rice teoremi yalnızca anlamsal özellikler için geçerlidir.
Sözdizimsel özellikler (dikkatli olun, Rice'ın teoremi geçerli değildir) | Anlamsal özellikler (ve bu nedenle Rice teoremi ile karar verilemez) |
---|---|
|
|
Bir programın doğru olduğunu doğrulamak için , kod kapsamına sahip test pilleri dahil olmak üzere test kullanılabilir . Ancak Edsger Dijkstra'nın da belirttiği gibi "Test programları, böceklerin varlığını göstermenin çok etkili bir yolu olabilir, ancak bunların yokluğunu kanıtlamak için umutsuzca yetersizdir" .
Rice'ın teoreminin pragmatik formülasyonu, programların hiçbir otomatik statik analizi yönteminin, bir programın kaynak kodundan, girdileri bu programın çıktısıyla ilişkilendiren işlevin tatmin edip etmediğine karar vermeyi mümkün kılmamasıdır. (önemsiz olmayan) özellik.
Uygulamada, Rice teoreminin sınırlamalarını aşmak için stratejiler benimsiyoruz:
Bu stratejiler, programları test etmek için farklı yaklaşımlarla sonuçlandı: soyut yorumlama , doğrulama modelleri (model kontrolü) ve ispat asistanı tarafından yarı otomatik program ispatı . Bu yöntemlerin hiçbiri kapsam açısından evrensel değildir. Mevcut araştırma, doğrulayıcıların uygulama alanlarını genişletmeyi, dolayısıyla yukarıda belirtilen kısıtlamaları azaltmayı amaçlamaktadır, ancak Rice'ın teoremi, mutlak doğrulayıcının olmadığını veya Frederick Brooks'un dediği gibi "sihirli değnek olmadığını" söylüyor .
Rice teoremine bir giriş olarak, programın karar konusu özelliğinin programın belirli bir fonksiyonu hesaplaması olduğu özel durumu düşünün ; ayrıca programın işlevi " gerçekleştirdiğini " söylüyoruz . Girişte ve ilk paragrafta söylediğimizle karşılaştırıldığında, programla ilişkili işleve karar verme özelliği eşittir . Başka bir deyişle, program tarafından hesaplanan fonksiyonun fonksiyon olup olmadığını bilmek istiyoruz . Genelliğin arttığı üç durumu ele alacağız.
Program tarafından hesaplanan fonksiyon tanımlanmamış ise bu, giriş değerine bakılmaksızın programın asla bitmediği anlamına gelir. Bu özelliğe karar vermek, bir programın hiçbir yerde tanımlanmayan işlevi yerine getirip getirmediğine karar verecek bir algoritma olmadığını söyleyerek formüle edilebilen durdurulamazlık teoremini uygulayarak mümkün değildir .
Bir programın kare işlevini yerine getirip getirmediğine , başka bir deyişle işlevi yerine getirip getirmediğine karar vermek istediğimizi varsayalım . Programın
programmeCarré _p (x) = (x); x * xnerede herhangi bir program, tanımsız kalmadan bir değer için işlevi etkin bir şekilde hesaplar . Program programmeCarré _p fonksiyonunun kareyi hesaplayıp hesaplamadığına karar vermek için, bitip bitmediğine karar vermelidir . Bu nedenle durdurmaya karar vermelidir üzerinde . Bu, bildiğimiz gibi, karar verilemez olan ne az ne de çok durma sorunudur. Dolayısıyla, bir programın kendisine verilen değerin karesini girdi olarak hesaplayıp hesaplamadığına karar verilemez.
Bu durumda, herhangi bir fonksiyon için bir program tarafından hesaplanan fonksiyonun kararını da durdurma problemine indirebiliriz , x * x'i (x) ile değiştirmek, yani programın olup olmadığına karar vermek yeterlidir.
şey _p (x) = (x); (x)işlevi hesaplar . Bu nedenle, bir fonksiyon verildiğinde , bir programın fonksiyonu hesaplayıp hesaplamadığına karar vermenin kararsız olduğu sonucuna vardık .
Bu bölümde, Rice teoreminin literatürdeki farklı versiyonlarını açıklıyoruz.
Hesaplanabilirlik teorisi çalışmalarında, Rice teoremi genellikle Turing makinelerinin desteğiyle ifade edilir. Wolper, Hesaplanabilirliğe Giriş adlı kitabında , özyinelemeli olarak numaralandırılabilen diller üzerindeki önemsiz olmayan herhangi bir özelliğin karar verilemez olduğunu belirtir . Bir Turing makinesi tarafından kabul edilirse, bir dilin yinelemeli olarak numaralandırılabileceğini hatırlıyoruz. Wolper, bunun Turing makinelerinde değil de Turing makinelerinde kabul edilen diller üzerindeki bir özellik, yani sözdizimsel değil anlamsal bir özellik olduğu konusunda ısrar ediyor.
Olivier Ridoux ve Gilles Lesventes, "genişletici" (yani anlambilimsel) ve programlar üzerinde önemsiz olmayan bir özellik önermektedir.
Rice teoremi, programlar tarafından hesaplanan fonksiyonlar açısından ifade edilebilir. Turing eksiksiz bir programlama dili ile çalıştığımızı varsayıyoruz . Izin vermek , program p tarafından hesaplanan fonksiyon olsun . bu nedenle , girişteki p programının değerlendirilmesinin sonucudur . Program p girişte bitmezse , tanımlanmaz. Bitmez programlar olduğundan, fonksiyon olduğunu kısmi . İle gösterelim FC tüm kısmi hesaplanabilir fonksiyonlar kümesi içinde . F FC olsun . Kümeyi P F ile gösterelim { p | F demek ki}, tüm programlar p fonksiyonu şu şekilde yer almaktadır F . Rice'ın teoremi söylüyor P F ise özyinelemeli ancak ve ancak F = ∅ veya F = FC .
Rice'ın hesaplanabilir fonksiyonlar için teoremi, özyinelemeli olarak numaralandırılabilir kümeler açısından da ifade edilebilir . RE ile özyinelemeli olarak numaralandırılabilen tüm alt kümelerin sınıfını belirtin . E RE edelim . Ardında göstersin P programlar kümesi p bir dizi karar bir D (yani y bir bölgesinin IFF yürütme s girişi uçları y ). Rice'ın teoremi söylüyor P ise özyinelemeli ancak ve ancak E = ∅ veya E = RE .
Rice'ın yukarıdaki teoremi, özyinelemeli olarak numaralandırılabilir kümelerle ilgili özelliklerin karar verilemezliğini ifade eder. Bununla birlikte, bu tür özellikler arasında yarı karar verilebilir olanları karakterize etmek mümkündür . Bir özellik Prop ardışık enumerable setlerinde olduğu söylenir monoton tüm ardışık enumerable kümeleri için, eğer bir ve B gibi bir B , elimizdeki Prop (A) Prop (B) . Örneğin, "A sonlu bir kümedir" monoton değildir, "A, x öğesini içerir" dir. Let Prop olmak ardışık enumerable setleri ve üzerinde bir özellik E Prop RE ardışık enumerable setleri tatmin sınıfı Prop . Ardında göstersin P A programlar kümesi p bir dizi karar bir D (yani y bir bölgesinin IFF yürütme s girişi uçları y ). Rice'ın teoremin Bu varyant eğer söylüyor P E Prop olduğunu ardışık enumerable ardından Prop monoton olduğunu.
P, özyinelemeli olarak numaralandırılabilir kümeler üzerinde önemsiz olmayan bir özellik olsun . Genelliği kaybetmeden, P (∅) 'nin yanlış olduğunu varsayalım (eğer durum bu değilse, P'nin olumsuzlamasına benzer şekilde düşünüyoruz). Bize bu göstersin durdurma sorunu olan düşük bir Turing makinesi M içine Böylece M Turing makinesi durdurma problemi, (w, E) bir örneğini dönüştüren ve bir kelime w azalmayı tanımlayacağı P. kararı için ', P.
P'yi karşılayan özyinelemeli olarak numaralandırılabilir bir A kümesi ve A'yı kabul eden bir makine M A vardır. Bu nedenle, (M, w) 'den aşağıdaki Turing makinesini M' etkin bir şekilde oluşturuyoruz:
M'(u) Lancer M sur w Lancer MA sur uProva, azaltma düzeltmesiyle sona erer: M, w üzerinde durur, ancak ve ancak P (L (M ')). Aslında :
Rice'ın fonksiyonlar için teoremi benzer şekilde gösterilebilir.
On işlevleri için Rice'ın teoremi ile gösterilebilir sabit nokta teoremi Kleene . Kleene sabit nokta teoremi herhangi bir program transformatör için bahsedilen T toplam fonksiyonu, bir program vardır s şekilde programlar p ve t (s) aynı işlevi hesaplanması ( ).
Önemsiz olmayan bir özellik ( ve FC ) olsun. Saçma bir şekilde varsayalım ki P = { p | F } özyinelemelidir.
Yana F Önemsiz olmayan vardır f ve g . Fonksiyonları f ve g hesaplanabilir olmak üzere iki programlar vardır p ve q birlikte = f ve = gr . Program trafosunu T tanımlayalım :
T (x) = q eğer x P
T (x) = p eğer x P
Yana P özyinelemelidir, T hesaplanabilir bir toplam fonksiyonudur. By Kleene'nin sabit nokta teoremi , bir program vardır n böyle . Şimdi T (n) değerine ilişkin bir vaka çalışmasına geçelim :
Resmi bir kanıt oluşturmadan önce, ilk olarak pratik bir vaka ile bir yaklaşıma girelim. Bir programın p'nin kare alma fonksiyonunun doğru bir gerçeklemesi olduğunu kesin olarak belirleyen bir algoritmamız olduğunu varsayalım . Bu bir d tamsayısını alır ve d 2'yi döndürür . İspatın, bir programın önemsiz olmayan bir özelliğini doğrulayan herhangi bir algoritma için işe yaradığını unutmayın.
Kanıtın sezgisi, kareleme programlarını kontrol eden algoritmamızı, durduran fonksiyonları tanımlayan ve ardından durdurma problemini getiren bir algoritmaya dönüştürmektir . Bunu yapmak için, bize giriş olarak bir algoritma alma inşa izin bir ve i ve bu programın belirler bir bir durur verilen i .
Bu algoritma, yeni bir program açıklamasını oluşturur t tek bir argüman alarak n ve:
Eğer a (i) sonsuza dönerse, o zaman t , n'nin değeri ne olursa olsun asla (2) adımına ulaşmaz .
Öyleyse t , ancak ve ancak adım (1) biterse sayıların karelerini hesaplayan bir fonksiyondur.
İlk varsayımımız, kareleri hesaplayan programları kesin olarak tanımlayabileceğimiz olduğundan, a ve i'ye bağlı olan f'nin böyle bir program olup olmadığını belirleyebiliriz ve bu herhangi bir a ve i için . Bu nedenle, program eğer karar bir program var bir belli girişi için durur i .
Durdurma karar algoritmamızın hiçbir zaman t'yi yürütmediğini , ancak açıklamasını yalnızca varsayımla her zaman biten kare tanımlama programına ilettiğini unutmayın. Bu nedenle, t'nin açıklaması her zaman bitecek şekilde yapılandırılırsa, durdurma algoritması bu nedenle durmada başarısız olamaz.
halts (a,i) { define t(n) { a(i) return n×n } return est_une_fonction_de_carre(t) }Bu ispat yöntemi, kareleri hesaplayan fonksiyonlara odaklanmaz. Uzun olduğunca bazı programlar biz tanımak için çalışıyoruz ne yapabiliriz, yani Bir programın bir özelliği belirlemek, biz bir çağrı yapabilir bir bizim olsun t . Karekökleri hesaplayan programları kontrol eden bir yöntemimiz veya aylık ücreti hesaplayan programlarımız veya belirli bir " Abraxas " girişi ile biten programlarımız olabilir . Her durum için, kapatma sorununu benzer şekilde çözebiliriz.
Resmi kanıtBiçimsel kanıt için, algoritmaların kısmi işlevleri karakter dizileri olarak tanımladığını ve kendilerinin dizelerle temsil edildiğini varsayıyoruz . Bir karakter dizisi ile temsil edilen algoritması tarafından hesaplanan kısmi işlevi a ile gösterilir F bir . Bu kanıt, absürdün akıl yürütmesiyle ilerler : ilk önce, bir algoritma tarafından karar verilen önemsiz olmayan bir özelliğin olduğunu varsayacağız; daha sonra bu varsayımla durdurma probleminin hesaplanabilir olduğunu, bu imkansız ve dolayısıyla bir çelişki olduğunu gösterebileceğimizi göstereceğiz .
Şimdi varsayalım P (a) bir önemsiz olmayan özellikte karar bir algoritmadır F bir . Öyleyse, P (ne-sarrete_pas) = "hayır" olduğunu ve ne-sarrete_pas ile asla durmayan bir algoritmanın temsili olduğunu varsayalım . Bu doğru değilse, o zaman mülkün yadsınması için doğrudur. Yana P önemsiz olmayan bir özellik karar verir, bu bir karakter dizesini var olduğu ima b bir algoritma ve temsil P (b) = "evet". Daha sonra aşağıdaki gibi bir H (a, i) algoritması tanımlayabiliriz :
Artık H'nin durdurma sorununa karar verdiğini gösterebiliriz :
Durdurma problemi hesaplanamadığından, bir çelişki vardır ve bu nedenle , temsil edilen fonksiyon için önemsiz olmayan bir özelliğe karar veren bir algoritma P (a) olduğu varsayımı yanlış olmalıdır. CQFD.
Rice'ın kümeler için teoreminin ispatına benzer şekilde , durdurma probleminin yadsımasının yarı kararının, yinelemeli olarak numaralandırılabilir kümelerdeki monoton olmayan herhangi bir özelliğin yarı kararına indirgenebileceğini gösteriyoruz.
P monoton olmayan ve yarı karar verilebilir bir özellik olsun. Bu nedenle, sırasıyla Turing makineleri MA ve MB tarafından hesaplanan, birbirini takip eden iki A ve B kümeleri vardır, örneğin:
Ayrıca, bir Turing makinesinin herhangi bir temsili için, bu makine tarafından kabul edilen özyinelemeli olarak numaralandırılabilir küme P.
Bu nedenle, girdi olarak bir Turing makinesi M'nin temsilini ve ardından algoritması aşağıdaki gibi olan bir x girdisini alarak bir Turing makinesi H oluşturabiliriz:
1 Bir y girişinde bir Turing makinesi T'nin temsilini oluşturun: 1 Paralel olarak yürütünTarafından "paralel yürütme" makinesi T, Y üzerinde bir adım MA, y MB sonra adım x, M daha sonra adım, yani daha sonra ikinci bir y MA aşaması ve çalıştırır kastedilmektedir. Başka bir deyişle, biri bir makinenin hesaplama adımlarını diğer makineninkilerle "değiştirir".
M, x üzerinde durursa, T, ancak ve ancak MA veya MB y'yi kabul ederse ve y'yi kabul eder ve A, B'ye dahil olduğundan, bu, ancak ve ancak y'nin B'ye ait olması anlamına gelir.Bu nedenle, T, B kümesini tam olarak kabul eder, ki bu, hipotez ile P'yi doğrulamaz.Bu nedenle, MP T'yi kabul etmez. (P'nin yarı-karar verilebilir olduğu varsayılır, MP hiç durmayabilir) M x üzerinde durmazsa, T yalnızca ve yalnızca y'yi kabul eder. eğer y A'ya aitse, T, hipotezle P'yi tatmin eden A kümesini tam olarak kabul eder. Sonuç olarak, MP, T'yi kabul eder (ve bu nedenle yarı-karar verilebilirliğin tanımı gereği durma noktasına gelir). Makine H, bu nedenle, durdurma probleminin olumsuzlamasını hesaplar. İkincisi, çelişki nedeniyle yarı-karar verilebilir olmadığından, P yarı-karar verilemez.