时间戳

首页 > 解决方案 > 小打字机。我不明白 λ 最初的第二条诫命的含义

racket - 小打字机。我不明白 λ 最初的第二条诫命的含义

问题描述

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

我想做的是定义一个与（λ（y）（fy））不同的函数，当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)

标签： racketlambda-calculustype-theorypie-lang

解决方案

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

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

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

（我选择以这种方式编写声明以强调我们正在考虑函数内部的函数。）

为了了解我们的方向，这个简单的函数g需要两个Nat参数，并返回第一个。

让我们调用内部函数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“接受两个（咖喱）参数并返回第一个”的函数开始。然后，我们围绕内部函数引入了一个错误的 eta 扩展。结果，我们最终得到了一个g1“接受两个（咖喱）参数并返回第二个”的函数。显然不等同于原来的功能g。

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

重要的提示：

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

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

推荐阅读