*CS

gds 26.03.2013 22:32

"thunk" / "deferred computation" — "личинка вычисления".
Соответственно, при использовании лентяйки программа откладывает в память личинки вычислений.
//
"use" — "использование". "abuse" — "извредствование"?

gds 20.03.2013 17:25

Зарелизил мелкую библиотечку для отладки редукций выражений в пределах coq: https://bitbucket.org/gds/coq-breakpoint...

coq, cs, fp
gds 19.03.2013 11:14

Посоны, помогите с задачкой. Я совсем разучился в графы. Наговнокодить могу, но должно быть красивое решение (скорее всего, ещё и более быстрое, чем наивный говнокод).
Есть направленный ациклический граф: https://docs.google.com/drawings/d/1OPIv...
Задана ... more →

cs, it, math
gds 18.03.2013 11:44

Наша редакция рада ответить на просьбу господина @ulidtko, изложенную в http://amd63.psto.net/tsfgse#123 , нижеследующим куском кода: https://gist.github.com/gdsfh/7140f41aca...
Там в каментах я показал, во что экстрактится всё это безобразие. Как обычно, все пруф-термы стёрты, остались только ... more →

coq, cs, fp, it, ocaml
gds 28.02.2013 11:09

Пост про различие "proof of negation" vs "proof by contradiction", в том числе есть интересное про отличие классической от интуиционистской (конструктивной) логики (однако, если последнее вам известно, в том числе на практике, то читать будет не очень интересно, разве что для структуризации знаний): ... more →

math, cs
gds 11.02.2013 18:03

"построение термов тактиками в coq — безопасно" [ http://gds.livejournal.com/66182.html ]

coq, cs, it
gds 26.01.2013 09:51

"Можно [...] самим попытаться двинуть науку в бок, потому что вперед не можем, а назад не разрешают :-)" [lj\maxim]

cs
gds 15.01.2013 14:39

"
There are only two hard things in Computer Science: naming things, cache invalidation and off-by-one errors.
"
[lj\wizzard0]

Marisa 12.01.2013 23:43

>В любом случае, если вы хотите узнать о теории типов, купите книгу "Типы и Языки Программирования" от Бенджамина Ф. Пирса. Если вы всё ещё запутались, вы можете развеять все трудности с помощью "Продвинутых Вопросов в Типах и Языках Программирования" от Бенджамина Ф. Пирса. Предположительно, Профессор Пирс сейчас ... more →

gds 07.01.2013 18:54

"
This reminds me of a funny event at the Haskell workshop 2006. One participant stood up and sincerely proposed that Haskell' standard would find a way to automatically derive a monadic version of a pure expression. Chung-chieh Shan recommended that person to take a look at OCaml...
"
(уже второй раз лезу за этой ... more →

4da 24.12.2012 19:46

Вы тупое, убогое, безграмотное ничтожество.

Повторяю, свинья, проблема P=NP не имеет ни малейшего отношения к нечеткой логике. Это во первых. Во вторых, нечеткая логика имеет самое непосредственное отношение к математике.

Ну да у вас же IQ явно меньше 50, смысла вам что либо объяснять нет. Вы всего лишь убогая ... more →

gds 20.12.2012 17:25

При создании рекурсивных структур данных часто используется приём, известный как "tying the кот".

4da 19.11.2012 00:15

Normalized Device Coordinates → Нормализованное пространство приборных координат
Ничотак перевод, да?

shit, cs
hedgehog 12.11.2012 08:45

посоны где скачать контру 1.6?

gds 05.11.2012 19:17

Опыт использования Coq на практике, или Как я сам себя отпетушил COQОКОКОКО < http://gds.livejournal.com/65879.html >

XonX 30.09.2012 19:52

Кто тут в кемперстрайк играет? Реквестирую советов по поводу того, как не быть дном

gds 08.09.2012 14:34

Постил в камлочятик, но запощу и тут.
Есть вероятность, что Олег будет давать интервью. Можно повлиять на вопросы. Присылайте мне, я передам куданадо.
Вопрос про то, не жмёт ли ему череп, я задать хотел бы, но это некультурно. Вопрос про будущее метаокамла уже скинул. Вопрос про субъективное сравнение языков с ... more →

gds 05.09.2012 18:47

"гулял в компании зависимых типов"

gds 06.07.2012 15:08

#coq:
ianjneu: Javascript and Python have nonsense-ical scope. A colleague says, "they don't have lexical scope. They have kaleidoscope."

gds 29.05.2012 19:28

К нам сегодня заходил
Лиспомакроскобкофил,
Он межушным поролоном
Типизацию хулил.

gds 23.05.2012 12:29

Офигенная штука: http://logitext.ezyang.scripts.mit.edu/l... — интерактивная обучалка sequent calculus, и, в том числе, "Невыносимо-Непонятного Контекста Γ".

cs