减少WHNF中的lambda表达式

Question

我必须将以下lambda表达式减少为WHNF,但我不太清楚如何做到这一点:

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

那么,我该怎么做？呼叫减少名称？

这个表达式(其他例子)(?z x. (?x. x) z) x在WHNF中了吗？

Answer 1

WHNF(弱头范式)意味着要么有一个值(例如整数)或表达是那种(?x . e(x))其中e(x)是可含有以引用的表达式x,所以基本上必须的结果是一个函数.

在您的情况下,您拥有的表达式包含一些需要减少的应用程序:

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

请注意,在这种情况下y,不会出现在函数体中,因此+ 6 7在缩小期间会"消失".

不,(?z x. (?x. x) z) x是不是在WHNF因为"顶运营商"仍是一个应用程序.请注意,这种情况的减少有点棘手,因为你有一个自由变量x在外面并且?也绑定x.但是我们可以先做一些重命名:(?z k. (?t. t) z) x现在执行减少:(?k. (?t. t) x)现在这是WHNF.请注意,我们不会减少应用程序,(?t. t) x因为它位于a ?.

要检查表达式是否在WHNF中,您必须将其视为语法树.让我们考虑上面的两个例子,让我们明确地表示应用程序$.请记住,该应用程序f x y相当于(f x) y.

在第一种情况下,表达式是:

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

正如您所看到的树的根是a $,所以我们必须执行应用程序.为了做到这一点,我们必须首先减少左侧,这也是必须首先减少左侧$,获得:

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

现在在左侧我们有一个,?所以我们可以减少最外层的应用程序$:

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

现在根仍然是一个$所以我们也必须减少那个:

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

根是a +,所以我们再次减少获得:

|
7

现在我们完成了.

在第二种情况下,我们有表达式(?z . ?k. ((?t. t) z)) x成为树:

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

根是一个$所以我们必须减少它:

     ?k
     |
+----$----+
|         |
?t        x
|
t

现在我们有一棵树,其根是?,这意味着表达式在WHNF中,所以我们停止.