барендрегт, лямбда исчисление, вывод из аксиом, похожий на булевы алгебры

Следует напрямую из 5й строки определения, нет?

((s -> t) & (s' -> t)) <= ((s & s) -> (t & t)) и всё.

((s -> t) & (s' -> t)) <= ((s & s') -> (t & t)) исправил опечатку.

(1) тоже следует напрямую из определения, всё правильно написал: строки 3 и 4.

Спасибо, предложенное объяснение несколько прояснило для меня ситуацию. Я не осознал что там тривиальное s & s = s слева в правой части пятого правила.

Однако, всё равно не совсем ясно. У нас нет правила вроде

(s -> t) & (s' -> t') <= (s & s' -> t & t')

(s -> t) & (s -> t') <= (s & s -> t & t')

следовательно

(s' -> t) & (s' -> t) <= (s & s' -> t & t)

Кстати говоря, пока далеко не ушли, если есть минутка, глянь свежим взглядом пожалуйста, если не затруднит:

Страница 58, определение 4.2.1, пункт 1.

До «или» мы имеем, переводя на «словесный русский» с формул: s больше t если мы получаем t путём добавления к s квантора всеобщности. Другими словами, берём тип, добавляем квантор всеобщности по некоему альфа, и это получается меньше чем было.

После «или» мы имеем (опять же, говоря словами): «s больше t если мы получаем t путём удаления из s квантора всеобщности. Другими словами, берём тип (с квантором), убираем квантор по некоему альфа, и это получаеся меньше чем было.

Мне кажется или мы противоречим себе в двух частях одного пункта? Получается ведь: мы либо добавляем всеобщность, либо убираем и результат меньше чем был. Я смущаюсь что то. Наверное чего то не понимаю, но не вижу чего именно.

Нет, это я ошибся. Вроде так:

Пусть s & s' = I

I <= s
I <= s'

Тогда

s -> t <= I -> t 
s' -> t <= I -> t 
И, например
(s' -> t) & a <= s' -> t <= I -> t 

Где а = s -> t.

На страницу 58 посмотрю чуть позже.

Да, так всё сходится.

По поводу 58 страницы - я вроде понял, там действительно «противоречиво», но там так и должно быть. Смысл там в том что «тип после применения любого правила с квантором всеобщности тип становится меньше». Технический момент нужный в доказательстве которое идёт сразу после.

Спасибо! Я сам бы вряд ли так быстро разобрался.

да не, не вряд ли, а точно провтыкал бы ещё чёрт знает сколько и может и не добил бы... ))

Пожалуйста, обращайся. Не зря я, оказывается, этим 4 года занимался :D

Ну а вообще за такими вещами должна стоять какая-то мотивация, часто при достаточном понимании появляется «интуиция».

Не зря я, оказывается, этим 4 года занимался :D

прям вот этим? или, более обще, на математике учился? Я тоже в вузе учился в общем то, но филонил, троечник с нятяжкой. Поэтому, видимо, некоторые вроде как простые вещи иногда довольно трудно даются. Жалею, что не учился когда время было... так что, возвращаясь к вопросу - на мой взгляд точно не зря.

Ну а вообще за такими вещами должна стоять какая-то мотивация, часто при достаточном понимании появляется «интуиция».

Не знаю что это значит, но звучит убедительно)

Не знаю что это значит, но звучит убедительно)

Например, когда говоришь о мерах (кроме всякой экзотики), чаще проще думать о мере Лебега, длинне. А потом пытаться как-то доказать формально. В твоём случае я думал о <= как о включении множеств. -> хз что такое, если честно.

на математике

Да. В прошлом году закончил на магистра учиться.

Например, когда говоришь о мерах (кроме всякой экзотики), чаще проще думать о мере Лебега, длинне. А потом пытаться как-то доказать формально. В твоём случае я думал о <= как о включении множеств. -> хз что такое, если честно.

В целом, конечно. Но интуиция нарабатывается, кажется, чуть более обще. Это всё таки математика, и тут видно, что у тебя мат. интуиция как минимум кое-какая наработана. А вот у меня её совсем мало, я не сделал вывод например, что если в первую очередь два стрелочных типа сравниваются по правой компоненте, то _затем_-_то_ по левой (хотя казалось бы...). А я что то сижу и не пойму как сравнить, если правые одинаковы. Так же не сделал вывод что s = s & s (хоть он не нужен был, но показательно). Т.е. видно что часто не хватает элементарных навыков которые к теме вообще не относятся. Вроде всё понятно когда ты расписал, но вот сам так быстро не справился бы. Безотносительно того что такое стрелка. Понятно что через годик-два поднаторею, но жалко что приходится нагонять. Ну плюс конечно уже 10 лет как закончил и математики не касался за это время. Но мне кажется пробелы всё таки сказываются сильно.

Чем бы более-менее интересным ты не занялся в жизни (в технике или науке), математика - это, по моему, не зря. Всё понимать проще и быстрее когда есть мат. база: от тензоров и диффуров до всяких там передаточных функций, и от графов и матриц до лямбда-исчисления.

Согласен, я тоже считаю, что математика - лучший способ развития абстрактного мышления.

Обдумал это ещё раз :)

Мне кажется то что (s' -> t) & a <= s' -> t не вытекает из аксиом (хотя и кажется интуитивно логичным). Не мог бы ты пояснить, как ты получил это? Если есть минутка, конечно.

На первый взгляд, это 6 строка определения, рассматривая (s' -> t) как просто элемент из T.

Ничего себе, целый год прошёл!

Да, действительно.
Не зря у меня год назад вопросов не возникло)

спасибо!