sea

Домашка по Топологии на ПНД

Lemma. Consider commutative triangle:

    { f = g . p,
      f: X -> Z,
      p: X -> Y,
      g: Y -> Z } where p: Quotient, g: Surjective.

Then f: Continuous <=> g: Continuous.


Record quot_class_of (T Q : Type) := QuotClass {
       repr : Q -> T;
       pi : T -> Q;
       reprK : forall x : Q, pi (repr x) = x }.

Record quotType (T : Type) := QuotType {
       quot_sort :> Type;
       quot_class : quot_class_of T quot_sort }

Record type_quotient (T : Type)
                     (equiv : T -> T -> Prop)
                     (Hequiv : equivalence equiv) := {
       quo :> Type;
       class :> T -> quo;
       quo_comp : forall (x y : T), equiv x y -> class x = class y;
       quo_comp_rev : forall (x y : T), class x = class y -> equiv x y;
       quo_lift : forall (R : Type) (f : T -> R), compatible equiv f -> quo -> R;
       quo_lift_prop : forall (R : Type) (f : T -> R) (Hf : compatible equiv f),
                       forall (x : T), (quot_lift Hf \o class) x = f x;
       quo_surj : forall (c : quo), exists x : T, c = class x
}.


____________
[1]. http://ai2-s2-pdfs.s3.amazonaws.com/1704/7a639180e384cea1f183cf9082e7e13f021a.pdf
sea

Домашка по Алкотрейдингу на KVS

> book:print().
  Id Price.10e8   Size.10e8
---- ------------ -----------
 166 118274000000 -744526365
 165 117076000000 -6443000000
 163 116609000000 -3287000000
  21 116435000000 -876000000
 161 115617000000 -279199700
 167 115545000000 -468957492
  27 115332000000 -25000000
  28 115331000000 -3000000
  62 115284000000 -301020000
 109 115283000000 -28000000
  66 115254000000 1000000
  64 115253000000 29800000
 149 114950000000 99000000
 133 114936000000 98000000
 130 114928000000 99000000
 127 114920000000 97000000
 126 114914000000 92000000
 124 114903000000 103000000
 123 114891000000 98000000
 122 114884000000 108000000
   1 114871000000 1700000000
 121 114865000000 100000000
 104 114854000000 265779000
  33 114792000000 25000000
 164 114791000000 449969320
  53 114774000000 316000000
  70 114753000000 195000000
 119    001000000 8973000000
Depth: 28
Total: 393844763
ok
sea

Новое увлечение

По мотивам sorhed блога https://telegram.me/alkotrading я решил написать Ticker Plant для основных бирж упомянутых в блоге. Они даются в виде домашнего задания, так что те, кто любят всякие тестовые задания, могут прямо сейчас взять и начать строить себе ордер буки, и писать себе своих карманных роботов :-) Стратегии все там описаны. Думаю за выходные написать построение ордер буков, рекордер стримов, ретрайвал хисторикал дейта и потом займусь вылизыванием команд консоли и кверей. А сейчас пока подключил только WebSocket стримы, конвертнул JSON в BERT и заюзал такие либы:

    {active, ".*", {git, "git://github.com/synrc/active",  {tag,"1.9"}}},
    {jsone,  ".*", {git, "git://github.com/sile/jsone",    {tag,"v0.3.3"}}},
    {rest, ".*", {git, "git://github.com/synrc/rest",      {tag,"2.9"}}},
    {websocket_client, ".*", {git, "git://github.com/jeremyong/websocket_client",  {tag,"v0.7"}}},
    {kvs,    ".*", {git, "git://github.com/synrc/kvs",     {tag,"3.9"}}}


HFT в Биткоинах не нужен, поэтому любой ваш PHP подойдет. Coq тоже подойдет :-)
Буду стараться писать регулярные отчеты по Алкотрейдингу! Бухайте и Торгуйте с нами!

https://github.com/spawnproc/ticker
sea

Рантайм библиотека на Coq

Одно из заданий диссертации, построение рантайм библиотеки компактнее всего можно сформулировать вот так:

CoREPL> spawn ack 4 1
20
CoREPL> spawn ack 4 1 
21
CoREPL> ls
[(20,ack,10043),(21,ack,10033)]
20:65533
21:65533
CoREPL> kill 20
Ok
CoREPL> send 20 "hello"
Error
CoREPL>


