PS
Dmitry Sokolov
Почему в префиксной нотации сначала стоят оба оператора, а потом операнды?
Потому что автор этой нотации, Ян Лукасевич, хотел составлять выражения без применения скобок.
Size: a a a
2020 March 09
МБ
Так что тут как ни крути - со всех сторон вылазит одна и та же сущность. 😊
Индексы де Бройна (или де Брауна)!
AK
Де Брёйн :)
AT
Индексы де Бройна (или де Брауна)!
Тут же нет переменных - при чём тут де Браун? 😊
МБ
Тут же нет переменных - при чём тут де Браун? 😊
Так как раз исключение переменных через введение окружения в виде стека. Ну. Это моя личная ересь, но, ведь, так и получается, если на оп. семнтику смотреть.
AT
Так как раз исключение переменных через введение окружения в виде стека. Ну. Это моя личная ересь, но, ведь, так и получается, если на оп. семнтику смотреть.
Резонно. Особенно если учесть, что лямбды тоже образуют дерево.
Но в начальном вопросе-то ни лямбд, ни переменных и близко не было. 😊
Но в начальном вопросе-то ни лямбд, ни переменных и близко не было. 😊
МБ
Резонно. Особенно если учесть, что лямбды тоже образуют дерево.
Но в начальном вопросе-то ни лямбд, ни переменных и близко не было. 😊
Но в начальном вопросе-то ни лямбд, ни переменных и близко не было. 😊
Но в итоге всегда приходят к одной конструкции. Потому что она объективна, потому что само лямбда-исчисление неотъемлемо связано с самой логикой.
МБ
Forth неизбежен :) Хотя, конечно, созадвался на других основаниях.
AT
Но в итоге всегда приходят к одной конструкции. Потому что она объективна, потому что само лямбда-исчисление неотъемлемо связано с самой логикой.
Оно связано только с математической логикой. К ней далеко-оо не все доходят. 😃
AT
Forth неизбежен :) Хотя, конечно, созадвался на других основаниях.
"Forth так же неисчерпаем, как и атом!" 😂
PS
Но в итоге всегда приходят к одной конструкции. Потому что она объективна, потому что само лямбда-исчисление неотъемлемо связано с самой логикой.
Ну вот, опять поиск первоэлемента... А как же комбинаторы или системы переписывания? Почему обязательно надо лямбда-исчисление во главу угла-то ставить? Еще Бэкус показал, что настоящее ФП — вообще не про лямбды %)
МБ
Оно связано только с математической логикой. К ней далеко-оо не все доходят. 😃
А можно ли вычисления достаточно строго описать иначе, чем логикой? Ну, точнее, исчислением секвентов?
BD
"Forth так же неисчерпаем, как и атом!" 😂
true true
AT
Ну вот, опять поиск первоэлемента... А как же комбинаторы или системы переписывания? Почему обязательно надо лямбда-исчисление во главу угла-то ставить? Еще Бэкус показал, что настоящее ФП — вообще не про лямбды %)
Комбинаторы в смысле Карри-Шрнфинкеля - это всего лишь специфические замкнутые лямбда-термы. 🤷♀️
МБ
Ну вот, опять поиск первоэлемента... А как же комбинаторы или системы переписывания? Почему обязательно надо лямбда-исчисление во главу угла-то ставить? Еще Бэкус показал, что настоящее ФП — вообще не про лямбды %)
Так доказано, что всё едино. Там нет ничего во главе угла, это просто разные аспекты одной и той же сущности.
PS
Комбинаторы в смысле Карри-Шрнфинкеля - это всего лишь специфические замкнутые лямбда-термы. 🤷♀️
Если одно можно выразить через другое, то это не закрывает вопрос, что же главнее. Особенно, если по историческому старшинству судить :)
AT
А можно ли вычисления достаточно строго описать иначе, чем логикой? Ну, точнее, исчислением секвентов?
Даже формально, по-моему, да. Но многих ли вообще интересует строгое формальное описание вычислений? Вопрос риторический. 😊
МБ
Комбинаторы в смысле Карри-Шрнфинкеля - это всего лишь специфические замкнутые лямбда-термы. 🤷♀️
А лямбда-термы - это всего лишь специальные последовательности комбинаторов :)
AT
А лямбда-термы - это всего лишь специальные последовательности комбинаторов :)
И это правильно! 😃
МБ
Если одно можно выразить через другое, то это не закрывает вопрос, что же главнее. Особенно, если по историческому старшинству судить :)
В истории я не силён :(