?

Log in

Из-Под Глыб

Apr. 30th, 2016

09:28 am - taking out the christmas tree in July

"How do you get rid of your dead grass? We have a dead grass in our front lawn which my husband has been wanting to get rid of. His parents wants to keep it on, but my husband is adamant to get rid of it. He's sick of seeing it and he does not want anything to do with it. I told him him he has my vote to get rid of it. He's been thinking of getting rid of it since last year. I do think it's about time we get rid if it once and for all. Any suggestions???"

That's what my neighbors write.

Apr. 29th, 2016

09:35 am - coq

Took me some time to prove

Theorem distr_rev : forall l1 l2 : natlist,
  rev (l1 ++ l2) = (rev l2) ++ (rev l1).


But I did.

Tags:

Apr. 28th, 2016

05:54 pm - а вы слыхали, кстати?

слово "Испания" происходит из баскского, где оно означало "Украина".

("скск" отдельно доставляет)

Apr. 27th, 2016

10:26 pm - FOL

Когда преподаешь логику первого порядка, то тебе там в учебнике написано, что truth tables применить не всегда представляется возможным, потому что не все комбинации значений предикатов допустимы по жизни. Ну в смысле, p1(x)=x>1 и p2(x)=x>2, то все комбинации не перебрать.

Ага. Потому что у нас вообще-то универсум - не прямоугольник. В смысле, не декартово произведение компонент. А что-нибудь похитрее. С зависимостями. Так что вообще-то описывается или категорией, или топологией Гротендика (пофиг, что так, что так). А декартово произведение состояний получается, если мы имеем дискретную категорию. Поэтому в FOL старательно скрывают вложение дискретной в категорию общего вида, и делают такое лицо, будто у нас тут сплошь булева логика. Причем, не двузначная, потому что же если есть несколько propositions, даже если каждое имеет два значения, то комбинаций-то уже 2^n, можно же это признать.

Ну и вот. Как люди умеют скрывать произвольную интуиционистскую логику за рассуждением о компонентах, это рехнуться можно. Ведь все ж тривиально же ж.

Я потом подробности напишу, но принцип-то понятен, так? И даже тривиален. Ну берем любую теорию, берем модельный топос... 21-й век же ж.

07:15 am - кто-нибудь знает?


How often can you dance Kizomba per week in St Petersburg, Russia?

Tags:

Apr. 26th, 2016

05:37 pm - rssh показывает пятимерный лямбда-куб

Java/Scala Lab_Руслан Шевченко_Несколько трюков scala-разработки

Apr. 25th, 2016

10:19 pm - one stupid question

Which restrooms in South Carolina are now gays discriminated from?

I'm confused.

Tags:

03:54 am - про Освальда

Большой пост - http://samsebeskazal.livejournal.com/368662.html

Apr. 24th, 2016

07:39 pm - Данечка на Лукоморье

06:05 pm - важный момент

Когда, скажем, сокращают в Айбиэм, то пакет дают - зарплата на полгода. А в иной конторе - три дня зарплаты. Или вообще ноль.

Так вот, лучше заранее знать. Чтоб не питать иллюзий, если что. Поэтому важно разговаривать с сокращенными, как там severance package.

Navigate: (Previous 10 Entries)