Вот такое написать — уже неплохая цель, думаю даже больше будет чем любые другие а ля VM на Coq. Странно конечно звучит писать обычные программы, а в полях держать поля username и password в теоремах, но почему нет?

В такое я думаю трансформировать со временем https://github.com/5HT/co
Кто там хотел в Групоид Инфинити, приходите писать на Coq будет весело https://gitter.im/groupoid/exe
Денег нет, популярности нет, чистейшее R&D под ваши нужды, предлагайте свои идеи, будем в эту сторону двигать! Область наших интересов в этом проекте: стрим процессинг, векторизация, стрим фьюжин (т.е. с вероятностью > 1/2 то же, чем вы занимаетесь у себя на производстве) компиляция в LLVM языки — точка соприкосновения с http://groupoid.space/hnc. Этот проект назовем в будущем условно co — такого двухбуквенного сочетания в домене проектов нашей вселенной Marvell еще не было — REPL интерпретатор и рантайм система для программирования на Coq.
sea

Языки и Программирование: Coq

Почему Coq не был офигенным еще 5 лет назад? Потому что никто не преуспел на его основе сделать язык общего назначения. Поискав "coq as general purpose language" вы пока ничего не найдете. На Coq дофига пакетов в OCaml, но большинство из них математические модели.
Но не на количество моделей надо смотреть, а можно ли на нем писать действительно что-то мощное, ну ладно мощное, хотябы хелоу ворлд и ехо сервер :-) 3 года назад Гиюм Кларе сделал веб-сервер Pluto, и если вы посмотрите на исходники, то найдете стиль poor man человека, с простенькими эфектами, простенькой функциональностью — но все работает. Я хотел прорекламировать сайт автора, но он почему-то лежит, поэтому я просто тут расскажу на пальцах.

Как только появится возможно писать нормальные хелоу ворлды и кто-то возьмется за базовую рантайм библиотеку, которая по производительности была бы хотя бы на уровне PHP, тогда можно выходить в продакшин местячково начинать, ну как мы с n2o. Но кто будет писать на зависимых типах n2o.coq спросите вы? Ну Haskell тоже все боялись, а сейчас каждый джаваскриптер видел уже PureScript и Elm и может на них писать. Так, что мое мнение такое, как только найдется чувак который сделает приятную писанину на Coq сразу появится говнокод и продакшин. Тем более, что для рантайм библиотеки хватит и System F. Я вижу, что Coq мне приятней чем Scala/Haskell, и что его можно окультурить, есть Notation, можно даже DSL строить прямо в языке.

Кстати про OCaml, он тоже довольно омолодился за последние 5 лет. Во-первых opam, во вторых более нормальный сайт, Multi-core OCaml, самый быстрый паттерн мачинг, ReasonML тоже. Кароче куча всего, Lwt по сути уже стандарт де факто, успех Джейн Стрит и т.д. Неспешный но прекрасный язык для командной разработки. В ЖЖ дофига чуваков пишут/писали на OCaml.

Я к чему веду, так как мы с вами 10 лет назад интересовались лямбдой, 5 лет назад зависимыми типами, так и сейчас это кто-то делает, и этого будет больше. Конечно сама теория зависимых типов создает некую элитарность, но успех таких чистых и приятных штук как PureScript говорит, что даже сложные вещи можно сделать простыми, для меня лично PureScript — это реинкарнация Miranda, т.е. System F язык каким он должен быть. Такой же реинкарнацией Coq является Lean, а позже и EXE. Но Coq in Coq круче будет чем EXE in Rust, к примеру.

Я думаю, что нужно продолжать дело coq.io, и искать новые рабочие формы в библиотеке рантайм типов (а не PhD хелоу ворлды, которые если чесно уже заебали, буду стараться сделать не очередной хелоу ворлд!). Эту библиотеку, как я ее видел для EXE, можно написать на Coq и попробовать на простеньких догфуд программах, ну а что мы пишем, WebSocket, бинарный стриминг и очередя. Так, что вцелом, мы в Coq вас не тащим, но сами стараемся туда попасть раньше чем вы.
sea

Actario: A Framework for Reasoning About Actor Systems

Shohei Yasutake, Takuo Watanabe

Coq:
CoFixpoint behvA := receive (fun msg ⇒
match msg with
| name_msg sender ⇒ me ← self; sender ! name_msg me; become behvA
|_⇒ child ← new behvB; child ! msg; become behvA
end)

