Tôi chưa bao giờ gặp phải điều như vậy và tôi chỉ có một cái nhìn chi tiết hơn. Có một lý do tính toán âm thanh để không thực hiện điều này theo mặc định - người ta phải chủ yếu tạo ra tất cả các kết hợp của đầu vào trước khi khớp mẫu hoặc bạn phải tạo giá trị sản phẩm chéo đầy đủ của mệnh đề kết hợp.
Tôi nghi ngờ rằng cách thông thường để thực hiện điều này sẽ đơn giản là viết cả hai mẫu (trong trường hợp nhị phân), tức là, có các mẫu cho cả C or $X và $X or C.
Tùy thuộc vào tổ chức dữ liệu cơ bản (thường là bộ dữ liệu), kết hợp mẫu này sẽ liên quan đến việc sắp xếp lại thứ tự các phần tử tuple, rất lạ (đặc biệt trong môi trường được gõ mạnh!). Nếu đó là danh sách thay vào đó, sau đó bạn đang trên mặt đất thậm chí còn run rẩy hơn.
Ngẫu nhiên, tôi nghi ngờ rằng các hoạt động cơ bản bạn muốn là mô hình công đoàn rời nhau trên bộ, ví dụ:
foo (Or ({C} disjointUnion {X})) = ...
Môi trường lập trình duy nhất mà tôi đã nhìn thấy rằng giao dịch với bộ tại bất kỳ chi tiết sẽ là Isabelle/HOL và tôi vẫn không chắc chắn rằng bạn có thể xây dựng các đối sánh mẫu trên chúng.
EDIT: Có vẻ như chức năng function của Isabelle (thay vì fun) sẽ cho phép bạn xác định các mẫu phức tạp không phải là nhà xây dựng, ngoại trừ bạn phải chứng minh rằng chúng được sử dụng nhất quán và bạn không thể sử dụng trình tạo mã nữa.
EDIT 2: Con đường tôi thực hiện chức năng tương tự trên n giao hoán, kết hợp và bắc cầu nhà khai thác là thế này:
thuật ngữ của tôi đã có dạng A | B | C | D, trong khi truy vấn là có dạng B | C | $X, nơi $X được phép phù hợp không hoặc nhiều thứ. Tôi đã sắp xếp trước những thứ này bằng cách sử dụng thứ tự từ vựng, để các biến luôn xuất hiện ở vị trí cuối cùng.
Trước tiên, bạn xây dựng tất cả các kết quả trùng khớp theo cặp, bỏ qua các biến cho bây giờ và ghi lại các biến phù hợp với quy tắc của bạn.
{ (B,B), (C,C) }
Nếu bạn coi đây là biểu đồ hai bên, thì về cơ bản bạn đang làm một vấn đề perfect marriage. Có tồn tại các thuật toán nhanh cho việc tìm kiếm các.
Giả sử bạn tìm thấy một, sau đó bạn thu thập tất cả mọi thứ mà không xuất hiện ở phía bên trái của mối quan hệ của bạn (trong ví dụ này, A và D), và bạn nhét chúng vào biến $X, và phù hợp với bạn là hoàn thành. Rõ ràng bạn có thể thất bại ở bất kỳ giai đoạn nào ở đây, nhưng điều này chủ yếu sẽ xảy ra nếu không có biến miễn phí trên RHS, hoặc nếu tồn tại một hàm tạo trên LHS không khớp với bất kỳ thứ gì (ngăn cản bạn tìm một kết quả hoàn hảo).
Xin lỗi nếu điều này bị nhầm lẫn một chút. Đã một thời gian kể từ khi tôi viết mã này, nhưng tôi hy vọng điều này sẽ giúp bạn, thậm chí một chút!
Để lưu nội dung này, có thể không phải là cách tiếp cận tốt trong mọi trường hợp. Tôi đã có khái niệm rất phức tạp về 'trận đấu' trên subterms (tức là, không đơn giản bình đẳng), và vì vậy xây dựng bộ hoặc bất cứ điều gì sẽ không làm việc. Có lẽ điều đó sẽ làm việc trong trường hợp của bạn mặc dù và bạn có thể tính toán các công đoàn tách rời trực tiếp.
Tôi không chắc chắn tôi đồng ý với sự nhầm lẫn của bạn đối sánh mẫu Prolog và so khớp mẫu ML. ML mô hình phù hợp hoàn toàn là cú pháp, và trong Prolog tôi không tin rằng đây là trường hợp. – Gian
Tôi không nói chúng giống nhau, chỉ có chúng có điểm chung so với các yếu tố theo thứ tự nghiêm ngặt. – rwallace
Tôi giả sử phần mềm chứng minh định lý chuyên dụng như Otter đã thực hiện điều này bằng cách đặt các công thức logic dưới dạng bình thường và xử lý các mệnh đề như cấu trúc dữ liệu đã đặt, tốn thời gian O (n log n) cho cả việc tạo và xác minh. Trong thực tế, tôi cho rằng chúng đã được lập trình tối ưu hóa cho các hoạt động cho các thuộc tính như kết hợp và giao hoán. –