Các loại chữ ký của một combinator không phù hợp với loại chữ ký của chức năng Lambda tương đương

Question

Cân nhắc combinator này:

S (S K) 

Áp dụng nó để các đối số XY:

S (S K) X Y 

Nó thu gọn lại để:

X Y 

Tôi đã chuyển đổi S (SK) thành các thuật ngữ Lambda tương ứng và nhận kết quả này:

(\x y -> x y) 

tôi sử dụng công cụ Haskell WinGHCi để có được những kiểu chữ ký của (\ x y -> x y) và nó trở lại:

(t1 -> t) -> t1 -> t 

Điều đó làm cho ý nghĩa với tôi.

Tiếp theo, tôi đã sử dụng WinGHCi để có được những kiểu chữ ký của s (s k) và nó trả về:

((t -> t1) -> t) -> (t -> t1) -> t 

Điều đó không có ý nghĩa đối với tôi. Tại sao các chữ ký kiểu khác nhau?

Lưu ý: Tôi định nghĩa s, k, và tôi như:

s = (\f g x -> f x (g x)) 
k = (\a x -> a) 
i = (\f -> f) 

Answer 1

Nhờ tất cả những ai đã trả lời câu hỏi của tôi. Tôi đã nghiên cứu câu trả lời của bạn. Để chắc chắn rằng tôi hiểu những gì tôi đã học được, tôi đã viết câu trả lời của riêng tôi cho câu hỏi của tôi. Nếu câu trả lời của tôi không đúng, xin vui lòng cho tôi biết.

Chúng tôi bắt đầu với các loại k và s: Tác phẩm đầu tay

k :: t1 -> t2 -> t1 
    k = (\a x -> a) 

    s :: (t3 -> t4 -> t5) -> (t3 -> t4) -> t3 -> t5 
    s = (\f g x -> f x (g x)) 

Hãy vào determing loại chữ ký của (s k).

Nhớ lại s 's định nghĩa:

s = (\f g x -> f x (g x)) 

Thay k cho f kết quả trong (\f g x -> f x (g x)) hợp đồng để:

(\g x -> k x (g x)) 

quan trọng Loại g và x phải phù hợp với k' s nhập chữ ký.

Nhớ lại rằng k có kiểu chữ ký này:

k :: t1 -> t2 -> t1 

Vì vậy, đối với chức năng định nghĩa k x (g x) này, chúng ta có thể suy ra:

• Loại x là loại đối số đầu tiên k 's , là loại t1.

• Loại đối số thứ hai của k là t2, do đó, kết quả của (g x) phải là t2.

• g có x làm đối số mà chúng tôi đã xác định có loại t1. Vì vậy, chữ ký loại (g x) là (t1 -> t2).

• Loại kết quả k là t1, do đó, kết quả của (s k) là t1.

Vì vậy, loại chữ ký của (\g x -> k x (g x)) là thế này:

(t1 -> t2) -> t1 -> t1 

Tiếp theo, k được định nghĩa để luôn luôn trả số đầu tiên của nó.Vì vậy, đây:

k x (g x) 

hợp đồng này:

x 

Và đây:

(\g x -> k x (g x)) 

hợp đồng này:

(\g x -> x) 

Được rồi, bây giờ chúng tôi đã tìm ra (s k) :

s k :: (t1 -> t2) -> t1 -> t1 
    s k = (\g x -> x) 

Bây giờ, hãy xác định chữ ký loại s (s k).

Chúng tôi tiến hành theo cách tương tự.

Nhớ lại s 's định nghĩa:

s = (\f g x -> f x (g x)) 

Thay (s k) cho f kết quả trong (\f g x -> f x (g x)) hợp đồng để:

(\g x -> (s k) x (g x)) 

quan trọng Loại g và x phải phù hợp với (s k)' s nhập chữ ký.

Nhớ lại rằng (s k) có kiểu chữ ký này:

s k :: (t1 -> t2) -> t1 -> t1 

Vì vậy, đối với chức năng định nghĩa (s k) x (g x) này, chúng ta có thể suy ra:

• Loại x là loại đối số đầu tiên (s k) 's , là loại (t1 -> t2).