Erlang:
behvA() → receive Msg → case Msg of
{name_msg, Sender} → Me = self(), Sender ! {name_msg, Me}, behvA()
     _ → Child = spawn(fun() → behvB() end), Child ! Msg behvA()
end.

_______________
[1] http://amutake.github.io/actario/AGERE2015.pdf
sea

CoFixpoint Extraction REPL Prototype Zero

Ну что, я таки нанписал CoFixpoint корекурсию на коке. Точнее сразу REPL для коиндуктивного типа. No OCaml was involved.
$ brew install opam
$ opam install coq
$ opam install coq-io-system

Быстрый старт предполагает наличие всех необходимых opam модулей, которые в предыдущих постах я рассказал как насетапить, а если и не рассказал, то показал какие из них необходимые.
$ git clone git://github.com/5HT/co && cd co
$ make && cd extraction && make && ./main.native
ocamlbuild main.native -use-ocamlfind -package io-system
Finished, 5 targets (5 cached) in 00:00:00.
1
Input: 1.
2
Input: 2.
3
Input: 3.
CTRL-D


Что тут происходит, тут происходит нативный с точки зрения пи калкулуса процесс квантификации операционной бесконечности, комонада спрятаная внутри тайпчекера кока, преобразует корекурсию в потенциально бесконечный процесс на OCaml.

Здесь не используются никакие биндинги, кроме Lwt.

$ cat Main.v
Require Import Coq.Lists.List.
Require Import Io.All.
Require Import Io.System.All.
Require Import ListString.All.
        Import ListNotations.

  CoInductive Co (E : Effect.t) : Type -> Type :=
    | Ret   : forall (A : Type) (x : A), Co E A
    | Bind  : forall (A B : Type), Co E A -> (A -> Co E B) -> Co E B
    | Call  : forall (command : Effect.command E), Co E (Effect.answer E command)
    | Split : forall (A : Type), Co E A -> Co E A -> Co E A
    | Join  : forall (A B : Type), Co E A -> Co E B -> Co E (A * B).

  Arguments Ret {E} _ _.
  Arguments Bind {E} _ _ _ _.
  Arguments Call {E} _.
  Arguments Split {E} _ _ _.
  Arguments Join {E} _ _ _ _.

  Definition ret   {E : Effect.t} {A : Type} (x : A) : Co E A := Ret A x.
  Definition split {E : Effect.t} {A : Type} (x1 x2 : Co E A) : Co E A := Split A x1 x2.
  Definition join  {E : Effect.t} {A B : Type} (x : Co E A) (y : Co E B): Co E (A * B) := Join A B x y.
  Definition call  (E : Effect.t) (command : Effect.command E):
                   Co E (Effect.answer E command) := Call (E := E) command.

  Notation "'ilet!' x ':=' X 'in' Y" := (Bind _ _ X (fun x => Y))
           (at level 200, x ident, X at level 100, Y at level 200).

  Notation "'ilet!' x : A ':=' X 'in' Y" := (Bind _ _ X (fun (x : A) => Y))
           (at level 200, x ident, X at level 100, A at level 200, Y at level 200).

  Notation "'ido!' X 'in' Y" := (Bind _ _ X (fun (_ : unit) => Y))
           (at level 200, X at level 100, Y at level 200).

  Definition read_line : Co effect (option LString.t) :=
    call effect ReadLine.

  Definition printl (message : LString.t) : Co effect bool :=
    call effect (Print (message ++ [LString.Char.n])).

  Definition log (message : LString.t) : Co effect unit :=
    ilet! is_success := printl message in
    ret tt.

  Definition run (argv : list LString.t): Co effect unit :=
    ido! log (LString.s "What is your name?") in
    ilet! name := read_line in
    match name with
      | None => ret tt
      | Some name => log (LString.s "Hello " ++ name ++ LString.s "!")
    end.

  Parameter infinity : nat.
  Parameter error : forall {A B}, A -> B.

  Fixpoint eval_aux {A} (steps : nat) (x : Co effect A) : Lwt.t A :=
    match steps with
      | O => error tt
      | S steps =>
        match x with
          | Ret _ v => Lwt.ret v
          | Call c => eval_command c
          | Bind _ _ x f => Lwt.bind (eval_aux steps x) (fun v_x => eval_aux steps (f v_x))
          | Split _ x1 x2 => Lwt.choose (eval_aux steps x1) (eval_aux steps x2)
          | Join _ _ x y => Lwt.join (eval_aux steps x) (eval_aux steps y)
        end
    end.

  Definition eval {A} (x : Co effect A) : Lwt.t A :=
    eval_aux infinity x.

  CoFixpoint handle_commands : Co effect unit :=
    ilet! name := read_line in
    match name with
      | None => ret tt
      | Some command =>
        ilet! result := log (LString.s "Input: " ++ command ++ LString.s ".") in
        handle_commands
    end.

  Definition launch (m : list LString.t -> Co effect unit): unit :=
    let argv := List.map String.to_lstring Sys.argv in
    Lwt.launch (eval (m argv)).

  Definition corun (argv : list LString.t): Co effect unit :=
    handle_commands.

  Definition main :=
    launch corun. (* launch run. *)

