gistfile1.txt

T[[#1 e]] = T[[e]] (λ x. λ y. x)

T[[(e₁, e₂)]] = λ f. f T[[e₁]] T[[e₂]]

T[[(e₁, e₂)]] = (λ x. λ y. λ f. f x y) T[[e₁]] T[[e₂]]


p = (λx.x, Ω)

* CBN w/ pairs

#1 p → λx.x

terminates

* CBV a

T[[#1 p]] = T[[p]] (λ x. λ y. x)
          = (λ x. λ y. λ f. f x y) T[[λx.x]] T[[Ω]] (λ x. λ y. x)
          = (λ x. λ y. λ f. f x y) λx.x      T[[Ω]] (λ x. λ y. x)
          → (λ y. λ f. f λx.x y) T[[Ω]] (λ x. λ y. x)
          = (λ y. λ f. f λx.x y) Ω (λ x. λ y. x)
          → (λ y. λ f. f λx.x y) Ω (λ x. λ y. x)
          ⋮

does not terminate?

* CBV b

T[[#1 p]] = T[[p]] (λ x. λ y. x)
          = (λ f. f T[[λx.x]] T[[Ω]]) (λ x. λ y. x)
          → (λ x. λ y. x) T[[λx.x]] T[[Ω]]
          = (λ x. λ y. x) (λx.x)    T[[Ω]]
          → (λ y. (λx.x)) T[[Ω]]
          = (λ y. (λx.x)) Ω
          → (λ y. (λx.x)) Ω
          → (λ y. (λx.x)) Ω
          ⋮

does not terminate?