These are chat archives for groupoid/exe

3rd
Apr 2016
nponeccop
@nponeccop
Apr 03 2016 00:43
LEAN ASSERTION VIOLATION
т.е. С++ не при чём
про Quote, актуальный материальчик
nponeccop
@nponeccop
Apr 03 2016 01:44

я тут читаю дисер по дедукти http://www.cri.ensmp.fr/people/saillard/Files/thesis.pdf

короче, это dependently typed term rewrite system, а ля Clean

Пока непонятно, зачем им лямбда при живой TRS
nponeccop
@nponeccop
Apr 03 2016 02:54
я так понял, что для shallow embedding
вадлера посмотрел, хороший оратор
Vag
@vagoff
Apr 03 2016 05:51
и для deep embedding тоже
DK -- это универсальный логико-независимый проверятор доказательств, полезный для проверки и прототипирования
особенно удобно им проверять сложные системы типов
например, им проверяли стдлибу Coq
например: Typing Rules кодируются в виде rewriting rules, на них же пишется элаборатор, и можно проверять : сам вывел, сам проверил (схлопнув правила вывода в True, убедившись, что всё сходится)
и как вишенка на торте, есть ещё возможность подключения внешнего confluency checker-а для term rewriting rules, предлагается использовать CSIHO http://cl-informatik.uibk.ac.at/software/csi/ho/
это не как Clean, это как Maude на Lambda Pi
дубовый и простой "как двери" инструмент домашнего тинкеринга с логиками, который можно выучить за 10 минут
Vag
@vagoff
Apr 03 2016 05:57
есть 3 реализации: на OCAML, на Haskell, и на C
похоже на то, что вот эта реализация самая up-to-date https://github.com/mboes/dedukti.git
Vag
@vagoff
Apr 03 2016 06:02
ProofCloud/OpenTheory-сты отдали проверку ему на откуп также
Vag
@vagoff
Apr 03 2016 06:20
или вот ещё use case: пишете вы typechecker к своем ЯП, а доказательства всякие для него делать неохота, потому что всё сильно in the state of flux; так вы тупо описываете typing rules в несколько строчек dedukti, а потом просто генерируете DK файлы typechecker-ом по мере вывода/проверки, и проверяеет потом dkcheck-ом. Легко, просто и можно всё менять без потери труда.
Zeit Raffer
@zraffer
Apr 03 2016 07:24
да, для проверки это может быть полезно - мы до сих пор пользовались минималистичным инструментом Morte, ввиду совпадения снитаксиса, но на данный момент от него уже отказались, так что внешний тул может придать уверенности в себе (пока мы не верифицировали свой верификатор)
Vag
@vagoff
Apr 03 2016 08:48
я ставил таким скриптом: # INSTALL #
set -e
sudo pacman -S ocaml git
yaourt -S opam --noconfirm
opam init -qy
opam update -qy
opam install menhir -qy
mkdir -p tmp
cd tmp
git clone git://scm.gforge.inria.fr/dedukti/dedukti.git
cd dedukti
PATH=$PATH:~/.opam/system/bin make
mkdir -p ~/.local/bin
find _build -name '*.native' -exec bash -c 'cp -a {} ~/.local/bin/basename {} .native' ';'
Vag
@vagoff
Apr 03 2016 09:01

если нужны теории с OpenTheory, то вот: # INSTALL #
set -e
sudo pacman -S mlton ocaml git
wget http://www.gilith.com/software/opentheory/opentheory.tar.gz
tar xzf opentheory.tar.gz
cd opentheory
make
cp -a bin/mlton/opentheory ~/.local/bin/
opentheory update
opentheory upgrade
opentheory install base

git clone https://scm.gforge.inria.fr/anonscm/git/holide/holide.git
cd holide
make
cp -a build/src/main.native ~/.local/bin/holide

Vag
@vagoff
Apr 03 2016 09:43
в правилах можно матчиться прямо по сырой лямбде
Namdak Tonpa
@5HT
Apr 03 2016 13:14
спасибо @vagoff !
:+1:
Namdak Tonpa
@5HT
Apr 03 2016 23:24
ma = function(a) {
                return function(b) {
                    return function(c) {
                        return function(d) {
                            return function(a) {
                                return function(b) {
В пурескрипте тоже внизу нетипизированная чистая лямбда:
http://sloosch.de/ps/gravity/
такое и мы можем уже генерировать, надо космический пример из BeOS взять с галактиками
Chart App
Namdak Tonpa
@5HT
Apr 03 2016 23:40
с примерами на ACL2 и схеме
надо эти примеры на OM записать в этой книге