Extract Constant infinity => "let rec inf = S inf in inf".
Extract Constant error => "fun _ -> failwith ""Unexpected end""".
Extraction "extraction/main" main.


Это то что мы ребятки называем основой верифицированного ядра операционной вычислительной среды для моделирования пи калкулуса и доказательства его основных теорем о бисимуляции, модальных логик и верификации протоколов, и просто для тестирования любых математик в интерактивной среде со своим простым интерпретатором. Наша цель создать единую среду для работы математиков и программистов, где экстракты моделей сразу линкуются с высокопроизводительным CAS рантаймом и CPS интерпретатором. Проверяйте ваши датасеты сразу на моделях заэкстракченых в Rust или OCaml, которые запускаются на seL4, Xen или Mac/Linux. Такой стартап, дали бы денег? :-)
sea

CoFixpoint Extraction

Coq Corecursion:
CoInductive Stream: Type := Cons: nat -> Stream -> Stream.
CoFixpoint facs : nat -> Stream := fun n : nat => Cons n (facs (n+1)).
Definition fs := facs 0.
Extraction "extraction/co" fs.

ML Extraction:
type nat = | O | S of nat
let rec add n m = 
    match n with
    | O -> m
    | S p -> S (add p m)

type stream = __stream Lazy.t
and __stream = | Cons of nat * stream
let rec facs n = lazy (Cons (n, (facs (add n (S O)))))
let fs = facs O

Proto Actor Process
CoInductive Compute (A:Set) : Type :=
   | Return : A -> Compute A
   | Bind : forall (B:Set), (B-> Compute A) -> Compute B -> Compute A.

Process Tree
CoInductive t (E : Effect.t) : Type -> Type :=
  | Ret : forall (A : Type) (x : A), t E A
  | Call : forall (command : Effect.command E), t E (Effect.answer E command)
  | Let : forall (A B : Type), t E A -> (A -> t E B) -> t E B
  | Split : forall (A : Type), t E A -> t E A -> t E A
  | Join : forall (A B : Type), t E A -> t E B -> t E (A * B).
sea

Coq Minimal Emacs Setup

Sick and tired of bullshit programming, lets have a party with Coq.
git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
cd ~/.emacs.d/lisp/PG
make

$ cat ~/.emacs
(load "~/.emacs.d/lisp/PG/generic/proof-site")
(require 'package)
(add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/") t)
(package-initialize)
(add-hook 'coq-mode-hook #'company-coq-mode)
(custom-set-variables '(package-selected-packages (quote (company-coq company))))
(custom-set-faces)

Coq is best to be installed from opam, as opam coq deps found as requires in coq files.
Coq codebase is maybe second after HOL/Isabell.
$ opam search coq | wc -l
     241

I use default emacs from brew
$ brew info emacs
emacs: stable 25.1 (bottled), devel 25.2-rc1, HEAD
sea

Топология на 10 LOC. Определение

Definition subset (A : Type) (u v : A -> Prop) := (forall x : A, u x -> v x).
Definition union (A : Type) (B : (A -> Prop) -> Prop) := fun x : A => exists U, B U /\ U x.
Definition inter (A : Type) (u v : A -> Prop) := fun x : A => u x /\ v x.
Definition empty (A: Type) := fun x : A => False.
Definition full (A: Type) := fun x : A => True.

Structure topology (A : Type) := {
          open :> (A -> Prop) -> Prop;
          empty_open: open (empty _);
          full_open: open (full _);
          inter_open: forall u, open u -> forall v, open v -> open (inter A u v) ;
          union_open: forall s, (subset _ s open) -> open (union A s) }.