Thực hiện combinator calculus

Question

Concept

Tôi đang thực hiện một thông dịch viên cho phép người dùng để xác định độc đoán combinators và áp dụng chúng với các điều khoản tùy ý. Ví dụ, người dùng có thể xác định Church encoding for pairs bằng cách nhập các định nghĩa combinator sau:

pair a b c → c a b 
true a b → a 
first a → a true 

Người dùng có thể sau đó nhập first (pair a b), được giảm từng bước theo các quy tắc được định nghĩa trước:

first (pair a b) 
→ pair a b true 
→ true a b 
→ a 

combinators khác cũng có thể được định nghĩa, chẳng hạn như những người sử dụng trong SKI combinator calculus:

S x y z → x z (y z) 
K x y → x 
I x → x 

các combi sắc nator cũng có thể được xác định theo hai tổ hợp đầu tiên theo số I → S S K K hoặc I → S K (K K) hoặc I = S K x. Sau đó, số điện thoại phổ dụng iota combinator có thể được xác định bởi:

ι x → x S K 

Những ví dụ này hy vọng minh họa những gì tôi đang cố gắng làm.

Thực hiện

Tôi đang cố gắng để thực hiện điều này bằng graph reduction và một hệ thống graph rewriting. Hãy tree là một kiểu dữ liệu được định nghĩa đệ quy bằng

tree = leaf | (tree tree) 

Đây là một cây nhị phân, nơi các nút có thể là lá (nút terminal) hoặc chi nhánh (hạch nội bộ) bao gồm một cặp subtrees. Các nhánh đại diện cho việc áp dụng một thuật ngữ cho một thuật ngữ khác, trong khi các lá đại diện cho các combinators và các đối số. Hãy rule là một kiểu dữ liệu được định nghĩa bởi

rule = (tree tree) 

này tương ứng với một quy tắc giảm biến đổi cây trái vào cây bên phải (một → b). Danh sách các rules sau đó có thể được xác định bởi

rules = rule | (rule rules) 

có hiệu quả, khi đánh giá một biểu thức như pair a b c → c a b, người phiên dịch xây dựng một cây có dạng (((pair a) b) c) tương ứng với phía bên tay trái, một cây có dạng ((c a) b) tương ứng với phía bên tay phải, xây dựng một cặp của cả hai cây tương ứng với rule (trong đó a,b,c được xác định bằng cách nào đó là tham số tùy ý và không nhất thiết là bộ phối hợp hoặc ký hiệu đầu cuối) và nối cặp này vào danh sách rules. Khi giảm một biểu thức có dạng first (pair a b), người phiên dịch xây dựng cây tương ứng (first ((pair a) b)) và áp dụng các quy tắc giảm thuế như sau:

(first ((pair a) b)) 
→ (((pair a) b) true) 
→ ((true a) b) 
→ a 

Để làm điều này, người phiên dịch phải thực hiện mô hình kết hợp trên cây và subtrees của nó, "di chuyển xung quanh "các combinators và tham số tùy ý để xây dựng một cây mới tương ứng với phía bên tay phải của quy tắc.An thực hiện ví dụ về cấu trúc cây trong C được cho bởi

struct tree_t { 
    bool is_leaf; 
    union { 
     char* symbol; 
     struct { 
      tree_t* left; 
      tree_t* right; 
     }; 
    }; 
}; 

Một chức năng khớp mẫu có thể được thực hiện như

bool matches(tree_t* pattern, tree_t* replacement) { 
    if (pattern -> is_leaf && replacement -> is_leaf) 
     //do stuff, return a boolean 
    else if (pattern -> is_leaf && replacement -> is_branch) 
     //do stuff, return a boolean 
    else if (pattern -> is_branch && replacement -> is_leaf) 
     //do stuff, return a boolean 
    else if (pattern -> is_branch && replacement -> is_branch) 
     return matches(pattern -> left, replacement -> left) && matches(pattern -> right, replacement -> right); 
     //The above tests for equality recursively by testing for equality in each subtree. 
} 

Tuy nhiên, tôi không chắc chắn làm thế nào để thực hiện chi tiết quan trọng của quá trình này, bao gồm :

1. Kết hợp cây đầu vào với cây LHS của quy tắc giảm.
2. Chuyển cây đầu vào thành cây RHS của quy tắc giảm, bảo toàn các thông số (có thể là lá hoặc cành) và "di chuyển chúng xung quanh" xung quanh vị trí thích hợp của chúng.

Tôi tin rằng khớp mẫu trên nút sẽ liên quan đến việc kiểm tra con trái và con phải của nút, v.v. cho đến khi đạt đến các nút đầu cuối. Có ai biết về một chương trình hoặc hướng dẫn trực tuyến đã thực hiện một khái niệm tương tự trong C và tôi có thể học hỏi từ? Tôi thậm chí còn đi đúng hướng trong việc tiếp cận vấn đề thông qua phương pháp này, hay là có một cách đơn giản hơn?

Answer 1

Bạn cần thực hiện theo hai bước riêng biệt. Trình ghép mẫu khớp với một mẫu đối với một cây và tạo các biến ánh xạ từ điển trong mẫu tới các giá trị trong cây.

Sau đó, bạn chuyển từ điển đó sang một hàm riêng biệt điền vào thay thế, bằng cách thay thế các biến bằng giá trị của chúng từ từ điển.

Cách tiếp cận đối sánh mẫu được mô tả trong SICP sẽ hoạt động tốt trong C, mặc dù bạn có thể thấy dễ dàng hơn khi sử dụng cấu trúc dữ liệu có thể thay đổi cho từ điển. Xem https://mitpress.mit.edu/sicp/full-text/sicp/book/node99.html