lambda演算求值順序的問題？

03-05

求值規則如圖(出自TAPL p72)
請問這種求值規則符合哪種求值策略(call-by-value call-by-name等)呢？

------------------------疑惑的分割線-----------------------------------
現在的問題出在了CBV的定義上。。。TAPL上是這麼描述CBV的：
按照這個說法一個redex可以被規約需要滿足兩個條件：

1. 最外層
2. 右側已經被規約到了一個value
可是E-APP1這一條卻不符合第二個條件，所以我才判斷這個不是CBV
------------------------恍然大悟的分割線-----------------------------------
找到了癥結所在。。。right-hand side of a redex是指redex內部的右側，比如(v1 v2)作為redex時v2就是這個redex的right-hand side。。。

這是call-by-value

你沒看懂這個operational semantics 主要有以下幾點原因：

1. 無論是call-by-value 還是call-by-name 都只對參數而言，在決定參數的求值（evaluation）之前先要完成函數的求值（即這裡的t1）。因為你不能保證程序中出現的函數調用語法全都是 ((lambda (x) lambda-body) argument) ，比如很有可能是(f argument)，而f 是一個variable，variable 不是value 所以還要去環境里找出f 到底引用了哪個lambda 才能進行下一步。

2. 第二條規則已經清楚的說明了t1 的位置上必須是個v（value），所謂value 就是解釋器中不再進一步解釋的東西，比如lambda abstraction。這也就暗示了做完上一條evaluation 的語法單元才能適用於這條規則。

3. 你說的outermost 意思是在非redex 情況下lambda 內部不求值。而「右面必需先reduce 到一個value」說的是在redex 中，即圖中的第三條規則。例如，((v1 v2) v3) 中的redex 是(v1 v2)，它的右面是v2