Mantık ve Curry-Howard yazışması hakkında bir soru

Question

Mantıksal programlama temelleri ile tip sistemler ve geleneksel mantık arasındaki sözdizimsel benzerlik olgusu arasındaki temel bağlantının ne olduğunu açıklayabilir misiniz?

Answer 1

Curry-Howard yazışmaları mantıksal programlama değil, fonksiyonel programlama ile ilgilidir. Prolog'un temel tamircisi, John Robinson'un resolution technique numaralı ispat kuramında, Horn cümleleri satisfiable olarak ifade edilen mantıksal formüller olup olmadığını kontrol etmenin nasıl mümkün olduğunu gösteren, yani bunları yapan mantık değişkenleri için terimleri bulabilmeniz için gerekli olup olmadığını gösterir. doğru.

Bu nedenle, mantıksal programlama, programların mantıksal formüller olarak tanımlanmasıyla ilgilidir ve programın hesaplanması, Prolog'un yeniden yorumlanmasında söylediğim gibi bir tür kanıt çıkarımıdır. Buna karşılık Curry-Howard yazışması, natural deduction olarak adlandırılan özel bir mantık formülü içindeki ispatların, ispatın kanıtladığı formüle karşılık gelen programın türüne göre lambda hesabı içindeki programlara nasıl karşılık geldiğini gösterir; lambda hesaplamasındaki hesaplama, ispatlamaları yeni ve daha doğrudan ispatlara dönüştüren normalleşme denilen ispat kuramında önemli bir olguya tekabül eder. Bu mantıksal programlama ve fonksiyonel programlama, bu mantıklarda farklı seviyelere karşılık gelir: mantıksal programlar, bir mantığın formülleriyle eşleşirken, fonksiyonel programlar formüllerdeki kanıtlarla eşleşir.

Başka bir fark var: kullanılan mantıklar genellikle farklı. Mantıksal programlama genellikle dediğim gibi daha basit mantıksal — kullanır. Prolog, imaların iç içe geçemeyeceği oldukça kısıtlı bir formül sınıfı olan Horn cümleleri üzerinde kuruludur ve Prolog, klasik mantığın tüm gücüyle klasik mantığın geri kazanılmasını sağlamıştır. kesme kuralı Aksine, Haskell gibi işlevsel programlama dilleri, türleri iç içe geçmiş olan ve her türden polimorfizmle süslenmiş olan programları ağır bir şekilde kullanır. Ayrıca sezgisel mantığa dayandırılırlar, Robinson'un hesaplama mekanizmasının dayandığı, dışlanmış ortalamanın ilkesinin kullanılmasını yasaklayan bir mantık sınıfı.

Diğer bazı noktalar:

1. O Horn maddeleri daha sofistike mantık üzerine baz mantık programlama mümkündür; Örneğin, Lambda-prolog, sezgisel mantığa dayanır, çözünürlükten farklı bir hesaplama mekanizmasına sahiptir.
2. Dale Miller Curry-Howard yazışmalar için kullanılan bir diğer terimdir programları metafor olarak deliller ile kontrast, programlama metafor olarak geçirmez arama programlama mantığı geride kanıt teorisi paradigma çağırdı.

Answer 2

Mantıksal programlama temel olarak ispat aramak için hedefe yöneliktir. Yazılan diller ve mantık arasındaki yapısal ilişki, genellikle zorunlu ve diğer diller olmakla birlikte, mantıksal programlama dilleri doğrudan olmasa da, işlevsel dilleri içerir. Bu ilişki programlara kanıtlarla ilgilidir. Bu nedenle, daha sonra işlevsel programlar olarak yorumlanan kanıtları bulmak için mantıksal programlama kanıtı arama kullanılabilir. Bu ikisi arasındaki en doğrudan ilişki gibi görünüyor (istediğin gibi).

Tüm programları bu şekilde oluşturmak pratik değildir, ancak programlardaki sıkıcı ayrıntıları doldurmak için yararlı olabilir ve pratikte bunun önemli bazı örnekleri vardır. Bunun temel bir örneği yapısal alt tiplemedir - ki bu basit bir ispat kanıtı ile birkaç kanıt adımı doldurmaya karşılık gelir.Çok daha sofistike bir örnek, Haskell'in belirli bir hedefe yönelik arama türünü içeren tip sınıf sistemidir - bu, aşırı bir zamanda, derleme zamanında Mantıksal Programlamanın eksiksiz bir formunu içerir.