Objective Caml - Понедельник, 25 марта 2013

Objective Caml

ocaml@conference.jabber.ru

Понедельник, 25 марта 2013< ^ >

Конфигурация комнаты

Участники комнаты

GMT+4
[00:09:08] Typhon вошёл(а) в комнату
[00:26:42] Typhon вышел(а) из комнаты
[00:33:32] f[x] вошёл(а) в комнату
[00:35:52] f[x] вышел(а) из комнаты
[01:13:26] Kakadu вышел(а) из комнаты
[01:15:18] ftrvxmtrx вышел(а) из комнаты
[01:27:00] Typhon вошёл(а) в комнату
[01:37:05] Sun][ вышел(а) из комнаты
[01:42:31] ftrvxmtrx вошёл(а) в комнату
[01:42:48] Typhon вышел(а) из комнаты
[01:45:02] komar вышел(а) из комнаты: Logged out
[01:45:05] komar вошёл(а) в комнату
[01:46:32] Sun][ вошёл(а) в комнату
[02:27:24] Typhon вошёл(а) в комнату
[02:39:58] strobegen вышел(а) из комнаты
[02:41:36] Sun][ вышел(а) из комнаты
[02:45:29] Typhon вышел(а) из комнаты
[03:28:06] Typhon вошёл(а) в комнату
[03:43:50] Typhon вышел(а) из комнаты
[07:52:35] strobegen вошёл(а) в комнату
[08:26:03] zinid вошёл(а) в комнату
[08:45:42] klapaucius вышел(а) из комнаты
[09:35:27] f[x] вошёл(а) в комнату
[09:35:32] f[x] вышел(а) из комнаты
[09:37:06] f[x] вошёл(а) в комнату
[10:09:49] ermine вошёл(а) в комнату
[10:46:40] komar вышел(а) из комнаты: Replaced by new connection
[10:46:40] komar вошёл(а) в комнату
[10:51:20] Kakadu вошёл(а) в комнату
[11:08:18] zinid вышел(а) из комнаты: Replaced by new connection
[11:08:19] zinid вошёл(а) в комнату
[11:08:35] zinid вышел(а) из комнаты
[11:08:41] zinid вошёл(а) в комнату
[11:10:52] f[x] вышел(а) из комнаты
[11:36:25] komar вышел(а) из комнаты: Logged out
[12:18:43] Typhon вошёл(а) в комнату
[12:22:06] Typhon вышел(а) из комнаты: Replaced by new connection
[12:22:16] Typhon вошёл(а) в комнату
[12:36:22] Sun][ вошёл(а) в комнату
[12:48:02] ftrvxmtrx вошёл(а) в комнату
[13:06:04] klapaucius вошёл(а) в комнату
[13:14:25] komar вошёл(а) в комнату
[13:21:10] klapaucius вошёл(а) в комнату
[13:21:30] klapaucius вышел(а) из комнаты
[14:04:32] Sun][ вышел(а) из комнаты
[14:18:40] f[x] вошёл(а) в комнату
[14:51:14] Sun][ вошёл(а) в комнату
[15:10:31] f[x] вышел(а) из комнаты
[15:44:43] Typhon вышел(а) из комнаты: Replaced by new connection
[15:44:53] Typhon вошёл(а) в комнату
[16:18:44] f[x] вошёл(а) в комнату
[17:41:56] zinid вышел(а) из комнаты
[17:48:51] <ermine> gds: в Coq elim - это исключение/упрощение или отбор по образцу? не смогла подобрать правильное понятие или соответствие кириллической математике
[17:50:29] <aleksey> исключать
[17:51:40] <ermine> всё равно не очень понятно
[17:55:15] <ermine> aleksey: а что такое исключать? например исключи по A /\ B в B /\ A
[18:06:51] <aleksey> ermine: исключать -- это избавиться от чего-то
[18:07:29] <aleksey> ermine: если у тебя, скажем, есть булевая переменная, то её можно исключив подставив вместо неё true и false, и доказав оба случая
[18:15:38] <ermine> aleksey: они не будевые, а Prop
[18:18:46] <aleksey> кто
[18:19:59] <ermine> aleksey: A B : Prop
[18:20:13] <ermine> но всё равно непонятно как и что
[18:20:23] <aleksey> значит ты их не исключишь
[18:20:28] <ermine> и почему получилось нечно
[18:20:55] <aleksey> ты, наверно, and исключить хочешь
[18:21:44] <ermine> не знаю
[18:22:07] <ermine> а что по-твоему получицо по команде elim?
[18:22:18] <ermine> см выше кого и где
[18:22:49] <ermine> изначально это доказательство коммутативности and
[18:23:38] <aleksey> у тебя будет гипотеза H : A /\ B, делаешь elim H, оно добавляет к цели A -> B ->
[18:24:08] <aleksey> потому что /\ вот так определён:
Inductive and (A B:Prop) : Prop :=
  conj : A -> B -> A /\ B
[18:25:59] <ermine> а кто исключается при этом?
[18:26:10] <aleksey> and
[18:26:35] <ermine> в гипотезе или цели?
[18:29:18] <ermine> вообще цель только обрастается этой импликацией
[18:29:35] <ermine> поэтому исключения не видно
[18:31:33] <aleksey> ну в гипотезах оно остаётся, но вообще тебе вместо A /\ B -> B /\ A теперь достаточно доказать A -> B -> B /\ A
[18:33:46] <ermine> aleksey: выглядит как unfold & substition back
[18:34:17] <ermine> хотя наверное это непривычно просто
[18:39:02] <gds> ermine: elim "ненужен".  Бери destruct для простых случаев и induction для доказательства по индукции.  Ещё годны case и case_eq, но редко, и, когда будет нужно, узнаешь о них.
[18:40:50] <ermine> та я уже интерпретировала elim в другом месте, по моему вышеописанному алгоритму
[18:41:09] <ermine> вместо деструкта, да, только оно влево идет
[18:43:59] <ermine> gds: неработает destruct
[18:44:08] <gds> ermine: покажи, что доказываешь.
[18:46:30] <ermine>   ADEpt работает, после деструкта еще сплит и ассумптионы, хе
[18:46:46] <ermine> ну сначала не догадалась что в аргумент деструкту вставить
[18:47:11] <ADEpt> huh?
[18:47:29] <aleksey> gds: elim короче чем destruct :)
[18:47:53] <aleksey> ermine: destruct H
[18:48:08] <gds> aleksey: Ltac d n := destruct n.  Где твой elim теперь?
[18:48:21] <ermine> aleksey: его, да
[18:48:32] <aleksey> так это ещё Ltac писать
[18:48:35] <ermine> но он до конца ж не доведет
[18:48:43] Sun][ вышел(а) из комнаты
[18:49:01] <ermine> а сплит может тоже некошерен?
[18:49:06] <gds> любая более-менее сложная разработка требует Ltac.
[18:49:12] <ermine> еще скажете что ауто короче будет
[18:49:58] <ermine> ADEpt: а ты давно осилил coq?
[18:51:01] <gds> ermine: "split" некошерен, да.  "constructor" всяко лучше будет -- более универсальный.  А то и "apply Названиеконструктора", что ещё лучше.
[18:51:19] <gds> (хотя для слишком простых случаев, типа and, split удобен.)
[18:51:28] <ADEpt> ermine: я не пробовал осилить coq
[18:51:29] <aleksey> опять же split короче :)
[18:51:45] <gds> aleksey: Ltac c ...  нутыпонел :]
[18:52:11] <aleksey> и надо все теоремы именовать a, b ..., z, a1, ... :)
[18:52:19] <gds> но да, когда один конструктор, split хорош.
[18:52:38] <aleksey> ADEpt: попробуй!
[18:52:50] <f[x]> що воны зробылы з мойим чятигом!
[18:53:26] <aleksey> кстати скоро gcj
[18:53:38] <gds> f[x]: вот-вот.  Может стоит переорганизоваться в другую жаббер-конфу?  (если через день-два не пройдёт.)
[18:53:39] <f[x]> aleksey: а cppgm ты не?
[18:53:50] <f[x]> gds: думаю пока не стоит
[18:54:01] <f[x]> и вообще не стоит наверное :)
[18:54:06] <aleksey> wtf cppgm
[18:54:18] <f[x]> http://cppgm.org/
[18:54:22] <gds> f[x]: ну смотри, не хочу никого напрягать.  Тем более, подобные дискуссии затухают быстро, как показала практика.
[18:54:29] <f[x]> aleksey: это такой вид мазохизма
[18:54:30] <ermine> ADEpt: твой код несертифицированный!!!
[18:54:40] <f[x]> gds: не напрягает
[18:54:49] <f[x]> я ведь и сам чуть-чуть того
[18:54:56] <f[x]> был на коке
[18:55:14] <gds> "горы кокоса, решал вопросы"?
[18:55:35] <aleksey> f[x]: судя по названию, я там точно не в тему :)
[18:56:15] <f[x]> gds: такие доказательства прокручивал!
[18:56:54] <gds> f[x]: небось, без всяких подсказок тупой железяки, а сразу в уме?
[18:58:20] <f[x]> gds: никак вы меня в чём-то подозреваете?
[18:59:12] <gds> f[x]: да нет же, кока это вполне хорошо, если в разумных количествах.
[18:59:31] <ermine> так, еду дальше в туториале
[19:04:20] <ermine> вообще игры в coq - весьма занудная штука - разложить, сложить, применить хинты, помнить про десятое и двадцатое и при этом полагаться не на свой ум, а на ум coq
[19:27:10] komar вышел(а) из комнаты: Logged out
[19:54:57] ftrvxmtrx вышел(а) из комнаты
[20:12:42] f[x] вышел(а) из комнаты
[20:23:09] tilarids вошёл(а) в комнату
[20:47:52] Kakadu вышел(а) из комнаты
[21:11:00] komar вошёл(а) в комнату
[21:14:55] komar вышел(а) из комнаты: Logged out
[21:15:21] tilarids вышел(а) из комнаты
[21:42:25] Kakadu вошёл(а) в комнату
[22:08:18] Typhon вышел(а) из комнаты
[22:12:49] komar вошёл(а) в комнату
[22:16:42] <ermine> Verified TLS in F#, using the refinement types work from MSR Cambridge;
http://mitls.rocq.inria.fr
tech report: http://mitls.rocq.inria.fr/downloads/miTLS-report.pdf
[22:17:42] <ermine> There are a number of caveats regarding performance (e.g. byte arrays are represented as functional strings, so performance involves huge amounts of copying), but the core work is extremely nice and you can see how to make it faster...
[22:19:57] <ermine> странно на страничке ни слова про coq
[22:22:37] komar вышел(а) из комнаты: Logged out
[22:22:40] komar вошёл(а) в комнату
[22:25:58] UncleVasya вошёл(а) в комнату
[22:53:51] ermine вышел(а) из комнаты
[23:02:09] Sun][ вошёл(а) в комнату
[23:45:14] UncleVasya вышел(а) из комнаты