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

Question

I have tried following examples, but no matter y occurred or not, The function f returns the same value as (λ(y)(f y)) after application.

I would like to do is to define a function that is not the same (-> Y X) as (λ (y)(f y)) when y occurred in y as a counter example, but I don't know how.

Do I misunderstand the meaning of The Initial Second Commandment of λ?

 

;;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

In order to create an example illustrating the importance of the caveat "...as long as y does not occur in f", we need to create a function f in which a name y occurs free. The provision that y is free in f is critical. This is also why it is difficult to create such an example: (top-level) functions cannot contain free variables. However, functions that are interior to other functions can. This is the key.

Here is function g that contains another function inside of it:

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

(I've chosen to write the claim in this way to emphasize that we are thinking about a function inside of a function.)

To get our bearings, this simple function g expects two Nat arguments, and returns the first.

Let's call the inner function f. Note that f contains a free variable y (for this reason, f is meaningless outside of g). Let's substitute (lambda (y) (f y)) for 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"

We can eliminate the application to produce the following expression:

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))

In the last step, I've renamed the second y to y1 to illustrate that the variable in the body of the inner function refers to the closer binding site, and not the farther one.

To recap, we started with a function g that "takes two (curried) arguments and returns the first". We then introduced a faulty eta-expansion around the inner function. As a result, we ended up with a function g1 that "takes two (curried) arguments and returns the second". Clearly not equivalent to the original function g.

So this commandment is about variable capture, which is the price we pay for working with names. I hope that helps!

IMPORTANT NOTE:

Due to the way that Pie checks types, you will need to introduce an annotation in the body of g if you want to try this example out:

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