deniok: (typed lambda)
В импликационном фрагменте классической пропозициональной логики у нас нет никаких связок кроме импликационной стрелочки. Поэтому мы не можем записать закон двойного отрицания или закон исключённого третьего - у нас для этого нет соответствующей связки. Однако имеется закон Пирса ((α → β) → α) → α, который в классической логике полностью эквивалентен упомянутым законам.

В просто типизированной лямбде тип ((α → β) → α) → α необитаем, поскольку соответствие Карри-Говарда задаёт изоморфизм с интуиционистской логикой, которая отличается от классической как раз отсутствием всех этих законов. Однако имеется слабый закон Пирса ((((α → β) → α) → α) → β) → β, про который известно, что он верен интуиционистски, а значит может быть получен конструктивно.

Откуда возникает задача: написать в просто типизированном лямбда-исчислении замкнутый терм типа ((((α → β) → α) → α) → β) → β.

Комменты не скринятся; Coq-читерам предлагается забыть про тактику auto и вспомнить про intros, apply и exact :)
deniok: (Default)
Вынесу-ка коммент как пост.

Во френдленте потихоньку обсуждается классическая задача про 12 монеток с одной фальшивой среди них, которую нужно найти за 3 взвешивания (и определить тяжелее она или легче настоящих). И ее обобщение на случай m монеток и n взвешиваний.
deniok: (typed lambda)
Придумал задачку по лямбда исчислению.

Общеизвестен лямбда-терм, не имеющий нормальной формы
(\x.xx)(\x.xx)
Этот терм обладает следующим свойством: он воспроизводит сам себя при каждой бета-редукции, ведя себя по отношению к ней как экспонента по отношению к дифференцированию.

А теперь задача: написать не имеющий нормальной формы терм, который бы вел себя как e^(-x). То есть при первой бета-редукции он должен превращаться во что-то другое, а при следующей возвращаться к исходному виду. Моя версия такого терма (flipflop) под катом белым цветом
Ответ тут, белым цветом... )
Может кто придумает попроще?

UPD: Эх, а у меня-то решение неправильное :) (Потому что у меня аж шесть шагов) Правильное - у [livejournal.com profile] lomeo в комментах.
deniok: (умничаю)
Пара задачек по лямбда-исчислению.

(1) Сконструируйте лямбда-терм F, такой что для любого терма M выполнялось бы
FM = MF


(2) Сконструируйте лямбда-терм G, такой что для любых термов M и N выполнялось бы
GMN = NG(NMG)


Ответы не скринятся, так что если хотите думать сами - не смотрите в комменты.
deniok: (ухмыляюсь)
Прекрасная логическая задачка с подробным обсуждением у [livejournal.com profile] avva. Формулировка там чуть-чуть неясная (допустимы формальные придирки), ниже, в комментах, [livejournal.com profile] vik_rud  дал более точный перевод (который я слегка причесал):

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

Из 1000 островитян 100 имеют голубые глаза, а остальные 900 имеют карие глаза, хотя островитяне первоначально не обладают этими статистическими данными (каждый из них может видеть только 999 из 1000 жителей).

Однажды голубоглазый иностранец посещает остров и завоевывает полное доверие племени.

Как-то вечером, он обращается ко всему племени, и благодарит их за гостеприимство.

Однако, не зная местных обычаев, иностранец делает ошибку, упоминая цвет глаз в своем обращении: "Как необычно видеть другого голубоглазого человека, такого как я, в этой части света".

Какое воздействие эта бестактность окажет на племя?


UPD. По совету друзей приобрел автомобиль "Москвич" подкорректировал перевод. Фактически у [livejournal.com profile] avva не очень ясно указано лишь, что статистика 100/900 неизвестна островитянам. Ну и подсказка "каждый знает, что каждый знает, ..." про общее знание опущена ;) Англоязычный оригинал.

Profile

deniok: (Default)
deniok

April 2017

S M T W T F S
      1
23 45678
9101112131415
16171819202122
23242526272829
30      

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 25th, 2017 02:52 pm
Powered by Dreamwidth Studios