Сбой проверки связанных переменных для комбинатора K - PullRequest
Новая
       92

Сбой проверки связанных переменных для комбинатора K

0 голосов
/ 31 октября 2018

Недавно у меня была копия "Основы языков программирования", второе издание. На странице 29 книга представляет следующую грамматическую схему для лямбда-исчисления со вкусом схемы: 

<expression> ::= <identifier>
             ::= (lambda (<identifier>) <expression>)
             ::= (<expression> <expression>)

Затем вводится определение (определение 1.3.3, стр. 31) свободных и связанных переменных, которое гласит: 

A variable x occurs free in a lambda calculus expression E if and only if

1. E is a variable reference and E is the same as x; or
2. E is of the form (lambda (y) E'), where y is different from x and x occurs free in E'; or
3. E is of the form (E1 E2) and x occurs free in E1 or E2.

A variable x occurs bound in a lambda calculus expression E if and only if

1. E is of the form (lambda (y) E'), where x occurs bound in E' or x and y are the same variable and y occurs free in E'; or
2. E is of the form (E1 E2) and x occurs bound in E1 or E2.

Такое определение затем легко трансформируется в две процедуры Scheme, называемые соответственно occurs-free? и occurs-bound?: 

(define occurs-free?
  (lambda (var exp)
    (cond
      ((symbol? exp) (eqv? exp var))
      ((eqv? (car exp) 'lambda)
       (and (not (eqv? (caadr exp) var))
            (occurs-free? var (caddr exp))))
      (else (or (occurs-free? var (car exp))
                (occurs-free? var (cadr exp)))))))

(define occurs-bound?
  (lambda (var exp)
    (cond
      ((symbol? exp) #f)
      ((eqv? (car exp) 'lambda)
       (or (occurs-bound? var (caddr exp))
           (and (eqv? (caadr exp) var)
                (occurs-free? var (caddr exp)))))
      (else (or (occurs-bound? var (car exp))
                (occurs-bound? var (cadr exp)))))))

Можно ожидать, что occurs-bound? вернет #t, когда комбинаторы (т.е. процедуры, состоящие только из связанных переменных) будут поданы в качестве входных данных. Однако тест для комбинатора K не пройден: 

> (occurs-bound? 'x '(lambda (c) (lambda (x) c)))
#f

Это связано с тем, что пункт 1. в определении связанных переменных гласит, что для привязки переменной она должна быть количественно определена в лямбда-выражении, а затем появиться свободной в своем теле. Поскольку x игнорируется в теле внутренней лямбды, тест возвращает false.

Очевидно, что occurs-bound? не представлено в третьем издании, поэтому невозможно провести какое-либо сравнение с самым последним изданием книги.

Является ли приведенное выше определение ошибочным или я что-то упустил? Вот ответ для кода .

Спасибо

1 Ответ

0 голосов
/ 31 октября 2018

Почему это должно быть ошибочным? Каково происхождение ваших подозрений?

'x встречается ли в '(lambda (c) (lambda (y) c))?

'x встречается ли в '(lambda (c) (lambda (z) c))?

Вам кажется странным, что это не так? Я бы не ожидал. Тогда почему его следует считать связанным в альфа-эквиваленте '(lambda (c) (lambda (x) c)), тогда?

Это не должно. Это даже не там.

...