• Loại đối số thứ hai của (s k) là t1, do đó kết quả của (g x) phải là t1.

• g có đối số của nó, mà chúng tôi đã xác định là loại (t1 -> t2). Vì vậy, chữ ký loại (g x) là ((t1 -> t2) -> t1).

• Loại kết quả của (s k) là t1, do đó, kết quả của s (s k) là t1.

Vì vậy, loại chữ ký của (\g x -> (s k) x (g x)) là thế này:

((t1 -> t2) -> t1) -> (t1 -> t2) -> t1 

Trước đó chúng tôi xác định rằng s k có định nghĩa này:

(\g x -> x) 

Nghĩa là, nó là một chức năng mà phải mất hai đối số và trả về giá trị thứ hai.

Vì vậy, điều này:

(s k) x (g x) 

Hợp đồng này:

(g x) 

Và đây:

(\g x -> (s k) x (g x)) 

hợp đồng này:

(\g x -> g x) 

OK, bây giờ chúng tôi đã tìm ra s (s k).

s (s k) :: ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1 
    s (s k) = (\g x -> g x) 

Cuối cùng, so sánh các loại chữ ký của s (s k) với kiểu chữ ký của chức năng này:

p = (\g x -> g x) 

Loại p là:

p :: (t1 -> t) -> t1 -> t 

p và s (s k) có cùng một định nghĩa (\g x -> g x) vậy tại sao chúng có chữ ký kiểu khác nhau?

Lý do mà s (s k) có chữ ký loại khác với p là không có ràng buộc nào trên p. Chúng tôi thấy rằng s trong (s k) bị ràng buộc phải nhất quán với chữ ký loại k và s đầu tiên trong s (s k) bị ràng buộc để nhất quán với chữ ký loại (s k). Vì vậy, chữ ký loại s (s k) bị hạn chế do đối số của nó. Mặc dù p và s (s k) có cùng định nghĩa, các ràng buộc trên g và x khác nhau.

Answer 2

Chúng tôi bắt đầu với các loại k và s

k :: t1 -> t2 -> t1 
k = (\a x -> a) 

s :: (t3 -> t4 -> t5) -> (t3 -> t4) -> t3 -> t5 
s = (\f g x -> f x (g x)) 

Vì vậy, đi qua k như là đối số đầu tiên của s, chúng tôi hợp nhất loại của k với loại đối số đầu tiên của s và sử dụng s tại loại

s :: (t1 -> t2 -> t1) -> (t1 -> t2) -> t1 -> t1 

do đó chúng tôi có được

s k :: (t1 -> t2) -> t1 -> t1 
s k = (\g x -> k x (g x)) = (\g x -> x) 

Sau đó, trong s (s k), bên ngoài s được sử dụng ở các loại (t3 = t1 -> t2, t4 = t5 = t1)

s :: ((t1 -> t2) -> t1 -> t1) -> ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1 

áp dụng đó để s k giảm các loại đối số đầu tiên và lá chúng tôi với

s (s k) :: ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1 

Tóm tắt: Trong Haskell, loại s (s k) có nguồn gốc từ các loại biểu thức con của nó, không phải do ảnh hưởng của nó đối với (các) đối số của nó. Vì vậy nó có một loại ít chung hơn so với biểu thức lambda biểu thị hiệu ứng của s (s k).

Answer 3

Hệ thống kiểu bạn đang sử dụng về cơ bản giống như phép tính lambda được nhập đơn giản (bạn không sử dụng bất kỳ hàm đệ quy hoặc loại đệ quy nào). Cách tính toán lambda đơn giản là không hoàn toàn chung chung; nó không phải là Turing-complete, và nó không thể được sử dụng để viết đệ quy chung.Phép tính kết hợp SKI là Turing-complete, và có thể được sử dụng để viết các bộ kết hợp điểm cố định và đệ quy chung; do đó, toàn bộ sức mạnh của phép tính kết hợp SKI không thể được thể hiện bằng phép tính lambda được đánh máy đơn giản (mặc dù nó có thể trong phép tính lambda chưa được phân loại).