¿Qué es la "semántica de reducción"? Explique el uso de PLT Redex en términos sencillos

Question

Alguien explique el uso de la semántica de reducción y el PLT Redex en un lenguaje más simple.

Gracias.

Answer 1

Semántica de reducción es una técnica de cálculo que implica que reemplaza una expresión por una expresión equivalente (y con suerte más pequeña) hasta que no sea posible reemplazarla. Si un idioma es Turing-completo, hay expresiones que nunca dejan de reemplazarse. Reducción

se suele anotada por una flecha hacia la derecha, y se explica mejor con el ejemplo:

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

Esto demuestra la semántica de reducción estándar para las expresiones aritméticas. La expresión 15 no se puede reducir más.

Espero que esto ayude.

Answer 2

La semántica de reducción es similar (si no es la misma?) A la semántica contextual. Cualquier expresión se puede dividir en un contexto y redex.

Fundamentos prácticos de Robert Harper para lenguajes de programación (borrador en PDF disponible here) sección 9.3 La semántica contextual hace un trabajo decente al explicarlos.

Un ejemplo:

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 

Puede 'palo' del redex de nuevo en el 'agujero' del contexto para obtener: impresión del 5 + 4. La evaluación ocurre en redex. Se divide una expresión en un contexto + redex, se evalúa redex para obtener una nueva expresión, se vuelve a conectar al contexto, se enjuaga y se repite.

Aquí está un ejemplo un poco más complicado que requiere el conocimiento de una máquina abstracta que evalúa el cálculo 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: La parte difícil es reconocer dónde romper una expresión en un contexto & redex. Requiere conocimiento de la semántica operacional del lenguaje (qué 'pieza' de una expresión necesita evaluar a continuación).