Phương pháp hiện đại để giải các phương trình chức năng là gì?

Question

Giả sử rằng bạn muốn tìm một chương trình λ-calculus, T, thỏa mãn các phương trình sau:

(T (λ f x . x))   = (λ a t . a) 
(T (λ f x . (f x)))  = (λ a t . (t a)) 
(T (λ f x . (f (f x)))) = (λ a b t . (t a b)) 
(T (λ f x . (f (f (f x)))) = (λ a b c t . (t a b c)) 

Vào trường hợp này, nên tôi đã tìm thấy giải pháp này:

T = (λ t . (t (λ b c d . (b (λ e . (c e d)))) (λ b . b) (λ b . b))) 

Có bất kỳ chiến lược nào để giải các phương trình tính toán tự động như vậy? Tình trạng nghệ thuật về chủ đề đó là gì?

Answer 1

Nói chung, higher order unification là không thể xác định, vì vậy bạn không thể hy vọng cho một thủ tục chung để tìm giải pháp cho các loại phương trình này.

Đã có một số lượng đáng kể công việc tìm giải pháp cho các vấn đề như vậy, nhưng tôi không biết bất kỳ câu trả lời nào cho câu trả lời cho vấn đề cụ thể của bạn. Một số tài liệu tham khảo tốt được tóm tắt trong câu trả lời này: Higher-order unification

Answer 2

Tôi không chắc chắn về trạng thái của nghệ thuật, nhưng công việc của William E Byrd về phiên dịch quan hệ (chẳng hạn như this paper) cho phép tổng hợp chương trình loại này.

Ngoài ra, hãy xem số PolyConf talk của mình để biết một số nội dung thú vị về tìm kiếm cụm từ chương trình. Ví dụ của bạn có vẻ như họ sẽ khá dễ dàng để thể hiện theo cách đó.