"Ngữ nghĩa giảm" là gì? Vui lòng giải thích việc sử dụng PLT Redex trong thuật ngữ của người quản lý

Question

Ai đó vui lòng giải thích cách sử dụng ngữ nghĩa giảm và PLT Redex bằng ngôn ngữ đơn giản hơn.

Cảm ơn.

Answer 1

Thuật ngữ giảm là kỹ thuật tính toán liên quan đến thay thế biểu thức bằng biểu thức tương đương (và hy vọng nhỏ hơn) cho đến khi không thể thay thế thêm. Nếu một ngôn ngữ là Turing-hoàn thành, có những biểu thức mà không bao giờ ngừng thay thế. Giảm

thường được ký hiệu bằng một mũi tên bên phải, và nó giải thích tốt nhất bằng ví dụ:

(3 + 7) + 5 --> 10 + 5 --> 15 

Điều này cho thấy ngữ nghĩa giảm tiêu chuẩn cho các biểu thức số học. Không thể giảm thêm bất kỳ biểu thức nào 15.

Hy vọng điều này sẽ hữu ích.

Answer 2

Ngữ nghĩa giảm tương tự (nếu không giống nhau?) Đối với ngữ nghĩa theo ngữ cảnh. Bất kỳ biểu thức nào cũng có thể được chia nhỏ thành ngữ cảnh và redex.

Cơ sở thực hành của Robert Harper cho ngôn ngữ lập trình (dự thảo PDF có sẵn here) phần 9.3 Ngữ nghĩa ngữ cảnh thực hiện một công việc thích hợp để giải thích chúng.

Một ví dụ:

print 5+4 
**context: print [], redex: 5+4 
**evaluate redex: 9 
**plug back into context 

print 9 
**context: [], redex: print 9 
**evaluate redex: nil ==> 9 
**plug back into context 

nil 

Bạn có thể 'dính' các REDEX trở lại vào 'lỗ' của bối cảnh để có được: in 5 + 4. Việc đánh giá diễn ra tại redex. Bạn phá vỡ một biểu thức thành một bối cảnh + redex, đánh giá redex để có được một biểu thức mới, cắm lại vào ngữ cảnh, rửa sạch và lặp lại.

Dưới đây là một ví dụ hơi phức tạp hơn đòi hỏi kiến ​​thức của một máy trừu tượng mà đánh giá các giải tích lambda:

(lambda x.x+1) 5 
**context: [] 5, redex: (lambda x.x+1) 
**evaluate redex: <(lambda x.x+1), {environment}> <- create a closure 
**plug back into context 

<(lambda x.x+1), {}> 5 
**context: [], redex: <(lambda x.x+1), {}> 5 
**evaluate redex: x+1 where x:=5 
**plug back into context 

x+1 where x:=5 
**context: []+1, redex: x 
**evaluate redex: 5 (since x:=5 in our environment) 
*plug back into context 

5+1... 
6 

EDIT: Phần khó khăn được nhận nơi để phá vỡ một biểu thức vào một bối cảnh & REDEX. Nó đòi hỏi kiến ​​thức về ngữ nghĩa hoạt động của ngôn ngữ (mà 'mảnh' của một biểu thức bạn cần để đánh giá tiếp theo).