小打字机。不明白λ初二诫的意思

Question

我尝试了以下示例，但无论是否发生，函数 f returns 应用后与 (λ(y)(f y)) 相同的值。

我想做的是定义一个与 (λ (y)(f y)) 不同的函数 (-> Y X) 当 y 出现在 y 中作为反例时，但我没有知道怎么做。

我是不是误解了λ初二戒的意思？

 

;;y does not occurs
(claim f (-> Nat Nat))
(define f
  (λ(y)
    0))

;; both return (the Nat 0)
(f 5)
((the (-> Nat Nat)
   (λ(y)
     (f y)))
  5)


;; y occurs
(claim g  (-> Nat Nat))
(define g
  (λ(y)
    y))

;;both return (the Nat 5)
(g 5)
((the (-> Nat Nat)
   (λ(y)
     (g  y)))
  5)

Answer 1

为了创建一个示例来说明警告“...只要 y 不出现在 f”的重要性，我们需要创建一个函数 f 其中名字 y 出现 free。 y 在 f 中免费的规定很关键。这也是为什么很难创建这样一个示例的原因：（顶级）函数不能包含自由变量。但是，interior 其他函数的函数可以。这是关键。

这是函数 g，其中包含另一个函数：

(claim g (-> Nat
           (-> Nat
             Nat)))
(define g
  (lambda (y)
    (lambda (x)  ;; Call this inner
      y)))       ;; function "f"

（我选择这样写声明是为了强调我们正在考虑函数内部的函数。）

为了得到我们的支持，这个简单的函数 g 需要两个 Nat 个参数，returns 第一个。

让我们调用内部函数f。请注意，f 包含一个自由变量 y（因此，f 在 g 之外是没有意义的）。让我们用 (lambda (y) (f y)) 代替 f:

(claim g1 (-> Nat
            (-> Nat
              Nat)))
(define g1
  (lambda (y)
    (lambda (y)     ;; Here we've replaced "f"
      ((lambda (x)  ;; with an eta-expanded
         y)         ;; version, introducing
       y))))        ;; the name "y"

我们可以消除应用程序以产生以下表达式：

g1
---------------- SAME AS
(lambda (y)
  (lambda (y)
    ((lambda (x)
       y)
     y)))
---------------- SAME AS
(lambda (y)
  (lambda (y)
    y))
---------------- SAME AS
(lambda (y)
  (lambda (y1)
    y1))

在最后一步中，我将第二个 y 重命名为 y1 以说明内部函数主体中的变量指的是更近的绑定站点，而不是更远的绑定站点一.

回顾一下，我们从一个函数 g 开始，它“接受两个（柯里化的）参数和 returns 第一个 ”。然后我们围绕内部函数引入了错误的 eta 扩展。结果，我们最终得到了一个函数 g1，它“接受两个（curried）参数和 returns second”。显然不等同于原函数g.

所以这条诫命是关于变量捕获的，这是我们为使用名称而付出的代价。希望对您有所帮助！

重要提示：

由于 Pie 检查类型的方式，如果您想尝试这个示例，您需要在 g 的正文中引入注释：

(claim g1 (-> Nat
            (-> Nat
              Nat)))
(define g1
  (lambda (y)
    (lambda (y)
      ((the (-> Nat Nat)
         (lambda (x)
           y))
       y))))

小打字机。不明白λ初二诫的意思

The Little Typer. I don't understand the meaning of The Initial Second Commandment of λ

type-theory

lambda-calculus

racket

pie-lang