2015-02-08 31 views
5

Tôi có một sự hiểu lầm trong khi chuyển đổi công thức logic đơn giản thành biểu thức lambda (bằng chứng về công thức đó).Biểu thức lambda Haskell và công thức logic đơn giản

Vì vậy, tôi có công thức sau: ((((A-> B) -> A) -> A) -> B) -> B trong đó -> có nghĩa là toán tử logic.

Tôi có thể viết một số biểu thức lambda bằng bất kỳ ngôn ngữ chức năng nào (Haskell, tốt hơn) tương ứng với nó?

Tôi có một số "kết quả" nhưng tôi thực sự không chắc chắn rằng nó là cách chính xác để làm điều này:

  • (((lambda F -> lambda A) -> A) -> lambda B) -> B
  • ((((lambda A -> lambda B) -> A) -> A) -> B) -> B.

Làm thế nào nó có thể được thể tranform công thức vào lambda biểu hiện? Nó sẽ rất hữu ích nếu bạn biết một số tài liệu đề cập đến vấn đề này.

Cảm ơn

+2

Đây là một vấn đề phức tạp. Phép tính liên tiếp trực giác LJ và các kết quả liên quan của nó đóng vai trò quan trọng trong giải pháp "tiêu chuẩn" của nó. Công cụ Djinn là một "nổi tiếng" thực hiện một tìm kiếm bằng chứng trong hệ thống này (gần), và các isomorphism Curry-Howard cho phép trình bày các bằng chứng này là điều khoản lambda. – chi

+3

Hơn nữa, không có một thứ như "chuyển đổi" một công thức thành một biểu thức lambda.Điều đó sẽ tạo ra các định lý "chuyển đổi" thành chứng minh của chúng, điều này là vô nghĩa - các định lý thừa nhận nhiều bằng chứng khác biệt, nói chung. Tốt nhất, bạn có thể thực hiện tìm kiếm bằng chứng, nơi bạn tìm kiếm một bằng chứng như vậy. – chi

+1

Cảm ơn bạn đã làm rõ. Tôi thực sự vui mừng với rất nhiều thông tin hữu ích trong thời gian ngắn. –

Trả lời

10

Đây là thời điểm tuyệt vời để sử dụng chế độ tương tác của Agda. Nó giống như một trò chơi. Bạn cũng có thể làm điều đó bằng tay nhưng nó hoạt động nhiều hơn. Dưới đây là những gì tôi đã làm:

f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B 
f x = ? 

Goal: B 
x : (((A -> B) -> A) -> A) -> B 

Về cơ bản di chuyển duy nhất chúng ta có là để áp dụng x, vì vậy chúng ta hãy cố gắng đó.

f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B 
f x = x ? 

Goal: ((A -> B) -> A) -> A 
x : (((A -> B) -> A) -> A) -> B 

Bây giờ mục tiêu của chúng tôi là một loại chức năng, vì vậy hãy thử một lambda.

f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B 
f x = x (\y -> ?) 

Goal: A 
x : (((A -> B) -> A) -> A) -> B 
y : (A -> B) -> A 

Chúng ta cần một A, và y có thể cung cấp cho chúng tôi nếu chúng tôi cung cấp nó với lập luận đúng. Bạn không chắc chắn đó là những gì nêu ra, nhưng y là đặt cược tốt nhất của chúng tôi:

f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B 
f x = x (\y -> y ?) 

Goal: A -> B 
x : (((A -> B) -> A) -> A) -> B 
y : (A -> B) -> A 

mục tiêu của chúng tôi là một loại chức năng vì vậy hãy sử dụng một lambda.

f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B 
f x = x (\y -> y (\z -> ?)) 

Goal: B 
x : (((A -> B) -> A) -> A) -> B 
y : (A -> B) -> A 
z : A 

Bây giờ chúng ta cần một B, và điều duy nhất mà có thể cung cấp cho chúng ta một Bx, vì vậy hãy thử lại.

f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B 
f x = x (\y -> y (\z -> x ?)) 

Goal: ((A -> B) -> A) -> A 
x : (((A -> B) -> A) -> A) -> B 
y : (A -> B) -> A 
z : A 

Bây giờ mục tiêu của chúng tôi là một loại chức năng trở A, nhưng chúng tôi có z mà là một A nên chúng tôi không cần phải sử dụng các đối số. Chúng tôi sẽ bỏ qua nó và trả lại z.

f : {A B : Set} -> ((((A -> B) -> A) -> A) -> B) -> B 
f x = x (\y -> y (\z -> x (\_ -> z))) 

Và ở đó bạn đi!

+0

Thật tuyệt vời! Đó là câu trả lời thực sự tốt nhất và nhanh nhất mà tôi từng thấy ở đây. Cảm ơn bạn rất nhiều. Tôi đã cài đặt Coq và đã cố gắng sử dụng nó nhưng tôi không thể đọc đầu ra. Nó quá phức tạp: ( –

+0

Tôi sẽ cố gắng sử dụng Agda theo lời khuyên của bạn. Thật kỳ lạ là chúng tôi không xem xét các ứng dụng như vậy và đã làm tất cả mọi thứ bằng tay ngay cả khi không có quy tắc đã đề cập! Cảm ơn bạn rất nhiều. –

+0

Ehm, nếu tôi hiểu bạn đúng câu trả lời có thể được viết lại theo cách sau: x (lambda y -> y (\ lambda z -> x (z)))? –