Problem, matematik ve analiz · 04 / 53
Invariant, indüksiyon ve test
Anla → iz sür → uygula → gerekçelendir
2 dk okuma · uygulama için ayrıca zaman ayırBir invariant, işlemin belirli noktasında her zaman doğru kalan önermedir. Döngü ispatını üç adımda kur: başlamadan önce doğru mu, bir tur doğruysa sonraki turda korunuyor mu, bittiğinde istenen sonucu çıkarıyor mu? Insertion sort için ilk i elemanın sıralı ve aynı elemanları içeriyor olması uygun invariant'tır.
Sıralı çıktı tek başına yeterli değildir: eleman kaybı ve çoğaltma olmamalıdır. Bu yüzden “sonuç sıralıdır” ile “sonuç girdinin permütasyonudur” ayrı doğruluk özellikleridir. Sonlanma da kanıtın parçasıdır; her turda azalan negatif olmayan bir ölçü bul. Recursion için problem boyutunun küçülmesi gerekir.
Test, hataları bulur; sonlu testler sonsuz girdi kümesinde doğruluğu ispatlamaz. Yine de karşı örnek avcılığı çok güçlüdür: boş, tek eleman, tümü eşit, ters sıralı, taşma sınırı, bağlantısız graf. Küçük girdilerde basit ama yavaş bir referans çözüme karşı diferansiyel test yap; property test ile sözleşme özelliklerini denetle.
Adım adım iz sürme
Binary search invariant: hedef varsa [lo,hi) aralığındadır. lo=hi olduğunda aralık boşalır. Sınırlar güncellenirken hiçbir aday atlanmamalı.
Maliyet ve varsayımlar
İspat maliyet değil doğruluk içindir. Doğru bir O(n²) çözüm, hatalı O(log n) çözümden değerlidir.
Çalıştırılabilir örnek
Python 3 ile çalıştır. Assert küçük bir örneği denetler; genel doğruluk ispatı değildir. Bazı ileri örnekler özellikle küçük model veya referans oracle'dır; tam üretim uygulaması değildir.
from collections import Counter
def assert_sort_contract(original, result):
assert all(result[i] <= result[i+1] for i in range(len(result)-1))
assert Counter(original) == Counter(result)
assert_sort_contract([3,1,3], [1,3,3])KAVRADIĞINI KONTROL ET
Sıra sende
Sonlanmayan ama invariant koruyan döngü mümkün mü?
Çözümün mantığını göster
Evet. while True içinde x=x işlemi x≥0 invariantını korur ama sonlanmaz. Kısmi doğruluk ile toplam doğruluk farklıdır.
Bir adım ileri
- Örneği değiştirmeden önce girdi sözleşmesini ve invariantı yaz.
- Uygun olan boş, sınır, tekrar ve adversarial girdileri ekle. Basit bir oracle ile karşılaştır.
- Belirtilen modelde maliyeti çıkar; farklı girdi büyüklüklerini ölç ve farkları gerekçelendir.
Temel kaynaklar ve ders notları
Bu eğitimde özgün anlatım kullanıldı; aşağıdaki kaynaklar ispatlar ve ileri okumalar sunar. Bağlantılar daha geniş ders modülünü kapsayabilir.
Jeff Erickson · Algorithms ↗