deniok: (Default)
Написал
<img src="http://www.codecogs.com/eq.latex? A:*,P:A\rightarrow *\ \vdash\ (\lambda a:A\ \lambda x:Pa\,.\,x):(\Pi a:A\,.\,(Pa\rightarrow Pa)):*">
получил


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

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

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

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

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

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

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


UPD. По совету друзей приобрел автомобиль "Москвич" подкорректировал перевод. Фактически у [livejournal.com profile] avva не очень ясно указано лишь, что статистика 100/900 неизвестна островитянам. Ну и подсказка "каждый знает, что каждый знает, ..." про общее знание опущена ;) Англоязычный оригинал.
deniok: (Default)
Из блога Вадлера: http://wadler.blogspot.com/2007/05/oh-no-alligators.html

One of my great joys on visiting Berkeley was to meet Bret Victor, of Magic Ink fame. I mentioned to him that I had been working with a student on a visual lambda calculus, in part because I wanted a way to explain lambda calculus to my eight-year old daughter and son. He responded with a game involving alligators and their eggs, such a clever morphing of lambda calculus that it wasn't until I reached the end that I realized exactly what was going on.

So far, I've had a chance to show it to my daughter, who managed to successfully solve the problem at the end. She guessed a definition of 'not', and then applied 'not' to 'true' and checked that the result is 'false'. But she was most interested in drawing pictures of alligators! I expect it would be more fun to use if there was software that implemented the game.

Ну и имплементация: http://worrydream.com/AlligatorEggs/

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:53 pm
Powered by Dreamwidth Studios