Làm cách nào để tránh lỗi tràn hoặc lỗi phân đoạn trong Coq nats?

Question

Tôi hiện đang làm việc với vellvm, phát triển một chuyển đổi trên đó. Tôi là một người mới.

Trong khi lập trình, tôi phải đối mặt với cảnh báo sau đây:

Warning: Stack overflow or segmentation fault happens when working with large numbers in nat (observed threshold may vary from 5000 to 70000 depending on your system limits and on the command executed).

chức năng của tôi mà tạo ra cảnh báo này sẽ tính toán một chữ ký. Chữ ký được chia thành các bit cao cấp và kém hơn. Với hai nats n1 và n2 đại diện cho các bit cao cấp và các bit kém hơn, nó tính toán (n1 * 65536) + n2 - đây là một sự trừu tượng để đặt hai số nhị phân 16 bit cạnh nhau.

Tôi khá ngạc nhiên vì định nghĩa coq nat xuất hiện để xử lý các int lớn từ bên ngoài, nhờ vào hàm tạo S.

Tôi nên tránh cảnh báo này/sử dụng số lớn trong coq như thế nào? Tôi đang mở để thay đổi việc triển khai từ nat thành một số loại xây dựng nhị phân.

Cảm ơn!

Answer 1

Thay vì sử dụng loại nat trong Coq, đôi khi (khi bạn phải thao tác số lớn) tốt hơn để sử dụng loại Z, đây là sự chính thức hóa các số nguyên sử dụng biểu diễn cặp độ lớn dấu. Sự cân bằng là bằng chứng của bạn có thể phức tạp hơn một chút; nat rất đơn giản và do đó thừa nhận các nguyên tắc chứng minh đơn giản.

Tuy nhiên, trong Coq, có một cách sử dụng rộng rãi ký hiệu để làm cho nó dễ dàng hơn để viết các định nghĩa, định lý và chứng minh. Coq có một hạt nhân cực nhỏ (chúng tôi muốn điều này bởi vì chúng tôi muốn có thể tin rằng trình kiểm tra bằng chứng là chính xác, và chúng tôi có thể đọc điều đó) với nhiều ký hiệu trên đầu trang của nó. Tuy nhiên, vì có những biểu diễn khác nhau của sự vật, và chỉ có một vài biểu tượng tốt, ký hiệu của chúng tôi thường xung đột. Để vượt qua điều này, coq sử dụng interpretation scopes để phân biệt các ký hiệu và phân giải chúng thành các tên (vì "+" có nghĩa là add, plus, v.v ...).

Bạn chính xác, sử dụng Z_scope là ở đâu, + cho plus trong vòng Z.