Sự khác nhau giữa Program Fixpoint và Function trong Coq là gì?

Question

Chúng dường như có mục đích tương tự. Sự khác biệt mà tôi đã nhận thấy cho đến thời điểm này là trong khi Program Fixpoint sẽ chấp nhận một biện pháp hợp chất như {measure (length l1 + length l2) }, Function dường như từ chối điều này và sẽ chỉ cho phép {measure length l1}.

Có phải Program Fixpoint nghiêm ngặt hơn Function hoặc chúng phù hợp hơn cho các trường hợp sử dụng khác nhau không?

Answer 1

Điều này có thể không phải là một danh sách đầy đủ, nhưng nó là những gì tôi đã tìm thấy cho đến nay:

• Như bạn đã đề cập, Program Fixpoint cho phép các biện pháp để xem xét nhiều hơn một đối số.
• Function tạo một câu hỏi foo_equation bổ đề có thể được sử dụng để viết lại các cuộc gọi tới foo bằng RHS của nó. Rất hữu ích để tránh các vấn đề như Coq simpl for Program Fixpoint.
• Trong một số trường hợp (đơn giản?), Function có thể xác định foo_ind bổ đề để thực hiện cảm ứng dọc theo cấu trúc của các cuộc gọi đệ quy foo. Một lần nữa, rất hữu ích để chứng minh những điều về foo mà không lặp lại hiệu quả đối số chấm dứt trong bằng chứng.
• Program Fixpoint có thể bị lừa để hỗ trợ đệ quy lồng nhau, xem https://stackoverflow.com/a/46859452/946226. Đây cũng là lý do tại sao Program Fixpoint có thể define the Ackermann chức năng khi Function không thể.