Category: наука

Vash

Тов. Лавсан опять в ударе

Третья Теорема Лавсана (о бесполезности статической типизации)
Статическая типизация не добавляет ничего действительно полезного и только лишь отбирает время.
via LOR

Первый Принцип Пиздежа: выдавай гипотезу за теорему.

Тов. Лавсан опять затрудняется прочесть хотя бы базовую литературу по теме, в которой пытается выступать в роли эксперта. Типы нужны для того, чтобы доказать отсутствие определённых типов нежелательного поведения, что явно не похоже на "ничего". Механизм отбора времени у трудящихся не описан.
Vash

Ассоциативность

Думаю, вы уже слышали про "два подхода" к ассоциативности из математики и программирования. Недавно пришлось решать одну задачу, и стало ясно, что подход на самом деле один.

"Неассоциативность" (пр-е)
a :- b :- c писать нельзя, потому что по умолчанию это не a :- (b :- c) и не (a :- b) :- c

"Левоассоциативность" (пр-е)
a - b - c = (a - b) - c

"Правоассоциативность" (пр-е)
a : b : c = a : (b : c)

"Ассоциативность" (математика)
Это левоассоциативность и правоассоциативность одновременно.
a + b + c = (a + b) + c
a + b + c = a + (b + c)
=>
(a + b) + c = a + (b + c)

Таким образом, ассоциативность как свойство это пара из двух булевых констант.

Как это можно использовать? Для печати AST выражений, например. Есть проблема: в выражении не один оператор. Нам понадобятся ещё и приоритеты. Обозначим свойства оператора op:
1) priority(op) : Integer
2) left_assoc(op) : Bool 
3) right_assoc(op) : Bool.

Приоритет и ассоциативность образуют вместе что-то вроде лексикографического порядка, где приоритет идёт "раньше в слове".
В левой(правой) позиции от наружного оператора мы можем записать внутренний оператор без скобок, если либо у внутреннего оператора приоритет больше, либо если приоритеты равны, и оба оператора лево(право)ассоциативны.

Пусть P[|...|] это функция печати AST. Из вышесказанного следует, что её нужно реализовать так.
test(assoc, op1, op2) = priority(op2) > priority(op1) || priority(op2) == priority(op1) && assoc(op1) && assoc(op2)
op1( P[| op2(a, b) |], c ) =
        a op2 b op1 c, если test(left_assoc, op1, op2)
        (a op2 b) op1 c, иначе
op1( a, P[| op2(b, c) |] ) =
        a op1 b op2 c, если test(right_assoc, op1, op2)
        a op1 (b op2 c), иначе
Под нотацией "op1( P[| ... |], c )" подразумевалось, что нам известен контекст, в котором происходит печать, т.е. какой оператор стоит снаружи. В настоящем коде его нужно передать явно.

Приложение.
Из знакомства с теорией типов или логикой или чем-там-ещё многие знают, что a -> b это ba и подчиняется тем же законам.
Также известно, что (->) это (по хорошему, если мы хотим "каррирование" (независимо от его смысла в данной теории)) правоассоциативная операция. a -> (b -> c) = (cb)a = cba
Из этого можно сделать вывод: чтобы возведение в степень вело себя "правильно", следует задавать его левоассоциативным, а не как в Python.
Vash

Открытое исследование нейромедиатора Орексин-А

Оригинал взят у yantayga в Открыте исследование нейромедиатора Орексин-А
Оригинал взят у walter_simons в Открыте исследование нейромедиатора Орексин-А
В прошлом посте я описал формулу Орексина А - нейромедиатора, позволяющего человеку переносить длительное отсутствие сна без мучительной борьбы, собственно с засыпанием.



Весь сыр-бор с ним начался после запрета Модафинила, препарата для лечения нарколепсии, основным действием которого было увеличение/поддержание концентрации Орексина А в головном мозге.

Итак, нам ничего не мешает его сделать и попробовать. Есть куча биохимических фирм и фирмочек, за некоторую сумму (не маленькую) готовые синтезировать данный нейропептид. Я навел справки, и узнал порядок цен в России: 5мг искомого вещества (с чистотой 80%) обойдутся ~ 73 000 руб (синтез пептида 26697руб+ объединение спирали в два дисульфидных мостика - 46220руб)
Срок исполнения заказа - 4-6 недель. В качестве контроля качества предоставляют данные HPLC анализа и Масс-спектрометрии. Полученный неропептид предназначен только для научных исследований и не подлежит сертификации или получению регистрационных удостоверений. Таким образом он не подпадает под законодательство фармацевтического оборота.

