Đâ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 B
là x
, 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!
Đâ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
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
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. –