Đây là một vấn đề đã khiến tôi khó chịu trong một thời gian, và tôi tự hỏi liệu có ai ở đây có thể giúp đỡ hay không.PLT Redex: tham số hóa định nghĩa ngôn ngữ
Tôi có một mô hình Redex PLT của một ngôn ngữ được gọi là lambdaLVar, ít nhiều là một phép tính lambda chưa được phân loại, nhưng được mở rộng bằng một cửa hàng có chứa "biến mạng" hoặc LVars. Một LVar là một biến có giá trị chỉ có thể tăng theo thời gian, nơi mà ý nghĩa của "tăng" được đưa ra bởi một bộ đặt hàng một phần (còn gọi là một mạng) mà người sử dụng của ngôn ngữ chỉ định. Do đó lambdaLVar thực sự là một gia đình của ngôn ngữ - khởi tạo nó với một mạng và bạn nhận được một ngôn ngữ; với một mạng tinh thể khác, và bạn có một cái lưới khác. Bạn có thể xem mã số here; nội dung quan trọng là ở lambdaLVar.rkt.
Trong định nghĩa trên giấy của lambdaLVar, định nghĩa ngôn ngữ được tham số hóa bởi mạng được người dùng chỉ định đó. Trong một thời gian dài, tôi đã muốn thực hiện cùng một kiểu tham số hóa trong mô hình Redex, nhưng cho đến nay, tôi đã không thể tìm ra cách. Một phần của sự cố là ngữ pháp của ngôn ngữ phụ thuộc vào cách người dùng khởi tạo mạng tinh thể: các phần tử của mạng trở thành các đầu cuối trong ngữ pháp. Tôi không biết làm thế nào để diễn tả một ngữ pháp trong Redex trừu tượng qua mạng tinh thể.
Trong thời gian chờ đợi, tôi đã cố gắng tạo lambdaLVar.rkt làm mô đun theo cách có thể. Ngôn ngữ được định nghĩa trong tệp đó là chuyên biệt cho một mạng cụ thể: các số tự nhiên với max là hoạt động ít nhất trên ràng buộc (lub). (Hoặc, tương đương, số tự nhiên được yêu cầu bởi <=. Đó là một mạng lưới rất nhàm chán.) Các phần duy nhất của mã cụ thể cho mạng đó là dòng (define lub-op max) gần đầu và natural xuất hiện trong ngữ pháp. (Có một metafunction lub được xác định trong điều khoản của người dùng chỉ định lub-op chức năng. Sau đó là chỉ là một chức năng vợt, vì vậy lub phải thoát ra Racket gọi lub-op.)
Trừ khả năng để thực sự xác định lambdaLVar theo cách trừu tượng qua sự lựa chọn của mạng, có vẻ như tôi phải có khả năng viết một phiên bản lambdaLVar với hầu hết các xương trần của mạng - chỉ là Bot và các yếu tố hàng đầu, nơi Bot < = Đầu - và sau đó sử dụng define-extended-language để thêm nội dung khác. Ví dụ, tôi có thể định nghĩa một ngôn ngữ được gọi là lambdaLVar-nat được chuyên biệt hóa cho Naturals lattice tôi đã mô tả:
;; Grammar for elements of a lattice of natural numbers.
(define-extended-language lambdaLVar-nats
lambdaLVar
(StoreVal .... ;; Extend the original language
natural))
;; All we have to specify is the lub operation; leq is implicitly <=
(define-metafunction/extension lub lambdaLVar-nats
lub-nats : d d -> d
[(lub-nats d_1 d_2) ,(max (term d_1) (term d_2))])
Sau đó, để thay thế hai quan hệ giảm slow-rr và fast-rr rằng tôi đã cho lambdaLVar, tôi có thể xác định một vài wrappers:
(define nats-slow-rr
(extend-reduction-relation slow-rr
lambdaLVar-nats))
(define nats-fast-rr
(extend-reduction-relation fast-rr
lambdaLVar-nats))
hiểu biết của tôi từ các tài liệu trên extend-reduction-relation là nó phải diễn giải các quy tắc trong slow-rr và fast-rr, nhưng sử dụng lambdaLVar-nat. Đưa tất cả điều này với nhau, tôi đã cố gắng chạy bộ ứng dụng thử nghiệm mà tôi đã có với một trong những, quan hệ giảm mở rộng mới:
> (program-test-suite nats-slow-rr)
Điều đầu tiên tôi nhận được là một đơn khiếu nại vi phạm hợp đồng: small-step-base: input (((l 3)) new) at position 1 does not match its contract. Dòng hợp đồng của các bước nhỏ cơ sở chỉ là #:contract (small-step-base Config Config), trong đó Config là một ngữ pháp nonterminal có một ý nghĩa mới nếu diễn giải lại dưới lambdaLVar-nats hơn nó đã làm theo lambdaLVar, vì các công cụ mạng cụ thể. Là một thử nghiệm, tôi đã loại bỏ các hợp đồng trên small-step-base và small-step-slow.
Sau đó tôi có thể thực sự chạy 19 chương trình thử nghiệm của mình, nhưng 10 trong số đó không thành công. Có lẽ không ngạc nhiên, tất cả những người thất bại là những chương trình sử dụng LVS tự nhiên có giá trị số theo một cách nào đó. (Phần còn lại là các chương trình "thuần túy" không tương tác với cửa hàng của LVars.) Vì vậy, các bài kiểm tra thất bại chính xác là những người sử dụng ngữ pháp mở rộng.
Vì vậy, tôi tiếp tục theo dõi hố thỏ, và có vẻ như Redex muốn tôi mở rộng tất cả các hình thức phán đoán hiện có và các mối liên hệ được liên kết với lambdaLVar-nats chứ không phải lambdaLVar. Điều đó có ý nghĩa, và nó có vẻ ổn cho các hình thức phán xét theo như tôi có thể nói, nhưng với các trục trặc tôi gặp rắc rối: Tôi muốn sự thay đổi mới quá tải cái cũ cùng tên (vì các hình thức phán xét hiện tại đang sử dụng nó) và dường như không có cách nào để làm điều đó. Nếu tôi phải đổi tên các metafunctions, nó sẽ đánh bại mục đích, bởi vì tôi sẽ phải viết toàn bộ các hình thức phán xét mới. Tôi cho rằng những gì tôi muốn là một sự kết thúc muộn của các cuộc gọi metafunction!
Câu hỏi của tôi tóm tắt: Có cách nào trong Redex tham số hóa định nghĩa ngôn ngữ theo cách tôi muốn hoặc mở rộng định nghĩa ngôn ngữ theo cách mà tôi muốn làm không? Tôi sẽ chỉ phải viết các macro tạo Redex?
Cảm ơn bạn đã đọc!