2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки


Правила форума


Посмотреть правила форума



Начать новую тему Ответить на тему
 
 Глупые вопросы по основам лямбда-исчисления
Сообщение23.11.2019, 20:17 


30/04/18
7
Читаю "Типы в языках программирования" Пирса, на стр. 61 русского издания:
Изображение

Тут два места, которые я не могу понять:

1. Последний переход (выделенный красным). Если вдруг терм $v$ содержит переменную $f$ как свободную, то разве мы не должны при бета-редукции подставить вместо нее терм $w$ и получить, вообще говоря, терм, отличный от $v$?

2. Не проще ли определить терм $test$ как $\lambda x.x$? Казалось бы, тогда мы в одну редукцию (вместо трех) придем к $tru\;v\;w$.

 Профиль  
                  
 
 Re: Глупые вопросы по основам лямбда-исчисления
Сообщение23.11.2019, 20:25 
Заслуженный участник


27/04/09
28128
xz121 в сообщении #1427368 писал(а):
1. Последний переход (выделенный красным). Если вдруг терм $v$ содержит переменную $f$ как свободную, то разве мы не должны при бета-редукции подставить вместо нее терм $w$ и получить, вообще говоря, терм, отличный от $v$?
Я думаю, там выше должно было быть написано, что мы воспринимаем термы с точностью до α-конверсии и что мы заменяем переменные, если вдруг при подстановке они бы замкнулись. Здесь ровно такой случай: если в $v$ свободна $f$, подстановка $(\lambda f. t)[t\mapsto v]$ в строгом смысле запрещена, но если мы заменим $f$ на свежую переменную — или заранее выбрали её аккуратно — то мы сможем заменить и получить терм $\lambda f.v$, где в $v$ обязательно нет свободных вхождений $f$. Потому дальше всё норм.

xz121 в сообщении #1427368 писал(а):
2. Не проще ли определить терм $test$ как $\lambda x.x$? Казалось бы, тогда мы в одну редукцию (вместо трех) придем к $tru\;v\;w$.
Да, можно. Определение в тексте просто ради наглядности, ну и при некоторых стратегиях вычисления оно может быть предпочтительнее, чем просто $I$.

-- Сб ноя 23, 2019 22:27:14 --

Кстати Пирса вы хорошо выбрали. :-) Там вроде есть и какие-то пояснения дальше, и если будет совсем плохо, откройте оригинал, и там может быть небольшая разница в словах (хотя перевод этого кусочка по-моему чистый).

 Профиль  
                  
 
 Re: Глупые вопросы по основам лямбда-исчисления
Сообщение23.11.2019, 20:44 


30/04/18
7
arseniiv
Спасибо!
Как выяснилось, явно про альфа-конверсию написано на 10 страниц позже, а тут, видимо, подразумевалось как очевидное :)

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 3 ] 

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: oleg_2


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group