Curry-Howard, void ve Haskell'de tip kontrolü

Question

Burada verilen Haskell'de tip kontrolü ile ispatlayan bir teorem örneği anlamaya çalışıyorum . Örnek aşağıdaki gibidir.

Curry-Howard izomorfizmini kullanarak, türde bir sakini oluşturun ve bunu kanıtlayın $N= (A\vee (B\rightarrow A))\& (C\&(C\rightarrow B))\rightarrow ((\neg B\& A)\vee ((A\rightarrow B)\&(B\rightarrow A)))$ tutar.

Yazar aşağıdaki kodu sağlar.

data Void
nnot :: Void -> a
nnot = undefined
proposition :: (Either a (b -> a), (c, c -> b)) -> Either (Void -> b, a) (b -> a)
proposition (Left x, (y, f)) = Left (nnot, x)
proposition (Right g, (y,f)) = Left (nnot, (g (f y)))

İçerme $(A\vee (B\rightarrow A))\& (C\&(C\rightarrow B))\rightarrow (\neg B \& A)$tutmaz. Ancak inşa edilen terimin bunu kanıtladığı iddia ediliyor ve tip denetleyicisi bundan memnun. Neden?

Başlangıç ​​formüllerinin türüne kopyalanmasının propositionyanlış olduğunu hissediyorum , çünkü inkarının saçma olanla btemsil Void -> bedildiğini (ve olarak tanımlandığını nnot). Yani mantıksal açıdan, çift (Void -> b, a)terime karşılık gelir$\bot \& A$. Ancak bu, tür denetleyicinin yukarıdaki kodu neden doğruladığına bir cevap vermez. Bu nedenle, aşağıdaki iki soruyla ilgili herhangi bir ipucunu çok takdir edeceğim.

1. Haskell derleyicisi neden türünü onaylıyor proposition?
2. Curry-Howard olmadığında durum böyleyse, o zaman tür kontrolünü Curry-Howard aracılığıyla olumsuzluk içeren formülleri kanıtlamak için nasıl kullanabilirim?

Bu sorunun cs veya stackoverflow için daha uygun olduğunu bilmiyorum, bu yüzden konu dışı ise lütfen özür dilerim.

DÜZENLEME: Aşağıdaki düzeltilmiş teklif verildiğinde:

proposition :: (Either a (b -> a), (c, c -> b)) -> Either (b -> Void, a) (b -> a)

Bunun için aşağıdaki "kanıtı" yazdım ve tip denetleyicisi tatmin oldu. Tip kontrolünden sonra önerinin kanıtlanmış sayılabileceğine inanabilir miyim bilmiyorum.

proposition (Left x, (y, f)) = Right ((\z1 z2 -> z1) x)
proposition (Right g, (y,f)) = Right ((\z1 z2 -> z1) (g (f y))) 

Ve yine de tür kontrol prosedürü ile herhangi bir olumsuzlamayı kanıtlamanın mümkün olup olmadığı konusunda hiçbir fikrim yok.

Düzenleme2: Konuyu biraz anladığımı sanıyordum ama sonra şunu denedim:

prop1 :: ((Either a b), c) -> b
prop1 (Right x, y) = x

Bu kod Haskell için uygundur (örneğin, orada ). Ancak mantık açısından yanlış yazılmış gibi görünüyor: karşılık gelen tür$(A\vee B)\& C\rightarrow B$. Verilen davanın prop1(Right x, y) = xdoğru (heh) tipinde olduğu açıktır, ancak davayı ben tanımlamadım prop1(Left x, y), bu nedenle bu dava için önerme ispatlanmadı. Dolayısıyla, ayrılıkla ilgili sorunlar da yaşayabilirim.

Answer 1

Farklı bir öğretici bulurdum çünkü bu öğreticinin yazarının temelde kafası karışmış durumda. Yanlış iddia ediyorlar ki$\neg a$ ve $\bot\to a$ eşdeğerdir ($a\to\bot$ doğru olurdu) ve ayrıca yanlış bir şekilde bir tür işlevi yazamayacağınızı iddia edin $\texttt{Void}\to a$.

$\texttt{Void}\to a$boş bir şekilde doğrudur. Prensipte, bu türden bir fonksiyon hiçbir tanım gerektirmemelidir çünkü onu tanımlamanız gereken olayların sayısı sıfırdır. GHC bunu kabul etmiyor, ancak (birlikte -XEmptyCase) kabul ediyor

f :: Void -> a
f x = case x of {}

bu tamamen geçerli, mantıksal olarak sağlam bir tanımdır.

Haskell derleyicisi teklif türünü neden onaylıyor?

Haskell kodunda yazılan önerme aslında doğrudur. Kanıt, kullandığı için geçersiz olsa da$\texttt{undefined}$.

Sağ tarafı ile değiştirdiyseniz $(b\to\texttt{Void},a)$ o zaman yanlış olur, ancak yine de bunu kullanarak "kanıtlayabilirsin" $\texttt{undefined}$; aslında sadece yazabilirsin$\texttt{proposition} = \texttt{undefined}$ve tür denetleyicisi bunu kabul eder. Ayrıca kabul ederdi$\texttt{proposition} = \texttt{proposition}$. Haskell'i bir Curry-Howard sanal alanı olarak kullanmak istiyorsanız, kodunuzun bir istisna oluşturmamasına veya sonlandırmamasına dikkat etmelisiniz, çünkü derleyici bu hataları yakalayamaz.

---

Düzenlemeye yanıt: kanıtınız doğrudur, ancak basitleştirilebilir. İlk durumda, bir işlev oluşturmaya ve hemen bağımsız değişkenlerinden birine uygulamaya gerek yoktur. (\z1 z2 -> z1) xSenin yerine yazabilirsin \z2 -> xya \_ -> xda argüman / öncül kullanılmadığı için. İkinci durumda, b -> azaten sahip olduğunuz için kanıtlamanıza gerek yoktur g :: b -> a. Basitleştirilmiş kanıt

proposition (Left x, _) = Right (\_ -> x)
proposition (Right g, _) = Right g

Dan Doel'in bir yorumda bahsettiği tuzaklara ek olarak, eksik vakalar da dikkat edilmesi gereken başka bir konudur. GHC varsayılan olarak onlar hakkında uyarmıyor bile. Bununla -Werror=incomplete-patternsbirlikte, eksik vakaları olan programları kabul etmeyi reddedecektir.

Olumsuzlukları kanıtlayabilirsiniz. Bir tür değeri döndürmeniz gerekiyor$\texttt{Void}$, kendiniz yaratamazsınız ama başka yerden alabilirsiniz. Örneğin burada bir kanıt var$((P\Rightarrow Q) \mathbin{\&} \neg Q)\Rightarrow \neg P$:

f :: (a -> b, b -> Void) -> (a -> Void)
f (x, y) = \z -> y (x z)

Arayan kişinin tür değerini nereden aldığını makul bir şekilde merak edebilirsiniz $\texttt{Void}$ama bu arayanın sorunu, senin değil. Bir subproof içinde bir çelişki türetmek, mantığın tutarsız olduğu anlamına gelmez, sadece gerçek dünyada bu noktaya asla gerçekten ulaşamayacağınızı gösterdiğiniz anlamına gelir.