Остается понять, 5 мг - это много или мало для нас? На первый взгляд очень мало. Но если покопаться в научных работах:

Two methods of administration of orexin-A were tested, intravenous injections (2.5–10.0 μg/kg, i.v.) and a novel method developed for nasal delivery via an atomizer spray mist to the nostrils (dose estimated 1.0 μg/kg). Results showed that orexin-A delivered via the intravenous and nasal routes significantly improved performance in sleep-deprived monkeys; however, the nasal delivery method was significantly more effective than the highest dose (10 μg/kg) of intravenous orexin-A tested.

Суть вкратце: Обезьянок, лишенных сна 36 часов, тестировали на обучаемость и память. Было протестировано два метода введения внутривенный (по 2,5 - 10 мкг на кг массы тела) и интраназальный (орошение слизистой носа спреем, содержащим Орексин А) с концентрацией из расчета 1 мкг на кг массы тела. Оказалось, последний способ гораздо эффективнее, несмотря на вдесятеро меньшую концентрацию нейромедиатора!

1 микрограмм (мкг) равен 1/1.000 части миллиграмма. Таким образом, 5 мг синтезированного пептида, действующих доз будет почти на 5 тонн живого веса :) или ~ 80 человек.
Таким образом, цена нашего эксперимента по 1000 рублей на человека. Да и 80 человек уже неплохая статистика для начала!

Итак, 2 июня 2012 года, объявляю старт "Открытого исследования нейромедиатора Орексин-А"

Время проекта: 2.06.2012-2.10.2012

Цель - убедиться в управлении Орексина А на способность человека не спать.

Задачи: Собрать тестовую группу, собрать сумму, необходимую для оплаты синтеза нейропептида, создания раствора и расфасовки в спрей пульверизаторы, раздать дозы тестовой группе, собрать отчеты, обобщить результаты.

Для выполнения задач требуются
Не менее 80 волонтеров-донаторов. Каждый волонтер вносит 1 тыс рублей на публичный счет проекта.
Когда набирается нужная сумма, средства переводятся на счет биохимической лаборатории (выберем голосованием какую) для синтеза Орексин А, растворения и расфасовки.
Участники получают свою порцию для испытаний (на адрес, указанный при переводе). По результатам пишут отчет.

Если до конца срока проекта сумму набрать не удастся, проведем открытое обсуждение и голосование, какому проекту помочь

Готовы? - Подключайтесь!

Вот публичный кошелек:
Донаторствовать можно через него или вот этот виджет:

Ники волонтеров-донаторов будут опубликованы отдельным списком в апдейтах к этому посту.

Списки участников на 4.06.2012

1) walter_simons
2) nor_man_volk
3) yantayga
4) sontar
5) dposli
6) hawara
7) lyrialtus


Vash

(no subject)

В ответ на это: http://juick.com/jtootf/1812621

Agda это то, что я искал долгие годы. В ней нет синтетических конструкций вроде мультипараметрических классов типов с функциональными зависимостями и подобной высосанной из пальца фигни, которой пытаются покрыть Тьюринг-полный метаязык. Зависимые типы это совсем не типы даже, это способ производить метавычисления произвольной сложности и глубины. Ну и при наличии чекера завершимости ещё и способ доказать корректность программы или какую-нибудь другую теорему. На ближайшие несколько лет у меня есть задача по созданию чего-то зависимо типизированного, тотального, но эффективного и не такого страшного синтаксически как какой-нибудь ATS.

Жуйк, увы, гребёт.
Registration is temporary disabled. Please, come back later.
Vash

Квантовые вычисления vs криптография

Есть такая логическая цепочка, которую неплохо бы знать каждому. Наверняка вы уже не раз слышали в желтой прессе о том, что квантовые компьютеры придут и разрушат все схемы шифрования. Иногда там даже приводилось вполне логичное описание того, как система принимает множество состояний одновременно, и как с помощью этого проводится экспоненциально много вычислений. Но есть такая вещь, как принцип Ландауэра, гласящий, что в любой вычислительной системе, независимо от ее физической реализации, при потере 1 бита информации выделяется теплота. Квантовый брутфорс должен будет вычислять значения некой функции и сравнивать с образцом. Если это хеш-функции, очевидно, что они теряют информацию. Для прочих алгоритмов шифрования это не столь очевидно, но они теряют биты тоже (здесь, как я понимаю, играет роль обратимость процесса). Отличный от брутфорса метод позволит производить эти вычисления и на обычном компьютере. Квантовые компьютеры, быть может, и позволяют производить экспоненциально много вычислений за промежуток времени, но они будут и потреблять соответствующее количество энергии, и требовать отвод такого количества тепла.