Réduire lambda-expressions WHNF

Question

Je dois réduire le suivant lambda-expression dans WHNF, mais je ne suis pas tout à fait sûr de savoir comment faire:

(λx y. x 3) (+ 4) (+ 6 7) 

Alors, comment puis-je le faire? Réduction d'appel par nom?

Est-ce que cette expression (autre exemple) est (λz x. (λx. x) z) x dans WHNF?

Answer 1

WHNF (faible Chef normal formulaire) signifie que vous avez soit une valeur (par exemple, un entier) ou l'expression est du genre (λx . e(x)) où e(x) est une expression qui peut contenir des références à x, donc en gros vous avez le le résultat est une fonction.

Dans votre cas, l'expression que vous avez contient certaines applications qui doivent être réduites:

(λx . λy. x 3) (+ 4) (+ 6 7) = (λy . (+ 4) 3) (+ 6 7) 
          = (+ 4) 3 
          = 7 

Notez que dans ce cas y ne figure pas dans le corps de la fonction, et donc la + 6 7 « disparait » pendant la réduction.

---

Non, (λz x. (λx. x) z) x est pas dans WHNF parce que le "opérateur haut" est encore une application. Notez que la réduction dans ce cas est un peu difficile car vous avez une variable libre x à l'extérieur et λ lie également x. Cependant, nous pouvons d'abord faire un certain renommage: (λz k. (λt. t) z) x et maintenant effectuer la réduction: (λk. (λt. t) x) et cela est maintenant dans WHNF. Notez que nous ne réduisons pas l'application (λt. t) x car elle se trouve à l'intérieur d'un λ. Pour vérifier si une expression est dans WHNF, vous devez la regarder comme une arborescence syntaxique. Considérons les deux exemples ci-dessus, et notons l'application explicitement par $. Rappelez-vous que l'application f x y est équivalente à (f x) y.

Dans le premier cas, l'expression était:

      | 
       +-------------$-----------+ 
       |       | 
     +---- $ ----    +---(+)---+ 
     |   |    |   | 
     λx   λt    6   7 
     |   | 
     λy  +-(+)-+ 
     |  |  | 
    +---$---+ t  4 
    |  | 
    x  3 

Comme vous pouvez voir la racine de l'arbre est un $, donc nous devons exécuter l'application. Pour ce faire, nous devons d'abord réduire le côté gauche, ce qui est encore une $ si celle-ci doit être réduite d'abord, l'obtention:

      | 
       +-------------$-----------+ 
       |       | 
       |     +---(+)---+ 
       |     |   | 
       |     6   7 
       |   
      λy  
       |  
      +---$---+ 
      |  | 
     λt  3 
      | 
     +-(+)-+ 
     |  | 
     t  4 

Maintenant à gauche nous avons un λ afin que nous puissions réduire le plus à l'extérieur l'application $:

   | 
      +---$---+ 
      |  | 
     λt  3 
      | 
     +-(+)-+ 
     |  | 
     t  4 

Et maintenant, la racine est toujours un $ donc nous devons réduire celle-là aussi:

  | 
     +-(+)-+ 
     |  | 
     3  4 

La racine est un +, donc nous réduisons l'obtention de nouveau:

| 
7 

Et maintenant nous sommes fait.

Dans le second cas, nous avons l'expression (λz . λk. ((λt. t) z)) x qui devient l'arbre:

   | 
    +-------$-----------------+ 
    |       | 
    λz      x 
    | 
    λk 
    | 
+----$----+ 
|   | 
λt  z 
| 
t 

Encore une fois la racine est un $ donc nous devons réduire:

 λk 
    | 
+----$----+ 
|   | 
λt  x 
| 
t 

Maintenant, nous avons un arbre dont la racine est λ, ce qui signifie que l'expression est dans WHNF, donc nous nous arrêtons.