Que sont les "sémantiques de réduction"? S'il vous plaît expliquer l'utilisation de PLT Redex dans le terme profane

Question

Quelqu'un s'il vous plaît expliquer l'utilisation de la sémantique de réduction et le PLT Redex dans un langage plus simple.

Merci.

Answer 1

La sémantique de réduction est une technique de calcul qui implique en remplaçant une expression par une expression équivalente (et, espérons-le plus petite) jusqu'à ce que plus aucun remplacement n'est possible. Si une langue est Turing-complete, il y a des expressions qui n'arrêtent jamais de remplacer.

La réduction est généralement transcrite par une flèche droite, et il est mieux expliqué par exemple:

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

Cela montre la sémantique standard de réduction pour les expressions arithmétiques. L'expression 15 ne peut plus être réduite.

Espérons que cela aide.

Answer 2

La sémantique de réduction est similaire (sinon la même?) À la sémantique contextuelle. Toute expression peut être décomposée en un contexte et redex.

Fondements pratiques de Robert Harper pour les langages de programmation (version PDF disponible here) section 9.3 La sémantique contextuelle explique assez bien les problèmes.

Un exemple:

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 

Vous pouvez 'coller' le redex de nouveau dans le 'trou' du contexte pour obtenir: print 5 + 4. L'évaluation a lieu au redex. Vous cassez une expression dans un contexte + redex, évaluez le redex pour obtenir une nouvelle expression, replacez-la dans le contexte, rincez et répétez.

Voici un exemple un peu plus complexe qui nécessite la connaissance d'une machine abstraite qui permet d'évaluer le calcul 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 partie la plus délicate consiste à reconnaître où briser une expression dans un contexte & Redex. Il nécessite une connaissance de la sémantique opérationnelle de la langue (quelle «pièce» d'une expression que vous devez évaluer ensuite).