Homotopy Type Theory and Univalent Foundations

[Slavomir Kaslev]

Безплатна нова книга за Homotopy Type Theory, написана от екип дузина математици и програмисти през последните 6 месеца на Github. Мисля, че би заинтересувала някой в групата =-)

http://homotopytypetheory.org/

--
Slavomir Kaslev

[Boyko Bantchev]

> Безплатна нова книга за Homotopy Type Theory, написана от екип дузина
> математици и програмисти през последните 6 месеца на Github. Мисля, че би
> заинтересувала някой в групата =-)

Можеш ли да разкажеш сбито и на прост език за какво става дума?
Какво е това, как и с какво се яде или пие и защо?
Понеже май (и както обикновено) не е лесно да се разбере от
самия текст. Просвети ни, моля :)

[Krasimir Angelov]

Разлистих я тази книжка миналата седмица, но за сега съм още на въведението. Книгата е добре написана и на мен поне ми просветна за какво става дума. Преди това бях слушал презентации по темата от умни глави, но презентациите бяха за хора дето вече си имат идея за какво става дума. Въпросната книга си е баш за начинаещи.

Идеята е да се комбинира теория на типовете с идеи от топологията за да се реши проблема с равенството в теория на типовете. В теорията на типовете на Martin Löf две функции се считат за равни, т.е. еквивалентни, само ако имат еквивалентни дефиниции. От друга страна в математиката се използва по-силна дефиниция - две функции се считат за еквивалентни само ако те връщат еквивалентни резултати за еквивалентни входни данни. Примерно:

fib 0 = 1

fib 1 = 1

fib n = fib (n-1) + fib(n-2)

е математически еквивалентно (extensional equality) на:

fib n = fib' n 1 1

fib' 0 a b = a

fib' n a b = fib' (n-1) b (a+b)

въпреки че дефинициите на фунциите не са еквивалентни (intensional equality).

Homotopy Type Theory се опитва да реши този проблем. 

2013/7/1 Slavomir Kaslev <slavomi...@gmail.com>

--
You received this message because you are subscribed to the Google Groups "Polyglot Quine" group.
To unsubscribe from this group and stop receiving emails from it, send an email to polyglot-quin...@googlegroups.com.
To post to this group, send email to polyglo...@googlegroups.com.
Visit this group at http://groups.google.com/group/polyglot-quine.
For more options, visit https://groups.google.com/groups/opt_out.
 
 

[Slavomir Kaslev]

Книгата описва нов фундаментален език за матетика и логика, базиран на типове (мисли, Haskell types).

Използвайки Curry-Howard isomorphism (където типовете съответстват на логически твърдения, а функции от съответния тип са доказателства на тези твърдения), твърдения в този език могат да бъдат интерпретирани/преведни от гледна точка на логика, а също и теория на множествата (виж Таблица 1 в книгата стр.15). Това напомня за предишия опит на Whitehead и Russel да поставят математиката върху фундаментлни осннови Principia Mathematica, но използвайки множества вместо типове.

Трета интерпретация на езика и връзка с топология идва от Homotopy theory, където типовете са пространства, стойности от даден тип за точки в тези пространства, биецкии между типовете са пътища/хомотопии.

Едно плюс на езика е, е че твърденията могат да бъдат проверявани от компютър. Всъщност теоремите от книгата са били написани/доказани на Coq и по-късно преведени в традиционнен математически език за книгата. Авторите на книгата, пожелават един ден всички математически публикации да са във форма, в която могат да бъдат автоматично преверени от компютър.

Това са само няколко от областите, които имат връзка с Homotopy Type Theory, но списъка продължава да расте.

Нещо друго, което ме вълнува е връзката между Homotopy Type Theory и методите от новата книга Philippe Flajolet и Robert Sedgewick "Analytic Combinatorics" (видео лекции на Coursera), където използват формализъм много подобен на Homotopy Type Theory (според мен същия) за описване на различни комбинаторни структури и алгоритми. От тези спецификация може веднага да се намери генерираща фунцкия на съответната структура. Тези генериращи фунцкии могат да бъдат използвани за различни изчисления, например намиране на броя елементи на дадена структура, анализ на алгоритмична сложност, намиране на биекции между конструкции и др.

Като бонус, някои физици смятат, че supersymmetry следва директно от фундаментална математика ако се приеме Homotopy Type Theory като основа: връзка.

Така Homotopy Type Theory свързва информатика, много разчлини (вероятно всикчки) области на математиката (от логика и теория на множествата, комбинаторика и генериращи фунцки, до анализ, комплексен анализ, топология и др.), физика и вероятно още. Според мен, много вълнуващо ново развитие.

2013/7/1 Boyko Bantchev <boy...@gmail.com>

--
You received this message because you are subscribed to the Google Groups "Polyglot Quine" group.
To unsubscribe from this group and stop receiving emails from it, send an email to polyglot-quin...@googlegroups.com.
To post to this group, send email to polyglo...@googlegroups.com.
Visit this group at http://groups.google.com/group/polyglot-quine.
For more options, visit https://groups.google.com/groups/opt_out.

--
Slavomir Kaslev

[Boyko Bantchev]

Благодаря на Краси и Слави за поясненията.

За мен в тази работа остава тайна връзката между типове и „другото“,
което в главата ми се асоциира най-общо с топология. Едното е като
че от дискретния свят, другото – тъкмо наопаки.

Като пишат книги, сигурно виждат някаква връзка, но аз съм свикнал
да се питам има ли теорията и прагматична страна. Може би това е
очакваната формална доказуемост, която споменава Слави – ако тя се
окаже налице и ако при това е практически полезна. Но и така да е,
чудя се защо именно топологичен (континуален) подход ще дава
решението на проблем, който е логически.

Според мен в съвременната математика съществува огромен проблем: тя
се разпада на множество поддисциплини, твърде тясно обособени и всяка
натъпкана със специфична терминология. Обемът на терминологията расте
така застрашително, че като че ли заплашва да стане равен на – а това
значи да измести! – съдържанието.

Как може човек, дори да има навици за абстрактно мислене и за
усвояване на математика, да разбере смисъла на някое понятие от
съвременна област, в която той не е специалист? Ето един опит.
Отивам на една от дадените от Слави препратки и там попадам, да
речем на:

Algebra in homotopy theory is homotopical algebra, and in a way
the most fundamental object here is the sphere spectrum, the free
commutative infinity-ring on a single element. The sphere spectrum
is in homotopy foundations what the integers is in traditional
foundations.

Очевидно от този текст е колко Много Важно Нещо е sphere spectrum,
само че самият текст изобщо не ни казва какво всъщност е това. А ако
се опитаме да разберем от Уикипедия, става ясно, че ще е нужно покрай
това да имаме представа какво означава всяко от следните:

homology, cohomology, homology theory,
homotopy, homotopy theory,
algebraic topology,
homotopical algebra,
stable homotopy theory,
generalized cohomology theory,
spectrum,
suspension,
suspension functor,
product space,
quotient space.

Списъкът не е изчерпателен, и всъщност ако човек не прилага усилия да
го ограничава, той ще расте експоненциално от понятие на понятие.

Ама Уикипедия е кофти източник ли? Тогава само си помислете как се
осъществява същото изследване чрез ровене по монографии. Изобщо
осъществимо ли е?

Сега сравнете с евклидовата геометрия, която добре се справя от
около двайсет и пет века насам без да раздува щата …
Май сме пообъркали нещо напоследък.

Дали в крайна сметка разбрах какво е sphere spectrum? Не, отказах се.

П.П. Не разбрах връзката между HoTT и книгата Analytic Combinatorics.
Прехвърлял съм я, както и по-късната An Introduction to the Analysis
of Algorithms, 2nd ed. (http://amazon.com/dp/032190575X) от същите
автори, но не съм забелязал да ползват някакъв по-особен запис или
метод. Колкото до пораждащите функции, това си е отдавнашна,
класическа в комбинаторния анализ и анализа на алгоритми техника.
Кое е специфичното у Седжуик и Флажоле?

[Slavomir Kaslev]

Седжуик и Флажоле са развили "анализ на типовете". Пример, предписан от книгата за вкус:

Да речем, че искаме структура от данни дърво къдете всеки възел има произволен брой деца. На Хаскел, може да се дефинира така:

data G a = Node a [G a]

По Седжуик и Флажоле, използваме символен метод и превеждаме този тип до следното уравнение:

G(z) = z SEQ(z)                   (1)

Където SEQ(z) е типа списък и може да се дефенира така:

SEQ(z) = 1 + z + z^2 + z^3 + .... = 1 / (1 - z)

Замествайки SEQ(G(z)) = 1 / (1-G(z)) в (1), получаваме уравнението

G(z) = z / (1 - G(z))

=> G(z) - G(z)^2 = z

Решаваме като квадратично уравнение:

G(z) = 1/2 * (1 - sqrt(1 - 4z))

Развиваме в ред на Тейлър и след кратки сметки получаваме n-тия коефициент:

G(z) = Sum[n,0,inf] (Gn z^n), където

Gn = 1 / (4n - 2)  (2n)

                         (  n)

Gn ни дава броя дървета с пройзволен бранчинг фактор, с n възела.

Това е само вкус, но методите са много ефективни. Конструкциите върху които работят са най-разнообразни (от дървета, списъци, стрингове, до множества, цикли, пермутации, разделяния).

Книгата представя и добро въведение в комплексния анализ и методи. За оценка на дълбочината на материала, стига се до асимптотични методи, анализ на сингулярности, седлови методи и др.

2013/7/6 Boyko Bantchev <boy...@gmail.com>

--
You received this message because you are subscribed to the Google Groups "Polyglot Quine" group.
To unsubscribe from this group and stop receiving emails from it, send an email to polyglot-quin...@googlegroups.com.
To post to this group, send email to polyglo...@googlegroups.com.
Visit this group at http://groups.google.com/group/polyglot-quine.
For more options, visit https://groups.google.com/groups/opt_out.

--
Slavomir Kaslev

[Slavomir Kaslev]

G(z) = z SEQ(G(z))                   (1)

oops =-)

2013/7/6 Slavomir Kaslev <slavomi...@gmail.com>

--
Slavomir Kaslev

[Boyko Bantchev]

Слави, изглежда любопитно, но няма да се отървеш лесно, понеже ми се
струва, че липсва точно важната част :)

Решаването на рекурентно уравнение за пораждаща функция е стандартна
работа. Въпросът е как стигаме до самото уравнение – в твоя пример
това за G(z). По-точно, как от

data G a = Node a [G a]

стигаме до (1)?

Тук трябва да се уточнят няколко неща.

Какво е SEQ(z) и откъде се взима? Изглежда, това е пораждаща функция,
съответна на типа (в случая „подтип“) списък, така ли? А защо тя е
именно 1+z+z²+z³+…? Ако типът беше

data G a = Node a (Set a)

коя щеше да е пораждащата функция (за множесто, Set), същата като
за списък или друга, и защо? Защо в (1) SEQ(z) се умножава със z –
защото типът е декартово произведение на a и [G a] ли?

Изобщо, (а) как в общия случай се определя съответствието между тип и
пораждаща функция, и (б) за какво в крайна сметка служи съответната на
типа п.ф.?

Последното е съществено, защото, ако е за да се броят структурно
различните дървета и др.под. структури, то този въпрос е отдавна
изследван и обилно е писано (вкл. не една монография) точно по него
– това е т.нар. преброителна комбинаторика. Тогава има ли някаква
полза това броене да се свързва с типове, т.е. обслужва ли се по
някакъв начин именно програмирането. Не мога да съобразя.

[Boyko Bantchev]

> Тогава има ли някаква
> полза това броене да се свързва с типове, т.е. обслужва ли се по
> някакъв начин именно програмирането. Не мога да съобразя.

Или пък може би предполагаемата полза е в другата посока – задаването
на комбинаторни структури чрез т.нар. „алгебрични“ (йерархични,
конструктивни) типове да прави преброителната комбинаторика по-удобна?
Т.е. езиковите инструменти, които досега сме прилагали само в
програмирането, да проработят за чисто комбинаторни цели, извън
контекста на каквото и да е програмиране.

Както сега си мисля, вероятно тъкмо това всъщност е работата.
Слави, благодаря че обърна внимание!

[Stefan Kanev]

Абе хора, я дайте списък от две-три книги, които човек трябва да прочете, за да разбере за какво си говорите :)

2013/7/7 Boyko Bantchev <boy...@gmail.com>

[Krasimir Angelov]

На 06 юли 2013, 12:47, Boyko Bantchev <boy...@gmail.com> написа:

Благодаря на Краси и Слави за поясненията.

За мен в тази работа остава тайна връзката между типове и „другото“,
което в главата ми се асоциира най-общо с топология.  Едното е като
че от дискретния свят, другото – тъкмо наопаки.

Не е задължително. Като говорят за пространства се има предвид топологични пространства, а те не е задължително да са гладки и непрекъснати. Най-простият вид топологично пространство е множество от точки, за които е указано кои точки се смятат за близки и кои не. Уйкипедия дава проста дефиниция.

 

В компютърните науки май най-често срещани са дискретните пространства. Като пример за дискретно пространство можем да вземем пространството на компютърните алгоритми. Всеки алгоритъм е точка от това пространство. Ако два различни алгоритъма решават една и съща задача, то те са свързани с път в пространството, тъй като можем да деформираме един алгоритъм в друг. Ако пък задачите са различни, то точките са несвързани. Дискретно пространство от точки свързани с пътища вече познаваме - добре познатите графи.

Между другото физиците също все повече се интересуват от дискретни пространства, тъй като е много вероятно, че физическото пространството е също дискретно в много малък мащаб. Книгата на Alain Connes - "Noncommutative Geometry" поставя математическите основи на нов вид геометрия, която освен с досега познатите ни геометрични обекти може да работи също така с графи и фрактали. Върху тези обекти например могат да се дефинират диференциално и интегрално смятане. За съжаление книгата е много трудна за четене тъй като е препълнена с технически термини точно както казваш. За щастие попаднах на тази статия:

http://arxiv.org/pdf/hep-th/9404112v2.pdf

която дефинира диференциалното смятане върху графи и доста по-смилаема. Интересното в случая е, че в нормалното диференциално смятане умножението на скалар и вектор е комутативна операция, но когато го пренесем върху граф операцията става не комутативна. Същото се наблюдава и във физиката, и като следствие от това, наблюдаваме дуализъм между частици и вълни. Докато във физиката това е все още мистерия, когато работим с графи всичко става просто и очевидно.

[Boyko Bantchev]

> Като пример за дискретно пространство можем да вземем пространството
> на компютърните алгоритми. Всеки алгоритъм е точка от това
> пространство. Ако два различни алгоритъма решават една и съща
> задача, то те са свързани с път в пространството, тъй като можем да
> деформираме един алгоритъм в друг. Ако пък задачите са различни, то
> точките са несвързани. Дискретно пространство от точки свързани с
> пътища вече познаваме - добре познатите графи.

Вярно е, че има и дискретен вариант на топология. Но самата тя до
такава степен се асоциира с непрекъснатостта, че се налага винаги да
се уточнява, ако става дума за дискретни множества. Така че ако това
се разглежда в книгата HOTT, бележката ти идва тъкмо на място.

Не че оттам нататък става по-ясно, поне за мен. Изглежда ми твърде
отвлечено. Ако полезността е в това, че се създава някакъв общ език
на математиката, както се спомена – ами добре :) Но някаква
по-непосредствена връзка с информатиката не виждам. Например, даден
граф може да се разглежда като топол. пространство, да, но какво
печелим от това в сравнение с третирането му именно като граф?
А „деформирането на един алгоритъм в друг“ ми се вижда изкуствена
представа за мнозинството от случаите. Дори за много прости задачи,
за каквито се сещам, различните алгоритми са дотолкова наистина
различни, че не виждам как ще се привеждат един в друг. Тогава
„пътят в топологичното пространство“ между тях се състои само от
крайните си точки. Така че примерът с пространство от алгоритми е
ясен, но ми изглежда тривиален. Сигурно има нетривиални, които не
са лесно разбираеми. А нетривиален и разбираем има ли?

[Slavomir Kaslev]

2013/7/7 Stefan Kanev <stefan...@gmail.com>

Абе хора, я дайте списък от две-три книги, които човек трябва да прочете, за да разбере за какво си говорите :)

http://www.amazon.com/Analytic-Combinatorics-Philippe-Flajolet/dp/0521898064

Видео лекции (от Седжуик!).

[Slavomir Kaslev]

2013/7/6 Boyko Bantchev <boy...@gmail.com>

Слави, изглежда любопитно, но няма да се отървеш лесно, понеже ми се
струва, че липсва точно важната част :)

Решаването на рекурентно уравнение за пораждаща функция е стандартна
работа.  Въпросът е как стигаме до самото уравнение – в твоя пример
това за G(z).  По-точно, как от

    data G a = Node a [G a]

стигаме до (1)?

Тук трябва да се уточнят няколко неща.

Какво е SEQ(z) и откъде се взима?  Изглежда, това е пораждаща функция,
съответна на типа (в случая „подтип“) списък, така ли?  А защо тя е
именно 1+z+z²+z³+…?  Ако типът беше

SEQ е тип списък. Хаскел има синтаксис за списъци и не е очевидно за Prelude дефинициата

data [a] = a : [a]

Но ако дефинираме еквивалентно така:

data SEQ a = Nil | Cons a (SEQ a)

се превежда до:

SEQ(z) = 1 + z SEQ(z)

=> SEQ(Z) = 1 / (1 - z) = 1 + z + z^2 + z^3 + ...

 

    data G a = Node a (Set a)

коя щеше да е пораждащата функция (за множесто, Set), същата като
за списък или друга, и защо?  Защо в (1) SEQ(z) се умножава със z –
защото типът е декартово произведение на a и [G a] ли?

Да. `z` е типовата променлива `a`.

 

Изобщо, (а) как в общия случай се определя съответствието между тип и
пораждаща функция, и (б) за какво в крайна сметка служи съответната на
типа п.ф.?

Според мен, пораждащата функция е еквивалентен тип, разписан като ред на Тейлър.

 

Последното е съществено, защото, ако е за да се броят структурно
различните дървета и др.под. структури, то този въпрос е отдавна
изследван и обилно е писано (вкл. не една монография) точно по него
– това е т.нар. преброителна комбинаторика.  Тогава има ли някаква
полза това броене да се свързва с типове, т.е. обслужва ли се по
някакъв начин именно програмирането.  Не мога да съобразя.

--
You received this message because you are subscribed to the Google Groups "Polyglot Quine" group.
To unsubscribe from this group and stop receiving emails from it, send an email to polyglot-quin...@googlegroups.com.
To post to this group, send email to polyglo...@googlegroups.com.
Visit this group at http://groups.google.com/group/polyglot-quine.
For more options, visit https://groups.google.com/groups/opt_out.

--
Slavomir Kaslev

[Slavomir Kaslev]

пак oops =-)

data [a] = [] | a : [a]

2013/7/8 Slavomir Kaslev <slavomi...@gmail.com>

--
Slavomir Kaslev

[Boyko Bantchev]

> SEQ е тип списък. Хаскел има синтаксис за списъци и не е очевидно за Prelude
> дефинициата
>
> data [a] = a : [a]
>
> Но ако дефинираме еквивалентно така:
>
> data SEQ a = Nil | Cons a (SEQ a)
>
> се превежда до:
>
> SEQ(z) = 1 + z SEQ(z)
> => SEQ(Z) = 1 / (1 - z) = 1 + z + z^2 + z^3 + ...

Виж сега, как се прави списък на Хаскел е ясно, справяме се и
без пояснения :)

Вече писах какво НЕ е ясно, но явно трябва да повторя.
Не е ясно как от определение на тип да стигнеш до пораждаща
функция. И то в общия случай – т.е. според каква система от
правила от определение на тип получаваш пораждаща функция.

Зададох и други въпроси, но да ги пропуснем ...

А SEQ или е тип, или е пораждаща функция. Няма как да е и двете.
Изобщо ти някак уеднаквяваш типове и пораждащи функции и не
разбирам защо държиш да е така.

[Slavomir Kaslev]

2013/7/9 Boyko Bantchev <boy...@gmail.com>

> SEQ е тип списък. Хаскел има синтаксис за списъци и не е очевидно за Prelude
> дефинициата
>
> data [a] = a : [a]
>
> Но ако дефинираме еквивалентно така:
>
> data SEQ a = Nil | Cons a (SEQ a)
>
> се превежда до:
>
> SEQ(z) = 1 + z SEQ(z)
> => SEQ(Z) = 1 / (1 - z) = 1 + z + z^2 + z^3 + ...

Виж сега, как се прави списък на Хаскел е ясно, справяме се и
без пояснения :)

Вече писах какво НЕ е ясно, но явно трябва да повторя.
Не е ясно как от определение на тип да стигнеш до пораждаща
функция.  И то в общия случай – т.е. според каква система от
правила от определение на тип получаваш пораждаща функция.

От Хаскел дефинициятата

(1)    data SEQ a = Nil | Cons a (SEQ a)

чрез чисто символно изчисление се превежда до уравнението

(2)    SEQ(z) = 1 + z SEQ(z)

Решението на това уравнение за SEQ(z) е пораждащата фунцкия на типа.

 

Зададох и други въпроси, но да ги пропуснем ...

Ще се наложи да погледнеш книгата или видео лекциите. Не мога да обясня 600 страници теория в няколко мейла. Написах това изчисление само за вкус на методите. Книгата има много, много примери, които ще ти отговорят на въпросите.

 

А SEQ или е тип, или е пораждаща функция.  Няма как да е и двете.
Изобщо ти някак уеднаквяваш типове и пораждащи функции и не
разбирам защо държиш да е така.

SEQ е тип, дефиниран в (1). Схващането, че пораждащите функции също са типове е нова идея и за това казах "според мен". Не мога да го докажа в общия случай (ще трябва да разчиташ, че методите от комплексен анализ работят), но мога да го илюстрирам с няколко примери и да го докажа в частност.

Да вземем SEQ. От (2)

=> SEQ(z) = 1 / (1 - z) = 1 + z + z^2 + z^3 + ...

Десния израз е пораждащата функция на SEQ. Нека я кръстим G(z)

(3)    G(z) = 1 + z + z^2 + z^3 + ...

Може да преведем този израз обратно на псевдо-Хаскел

(4)    data G a = C0 | C1 a | C2 a a | C3 a a a | ....

Сега искаме да докажем, че (SEQ a) от (1) и (G a) от (2) са еквивалентни. За целта ще дефинираме две функции f, g:

f :: SEQ a -> G a

f Nil = C0

f (Cons x0 Nil) = C1 x0

f (Cons x0 (Cons x1 Nil)) = C2 x0 x1

....

g :: G a -> SEQ a

g C0 = Nil

g C1 x0 = Cons x0 Nil

g C2 x0 x1 = Cons x0 (Cons x1 Nil)

...

(Като скоба f,g са по-чисти, ако се използва Хаскел синтаксис за списъци

  f :: [a] -> G a

  f [] = C0

  f [x0] = C1 x0

  f [x0, x1] = C2 x0 x1

  f [x0, x1, x2] = C3 x0 x1 x2

  ...

  g :: G a -> [a]

  g C0 = []

  g C1 x0 = [x0]

  g C2 x0 x1 = [x0, x1]

  g C3 x0 x1 x2 = [x0, x1, x2]

  ...)

Очевидно 

  (f . g) :: SEQ a -> SEQ a    ===  id

  (g . f) :: G a -> G a             ===  id

защото f праща списъци с дължина n в наредени n-орки, запазвайки елементите, а g праща наредени n-орки в списъци с дълцина n, запазвайки елементите. Неформално:

    f [x0, x1, .. xn] = (x0, x1, ... xn)

    g (x0, x1, .. xn) = [x0, x1, ... xn]

Следователно (SEQ a) и (G a) са еквивалентни типове. qed.

Мисля, че доказателството може да се направи формално на Coq, но това е едно от нещата, които ми предстои да науча. Също, предполагам че f,g могат да се напишат на нормален Хаскел, а не на псевдо-Хаскел, който ползвам за илюстрацията горе. По-добри Хаскел програмисти от мен (Краси?) могат да кажат по-добре.

Още няколко илюстрации за прости пораждащи функции.

1. Нека 

    G(z) = 1

което се превежда до

    data G a = C

което е така наречения unit type.

2. Нека

    G(z) = 2

се превежда до

    data G a = C0 | C1

което изглежда познато на повечето Хаскел програмисти, именно:

    data Bool = True | False

3. Нека

    G(z) = 1 + z

се превежда до

    data G a = C0 | C1 a

което също изглежда познато, а именно типа (Maybe a):

    data Maybe a = Nothing | Some a

От такива съображения, мисля, че пораждащите фунцкии също са типове разписани в ред на Тейлър. Още ли не си убеден, Бойко?

--
Slavomir Kaslev

[Boyko Bantchev]

> разписани в ред на Тейлър. Още ли не си убеден, Бойко?

Ако питаш дали съм убеден, че пораждаща ф-я и тип (в смисъл на data
в Хаскел) са едно и също нещо – убеден съм, че не са.
П. ф-и са числови функции, а типовете в Хаскел не са числови функции
и не са изобщо функции.

Дали п.ф. е записана в затворен вид или в ред на Тейлър не променя
факта, че тя е числова функция. Това са само различни нейни
представяния, но математическият обект функция е един и същ.

Ти превръщаш п.ф. в типове на Хаскел, което за мен няма смисъл.
(Да не говорим, че на една п.ф. можеш да съпоставиш не един тип.)
Известен смисъл има обратното: от тип да получаваш съответна нему
п.ф. Това вече би трябвало да е еднозначно, а въпросът ми беше
какви правила осигуряват въпросното съответствие, т.е. извличането
на п.ф. от тип. Казано другояче, там където споменаваш:

> чрез чисто символно изчисление се превежда до уравнението

вместо да се каже само „символно изчисление“, което само по себе
си не значи нищо, би трябвало да се посочат правилата, за каквито
говоря. Но понеже пиша едно и също нещо вече трети път, всъщност
вече и не питам – мисля, че е по-добре да изоставим темата.

[Slavomir Kaslev]

2013/7/9 Boyko Bantchev <boy...@gmail.com>

> разписани в ред на Тейлър. Още ли не си убеден, Бойко?

Ако питаш дали съм убеден, че пораждаща ф-я и тип (в смисъл на data
в Хаскел) са едно и също нещо – убеден съм, че не са.
П. ф-и са числови функции, а типовете в Хаскел не са числови функции
и не са изобщо функции.

Аз твърдя, че Хаскел типове и техните (комплексни) пораждащи фунцкии са еквивалентни в смисъла, в който Curry-Howard isomorphism твърди, че Хаскел типове са екивавелтни с техния превод до логически твърдения.

С други думи, това е нов тип изоморфизъм подобен на Curry-Howard, но между Хаскел типове и комплексни функции.

Очаквах транслацията, да е очевидна от примерите, които дадох. В "Analytic Combinatorics" могат да се намерят много други примери и транслацията от техния формализъм към комплексни функции е обяснена по-формално. После, транслацията от техния формализъм до Хаскел типове е очевидна.

Неформално, правилата за превод в едната посока са: discriminated unions (sum types) отива в +; декартово произведение (product types) отива в *, типовата променлива a отива в комплексна променлива z.

В другата посока правилата на превод са подобни.

--
Slavomir Kaslev

[Boyko Bantchev]

Слави, позволявам си да се обадя отново по тази тема, по-точно по
допълнително повдигнатата от теб тема за метода в книгата Analytic
Combinatorics, по следната причина. След като прегледах тази книга
по-подробно (както казах, досега я бях поглеждал само съвсем бегло),
виждам, че представата ти за някаква връзка с типове, такива като в
програмирането, изобщо не отговаря на истината. А това, което
разказваш тук, дава заблуждаваща представа за книгата (съжалявам,
че трябва да го кажа).

Ти още в началото обяви, че „Седжуик и Флажоле са развили "анализ на
типовете"“ и все говориш за типове, при това даваш примери с Хаскел.
В книгата обаче такова нещо изобщо няма. Авторите са развили анализ
на комбинаторните структури, каквото казва и заглавието, а типове
нито споменават, нито имат нещо общо с предмета.

Какво *наистина* предлага книгата? Ще се опитам да резюмирам подхода
към комбинаторния анализ, изложен в нея.

Построява се формален език за описване на обширен клас от комбинаторни
структури (КС). В този език КС се образуват чрез построителни
операции, в ролята на каквито се вземат теоретикомножествените
конструкции множество, обединение, декартово произведение, редица,
степенно множество, мултимножество и цикъл.

Показано е, че на всяка КС от така представения клас можем да
съпоставим пораждаща функция (ПФ), като при това образуването на
ПФ става на основата на аритметични съответствия на построителните
операции (напр. аритметично умножение за декартовото произведение).
(Както би трябвало да е ясно на всеки занимавал се поне малко с
комбинаторика, ПФ служи за пресмятане на броя на различимите
представители на съответната КС, напр. броя на двоичните дървета с k
възела).

И така, ценността на подхода е двояка.
• Първо, той осигурява еднообразно и формално представяне (кодиране)
на комбинаторни структури чрез малък брой образуващи операции.
• Второ, показано е, че на основата на това представяне пораждащите
функции на КС могат да бъдат извеждани систематично и дори
механично (извеждането е потенциално автоматизируемо).

Може да се добави още – това е загатнато и в книгата – че освен за
намиране на ПФ, формалното представяне на КС би могло да помага и
за построяването на алгоритми: за изброяване и др.

Във всичко това няма причина да се говори за „типове“ и изобщо сюжетът
да се пренася на терена на езиците за програмиране, независимо Хаскел
или друг. Комбинаторните структури и типовете са съвсем различни
понятия! Истина е, че за изграждане и на едното, и на другото се
използват конструктивни езици, но друга прилика няма. (А конструктивни
формализми се прилагат и другаде.)

Няма причина да се говори и за „изоморфизъм“ или „еквивалентност“,
защото съответствието е само в една посока – на (изрази, представящи)
КС съпоставяме ПФ. Не обратното.

[Krasimir Angelov]

На 10 юли 2013, 01:19, Boyko Bantchev <boy...@gmail.com> написа:

> разписани в ред на Тейлър. Още ли не си убеден, Бойко?

Ако питаш дали съм убеден, че пораждаща ф-я и тип (в смисъл на data
в Хаскел) са едно и също нещо – убеден съм, че не са.
П. ф-и са числови функции, а типовете в Хаскел не са числови функции
и не са изобщо функции.

Не съм чел въпросната книга, но идеята за пораждаща функция ми звучи подобна на представянето за абстрактни типове от данни в теория на категориите. Идеята е, че който и да е абстрактен тип може да се представи чрез комбинирането на четири примитивни типа:

data One = One

data a :+ b = Inl a | Inr b

data a :* b = Prod a b

newtype Mu f = In (f (Mu f))

Примерно списъците могат да се представят по следния начин:

newtype List' a b = List' (One :+ (a :* b))

type List a = Mu (List' a)

Тук типа One :+ (a :* b) можем да запишем като формален алгебричен израз, т.е. 1 + а*b. Трика е, че за да получим истински списъци ще ни трябва и рекурсия и това е ролята на типа Mu. С така получените алгебрични изрази вече могат да се правят интересни неща примерно ако диференцираме функцията спрямо 'a' получаваме друга функция която формално съответства на zipper за съответния тип.

До тук става въпрос само за формално сходство на типове и аритметични изрази. Не бих се учудил обаче ако може да се отиде и по-далеч. Подобно преминаване от дискретни структури към "пораждащи функции" съм виждал поне веднъж при анализа на статистически модели за контекстно свободни граматики.

[cutthroat]

Един интересен разбор на специалното в HOTT

http://existentialtype.wordpress.com/2013/07/10/constructive-mathematics-is-not-meta-mathematics/

[Slavomir Kaslev]

Забавих се с отговор на този мейл, защото усещам канала е шумен и с Бойко не се разбираме напълно.

Ето как Седжуик и Флажоле описват аналитичната комбинаторика в тяхната книга:

"ANALYTIC COMBINATORICS aims at predicting precisely the properties of large structured combinatorial configurations"

Алгебричните типове в Хаскел са език за дефиниране на определен клас комбинаторни структури (като списъци, дървета, графи, и т.н.).

Това, което представих преди в няколко мейла е просто приложение на аналитична комбинаторика за анализ на няколко комбинаторни структури, дефинирани чрез алгебрични типове в Хаскел. Това е всичко.

Транслацията която описах от алгебричен тип до функционално уравнение на генериращата функция е просто трик, щастливо съвпадение между традиционната математическата нотация и Хаскел синтаксиса за алгебрични типове, което спестява малко сметки и не губи информация.

2013/7/11 Boyko Bantchev <boy...@gmail.com>

--
You received this message because you are subscribed to the Google Groups "Polyglot Quine" group.
To unsubscribe from this group and stop receiving emails from it, send an email to polyglot-quin...@googlegroups.com.
To post to this group, send email to polyglo...@googlegroups.com.
Visit this group at http://groups.google.com/group/polyglot-quine.
For more options, visit https://groups.google.com/groups/opt_out.

--
Slavomir Kaslev

[cutthroat]

Може да погледнете и тази книжка на същата тема по комбинаторика:

``Combinatorial Species and Tree-like Structures''

http://www.amazon.com/Combinatorial-Structures-Encyclopedia-Mathematics-Applications/dp/0521573238

[Boyko Bantchev]

> Ето как Седжуик и Флажоле описват аналитичната комбинаторика в
> тяхната книга: "ANALYTIC COMBINATORICS aims at predicting precisely
> the properties of large structured combinatorial configurations"
> Алгебричните типове в Хаскел са език за дефиниране на определен клас
> комбинаторни структури (като списъци, дървета, графи, и т.н.).

> ...................

В предишния пост ясно казах с какво не съм съгласен.
По-специално, т.нар. „алгебрични“ (предпочитам „конструктивни“) типове
в Хаскел или др. под. език не задават комбинаторни структури, а именно
(даннови) типове. Комбинаторните структури и типовете са съвсем
различни понятия и обслужват различни цели. Така че не е уместно да
се твърди, че книгата развива „анализ на типовете“, нито че типовете
дефинират комбинаторни структури. (Нека не ни обърква това, че и в
единия, и в другия случай обекти на разглеждане може да са напр.
дървета.)

Например при типовете и помен няма от *размер*, за какъвто се
споменава в цитираното по-горе изречение от учебника. При типовете
изобщо няма нищо свързано с броене, а то е нещото, заради което
съществуват пораждащите функции. Следователно е безсмислено едното
и другото да се разглеждат на едно място.

[Slavomir Kaslev]

2013/7/24 Boyko Bantchev <boy...@gmail.com>

> Ето как Седжуик и Флажоле описват аналитичната комбинаторика в
> тяхната книга: "ANALYTIC COMBINATORICS aims at predicting precisely
> the properties of large structured combinatorial configurations"
> Алгебричните типове в Хаскел са език за дефиниране на определен клас
> комбинаторни структури (като списъци, дървета, графи, и т.н.).

> ...................

В предишния пост ясно казах с какво не съм съгласен.
По-специално, т.нар. „алгебрични“ (предпочитам „конструктивни“) типове
в Хаскел или др. под. език не задават комбинаторни структури, а именно
(даннови) типове.  Комбинаторните структури и типовете са съвсем
различни понятия и обслужват различни цели.  Така че не е уместно да
се твърди, че книгата развива „анализ на типовете“, нито че типовете
дефинират комбинаторни структури.  (Нека не ни обърква това, че и в
единия, и в другия случай обекти на разглеждане може да са напр.
дървета.)

 

Истината може да няма корелация с това което си съгласен или не. Outline of combinatorics: забелижи количеството връзки към "Analytic Combinatorics", "Algebraic data type", "List", "Array", etc.

 

Например при типовете и помен няма от *размер*, за какъвто се
споменава в цитираното по-горе изречение от учебника.  При типовете
изобщо няма нищо свързано с броене, а то е нещото, заради което
съществуват пораждащите функции.  Следователно е безсмислено едното
и другото да се разглеждат на едно място.

Какво се дефинира под размер също е въпрос на избор и може да се променя от проблем на проблем върху същото изчисление. Виж главата за дървета където броят различните видове по външни, вътрешни, общо възли. Една и съща конструкция, различна дефиниция за размер, различна резултатна генерираща функция.

 

--
You received this message because you are subscribed to the Google Groups "Polyglot Quine" group.
To unsubscribe from this group and stop receiving emails from it, send an email to polyglot-quin...@googlegroups.com.
To post to this group, send email to polyglo...@googlegroups.com.
Visit this group at http://groups.google.com/group/polyglot-quine.
For more options, visit https://groups.google.com/groups/opt_out.

--
Slavomir Kaslev

[Boyko Bantchev]

> Истината може да няма корелация с това което си съгласен или не. Outline of
> combinatorics: забелижи количеството връзки към "Analytic Combinatorics",
> "Algebraic data type", "List", "Array", etc.

Аман, бе човек :) Къде я видя тази твоя „истина“?

Статията от Уикипедия, която привеждаш, не доказва нищо различно от
това, което казах.

Първо, тя изобщо не се отнася до тематиката на дискутираната от нас
книга и поради това няма отношение към спора ни. Ако трябва да
посочим наистина релевантен текст оттам – моля:
http://en.wikipedia.org/wiki/Analytic_combinatorics.

Второ, нито едната, нито другата, нито изобщо коя да е статия ти дава
основание да уеднаквяваш комбинаторни структури и даннови типове.

Разликите между тези две понятия са толкова съществени, че не виждам
как изобщо могат да подлежат на обсъждане. Това е почти като да
сравняваш крава и параход, да речем.

Все пак, ако ти трябват косвени свидетелства – и не ти е достатъчно,
че самата книга Analytic combinatorics и с една дума не подкрепя
тезата ти – разгледай, пак в Уикипедия, статията за даннов тип:
http://en.wikipedia.org/wiki/Datatype
и тези за комбинаторни структури:
http://en.wikipedia.org/wiki/Combinatorial_class
http://en.wikipedia.org/wiki/Combinatorial_species
Не ще да е случайно, че нито в първата се споменава комбинаторика,
нито в другите две се обсъждат даннови типове … с едно много
показателно изключение: в последната статия стои фразата
„algebraic descriptions of species are quite different from type
specifications in programming languages like Haskell“.

> Какво се дефинира под размер също е въпрос на избор и може да се променя от
> проблем на проблем върху същото изчисление. Виж главата за дървета където
> броят различните видове по външни, вътрешни, общо възли. Една и съща
> конструкция, различна дефиниция за размер, различна резултатна генерираща
> функция.

Какво значение има какво именно се брои?! Обърнах ти внимание, че
броенето се отнася до комбинаторните структури и няма нищо общо с
понятието даннов тип в програмирането. За спора ни само това е от
значение.

[Slavomir Kaslev]

Мислим на различни нива, Бойко. Ти мислиш за върховете (nodes, sites), докато аз мисля за ребрата (edges, links) на графа. Докато ти гледаш различните обасти от науката/математика/инжинерство като независими, аз гледам структурата на връзките между тях. Сиреч, това което Google наричат PageRank, a математиците eigenvalue problem.

Превода от algebraic data type до математическо уравнение може да е нова идея; поне аз не намерих някъде изказана същата идея, за да пратя линк (освен ако не четеш Analytic Combinatorics по правилния начин). Разговора щеше да свърши много бързо, както ако споряхме дали има сходство между algebraic data types и logic statements (отговор: да, има Curry-Howard correspondence) или дали може да взимаш производни на algebraic data types (отговор: да, можеш Differentiating Data Structures; всъщност дифенцирането е много просто приложение на превода, който показах -- транслираш, решаваш уравнението и взимаш производна; получаваш същите резултати като от линка).

Въпреки, че ми се иска да не беше така; сега разбирам, че тук явно не е мястото където могат да се дискутират нови идеи свободно. Ще представя идеята в форма приятна за четене и ще я кача онлайн на моя сайт когато намеря време.

Причината да вярвам, че работи е, че използвам тази траснлация като основа за един хоби проект по-който работя от известно време. Не само, че идеята работи (получава същите резултати ако направиш изчислението на някакъв друг начин за същия проблем), но е особено богата математически поради връзките с диференциални уравнения, линейни оператори, повърхности на Риман, ред на Тейлър, Паде апроксиманти, механика/физика и т.н.

Това Wigner нарича The Unreasonable Effectiveness of Mathematics. Всичко е математика, ако знаеш как да го погледнеш по правилния начин. Включително езиците програмиране, като пример Хаскел. Това разбира се не трябва да ни учудва като знаем, че Хаскел е основно инспириран от математически идеи, а именно Lambda calculus и Arithmetic (+, *, sum/product types).

2013/7/25 Boyko Bantchev <boy...@gmail.com>

--
You received this message because you are subscribed to the Google Groups "Polyglot Quine" group.
To unsubscribe from this group and stop receiving emails from it, send an email to polyglot-quin...@googlegroups.com.
To post to this group, send email to polyglo...@googlegroups.com.
Visit this group at http://groups.google.com/group/polyglot-quine.
For more options, visit https://groups.google.com/groups/opt_out.

--
Slavomir Kaslev

[Boyko Bantchev]

On Wednesday, July 31, 2013 6:58:23 AM UTC+3, Slavomir Kaslev wrote:

..................

Леле!  Тук само за международното положение няма нищо.

[Stefan Kanev]

> Въпреки, че ми се иска да не беше така; сега разбирам, че тук явно не е мястото където могат да се дискутират нови идеи свободно.

Дискутират свободно != всички да са съгласни

[Slavomir Kaslev]

2013/7/31 Stefan Kanev <stefan...@gmail.com>

> Въпреки, че ми се иска да не беше така; сега разбирам, че тук явно не е мястото където могат да се дискутират нови идеи свободно.

Дискутират свободно != всички да са съгласни

Да, "свободно" май е излишна от това изречение. Само "сега разбирам, че тук явно не е мястото където могат да се дискутират нови идеи" казва точно каквото имах пред вид.

--
Slavomir Kaslev

[Slavomir Kaslev]

Международното положение мога да ти го кажа лично, след 2 седмици съм в София. Освен това, международното положение е променливо и може само да се говори. Виж, математиката е вечна и е хубаво да се запише.

Което ми напомня, дали да не направим сбирка на групата в някоя пицария в Лозенец? Като в доброто не-толкова отдавнашно време. Аз съм в бг между 9-26 август. Стеф, какво мислиш?

--
Slavomir Kaslev

[Stefan Kanev]

Дискутират != .....

--

[Stefan Kanev]

Бива. Зарибен съм :).

На 24 има конференция в Бургас. Преди това - когато кажете

--

[Slavomir Kaslev]

2013/7/31 Stefan Kanev <stefan...@gmail.com>

Бива. Зарибен съм :).

На 24 има конференция в Бургас. Преди това - когато кажете

Аз също не мога 24ти уикенда, празнуваме 10 години от завършване на гиманазия (и аз не знам кога минаха =-). Четвъртък 21ви вечерта преди уикенда? Предлагам да отоворим нова тема, че някои хора може да са mute-нали тази твърде шумна дискусия вече.

--
Slavomir Kaslev

[Slavomir Kaslev]

Обещах преди доста време да напиша блог пост за спора, който водехме, но още не съм стигнал до там. Междувременно обаче написах два кратки статии използвайки транслацията между Хаскел и уравнения на github: iterating.pdf и balanced.pdf. Надявам се скоро да напиша и блог поста с по-прости примери, но този път няма да обещая кога =-)

2013/7/31 Slavomir Kaslev <slavomi...@gmail.com>

--
Slavomir Kaslev

[Boyko Bantchev]

> Обещах преди доста време да напиша блог пост за спора, който водехме, но още
> не съм стигнал до там. Междувременно обаче написах два кратки статии
> използвайки транслацията между Хаскел и уравнения на github: iterating.pdf и
> balanced.pdf.

Това дето си го написал не се отнася до предмета на тогавашния спор
и по-добре не търси такава връзка, щото иначе трябва пак обясняване
кое, какво … не си струва.

Няколко бележки по същество, след като прочетох първото изречение
(определението) в началото на balanced.pdf. Привеждам го:

General balanced trees are trees with all internal nodes having
at least one child and all leafs being equidistant from the root.

(1)
Нарекъл си въвежданото понятие „общо равновесно дърво“. Кое се има
предвид да е „общо“ (думата е подчертана и в заглавието)? Ако е това,
че не е двоично, то думата „общо“ е излишна: казва се само „дърво“.

(2)
Според определението от вътрешните възли се иска да имат поне един
наследник. А имаш ли пример за вътрешен възел, който няма наследници?

(3)
Определението споменава „коренът“ (the root). Според мен, тогава
трябва предварително да уточниш, че става дума за не какво да е дърво,
а посадено (поставено, rooted). В математиката, за разлика от
ботаниката, не всяко дърво има корен.

(4)
Терминът „равновесен“ не е много подходящ за понятието, което описваш,
или поне е добре да му се добави някаква уточняваща смисъла дума. Под
„равновесно“ може да се разбира дърво, в което наследниците на всеки
възел имат приблизително равно помежду си тегло, т.е. брой възли.
Такова тълкуване е даже по-естествено, тъй като думата произлиза
именно от „вес“, т.е. тегло. Дърво, равновесно по твоето определение
може да има много гъст храст в едно разклонение и хилав ластар със
само няколко верижно подредени възела в друго, съседно разклонение.
Такова дърво е странно да се разглежда като равновесно.

[Slavomir Kaslev]

2013/12/5 Boyko Bantchev <boy...@gmail.com>

> Обещах преди доста време да напиша блог пост за спора, който водехме, но още
> не съм стигнал до там. Междувременно обаче написах два кратки статии
> използвайки транслацията между Хаскел и уравнения на github: iterating.pdf и
> balanced.pdf.

Това дето си го написал не се отнася до предмета на тогавашния спор
и по-добре не търси такава връзка, щото иначе трябва пак обясняване
кое, какво … не си струва.

Няколко бележки по същество, след като прочетох първото изречение
(определението) в началото на balanced.pdf.  Привеждам го:

    General balanced trees are trees with all internal nodes having
    at least one child and all leafs being equidistant from the root.

(1)
Нарекъл си въвежданото понятие „общо равновесно дърво“.  Кое се има
предвид да е „общо“ (думата е подчертана и в заглавието)?  Ако е това,
че не е двоично, то думата „общо“ е излишна: казва се само „дърво“.

Съгласен съм. "Общо" трябваше да значи, че вътрешните възли могат да

имат произволен брой деца. По аналогия с терминологията на Седжуик

(binary trees for data F a = Leaf а | Node a (F a) (F a), general trees data G a = Node a [G a])).

Ще го променя като измисля нещо по-добро на английски. Какво би предложил? 

 

(2)
Според определението от вътрешните възли се иска да имат поне един
наследник.  А имаш ли пример за вътрешен възел, който няма наследници?

Да. Другия файл iterating.pdf е точно разработка на този случай, т.е.

data F a = F0 a | F1 (F [a])

Генериращата функция в този случай е изключително не-гладка и странна. В

случая на general balanced tree обаче фунцкията е аналитична. Според мен точно

поради забраната на вътрешни възли без деца, която дава "един вид" непрескъснатост

на пътищата от корена до листата.

 

(3)
Определението споменава „коренът“ (the root).  Според мен, тогава
трябва предварително да уточниш, че става дума за не какво да е дърво,
а посадено (поставено, rooted).  В математиката, за разлика от
ботаниката, не всяко дърво има корен.

Седжуик нарича дървета без корен free trees мисля. Доколкото аз знам

жаргона, по-подразбиране "дърво" значи дърво с корен, ако искаш да кажеш

дърво без корен допълваш "свободно дърво".

Но, разбираш, че това как наричаш нещо няма абсолютно никакво значение.

Математическата дефиниция или Хаскел кода е това което определя всичко.

Нещото може да го наричаш както си поискаш, "покипси", "джипси", "бибси",

всичко работи еднакво. Съгласен съм, че името което съм избрал за дървото

може да не оптимално и ще го променя скоро.

 

(4)
Терминът „равновесен“ не е много подходящ за понятието, което описваш,
или поне е добре да му се добави някаква уточняваща смисъла дума.  Под
„равновесно“ може да се разбира дърво, в което наследниците на всеки
възел имат приблизително равно помежду си тегло, т.е. брой възли.
Такова тълкуване е даже по-естествено, тъй като думата произлиза
именно от „вес“, т.е. тегло.  Дърво, равновесно по твоето определение
може да има много гъст храст в едно разклонение и хилав ластар със
само няколко верижно подредени възела в друго, съседно разклонение.
Такова дърво е странно да се разглежда като равновесно.

Отворен съм към идеи. Даже github pull request няма да откажа.

 

--
You received this message because you are subscribed to the Google Groups "Polyglot Quine" group.
To unsubscribe from this group and stop receiving emails from it, send an email to polyglot-quin...@googlegroups.com.
To post to this group, send email to polyglo...@googlegroups.com.
Visit this group at http://groups.google.com/group/polyglot-quine.
For more options, visit https://groups.google.com/groups/opt_out.

--
Slavomir Kaslev

[Boyko Bantchev]

> Съгласен съм. "Общо" трябваше да значи, че вътрешните възли могат да
> имат произволен брой деца. По аналогия с терминологията на Седжуик
> (binary trees for data F a = Leaf а | Node a (F a) (F a), general trees data
> G a = Node a [G a])).
> Ще го променя като измисля нещо по-добро на английски. Какво би предложил?

Както казах – да отпадне думата „общо“. Не е нужно да се добавя нещо
на нейно място.

>> Според определението от вътрешните възли се иска да имат поне един
>> наследник. А имаш ли пример за вътрешен възел, който няма наследници?
> Да. Другия файл iterating.pdf е точно разработка на този случай, т.е.
> data F a = F0 a | F1 (F [a])

Другият файл никъде не говори за дърво, дори думата не споменава,
така че няма да го обсъждаме. За мен, а струва ми се не само за мен,
е неразбираемо какво значи вътрешен възел да няма наследници. Както
го разбирам аз, възел на дърво или няма наследници и се нарича лист,
или има наследници и точно затова се нарича вътрешен. Ако имаш
предвид някакви други понятия, то те не са обичайните и е абсолютно
необходимо да ги обясниш – иначе няма да бъдеш разбран.

> Седжуик нарича дървета без корен free trees мисля. Доколкото аз знам
> жаргона, по-подразбиране "дърво" значи дърво с корен, ако искаш да кажеш
> дърво без корен допълваш "свободно дърво".

Вярно е, че в един или друг контекст под „дърво“ може да се
подразбира дърво с корен, но какво се подразбира наистина зависи
от контекста. С оглед на това за дадения случай ми изглежда
добре да се подразбира минималното, което е и обичайното в
теория на графите: свързан граф без цикли. Че е посадено лесно
се уточнява с една дума в определението: „… is a rooted tree with …“.

> Отворен съм към идеи. Даже github pull request няма да откажа.

Аз бих нарекъл дърво като твоето подравнено. На английски би могло
да е even или height-balanced. Последното дори вече се използва за
същото, но even ми се струва по-сполучливо.

[Slavomir Kaslev]

2013/12/6 Boyko Bantchev <boy...@gmail.com>

> Съгласен съм. "Общо" трябваше да значи, че вътрешните възли могат да
> имат произволен брой деца. По аналогия с терминологията на Седжуик
> (binary trees for data F a = Leaf а | Node a (F a) (F a), general trees data
> G a = Node a [G a])).
> Ще го променя като измисля нещо по-добро на английски. Какво би предложил?

Както казах – да отпадне думата „общо“.  Не е нужно да се добавя нещо
на нейно място.

>> Според определението от вътрешните възли се иска да имат поне един
>> наследник.  А имаш ли пример за вътрешен възел, който няма наследници?
> Да. Другия файл iterating.pdf е точно разработка на този случай, т.е.
> data F a = F0 a | F1 (F [a])

Другият файл никъде не говори за дърво, дори думата не споменава,
така че няма да го обсъждаме.  За мен, а струва ми се не само за мен,
е неразбираемо какво значи вътрешен възел да няма наследници.  Както
го разбирам аз, възел на дърво или няма наследници и се нарича лист,
или има наследници и точно затова се нарича вътрешен.  Ако имаш
предвид някакви други понятия, то те не са обичайните и е абсолютно
необходимо да ги обясниш – иначе няма да бъдеш разбран.

Доколкото разбирам, математиката не ти е силна. За съжаление, няма царски път

към знанието. Единствения начин да разбереш нещо фундаментално е чрез

математическо мислене и прецизност. 

В противен случай си ограничен да виждаш само върха на айсберга без да

разбираш деликатността на нещата в дълбочина.

В науката, дадена област е толкова успешна доколкото теорията е базирана

на математически фундамент. Poster child на това схващане е физиката. Можеш

ли да си преставиш физиката без математика, когато всички открити закони на

природата се описват най-добре от математически уравнения? Не може да пуснеш

сателит в орбита или да кацнеш на Марс без да имаш математически модел за 

орбитите на планетите и механиката на апарата.

Хора като Feynman, Gell-Mann, Dyson могат да бъдат авторитети в дадена област.

Те са положили необходимото усилие, дългогодишната работа, да разберат нещо

в детайл. Хора като теб нямат морално право да бъдат авторитети. Не си свършил

необходимата работа, за да бъдеш експерт в нещо. Ако живота ти е минал в

преписване, преразказване, превеждане и четене на чужди идеи като добър ученик,

ако никога не си имал нито една оригинална идея, не си в позиция да дадеш добра

оценка дали дадена идея си заслужава или не. Хора като теб могат само да размахват

с ръце да използват сложни думи. Файнман го е казал преди по-добре от мен:

Richard Feynman and Pseudoscience.

Опитай се някой мързелив ден в БАН да решиш сам някое уравнение, например

f(x) = x + f(x/(1-x))  или f(x) = x + f(x^2 + 1) или f(x) = x + f(x^2 + x^3). Е така, просто

за удоволствие. Надявам се един ден да проумееш колко плитко познаваш света.

Понеже не разбираш от логични аргументи, ще взема урок от Стефчо Кънев и 

Торвалдс и от този момент нататък ще се огранича само до мръсно тролване. 

Не заслужаваш дори да полагам усилие да ти обясня нещо. Вместо това просто

ще повтарям, че си тъп и грозен на всеки следващ твой негативен пост. Оставяш

ме без избор, единствения начин да комумикираш с ирационални хора е да бъдеш

ирационален като тях.

"Talk is cheap. Show me the code."

 

> Седжуик нарича дървета без корен free trees мисля. Доколкото аз знам
> жаргона, по-подразбиране "дърво" значи дърво с корен, ако искаш да кажеш
> дърво без корен допълваш "свободно дърво".

Вярно е, че в един или друг контекст под „дърво“ може да се
подразбира дърво с корен, но какво се подразбира наистина зависи
от контекста.  С оглед на това за дадения случай ми изглежда
добре да се подразбира минималното, което е и обичайното в
теория на графите: свързан граф без цикли.  Че е посадено лесно
се уточнява с една дума в определението: „… is a rooted tree with …“.

> Отворен съм към идеи. Даже github pull request няма да откажа.

Аз бих нарекъл дърво като твоето подравнено.  На английски би могло
да е even или height-balanced.  Последното дори вече се използва за
същото, но even ми се струва по-сполучливо.

--
You received this message because you are subscribed to the Google Groups "Polyglot Quine" group.
To unsubscribe from this group and stop receiving emails from it, send an email to polyglot-quin...@googlegroups.com.
To post to this group, send email to polyglo...@googlegroups.com.
Visit this group at http://groups.google.com/group/polyglot-quine.
For more options, visit https://groups.google.com/groups/opt_out.

--
Slavomir Kaslev

[Stefan Kanev]

Непропорционално агресивна реакция. Не разбирам защо е нужна.

[Slavomir Kaslev]

Защото ми е писнало от авторитарен тон от човек, който дори няма умението да прочете какво точно съм написал

след първото изречение. Но въпреки това се представя за експерт и има изградено мнение. Когато става дума за

математика, нещата са черни или бели. Няма място за философия, всички философи ги изби Wittgenstein през 50те.

2013/12/7 Stefan Kanev <stefan...@gmail.com>

--
Slavomir Kaslev

[Stefan Kanev]

Защото ми е писнало от авторитарен тон от човек, който дори няма умението да прочете какво точно съм написал

след първото изречение. Но въпреки това се представя за експерт и има изградено мнение. Когато става дума за

математика, нещата са черни или бели. Няма място за философия, всички философи ги изби Wittgenstein през 50те.

Не виждам как това го оправдава.

Също, струва ми се, че смесваш две неща - съдържанието и тона. Сега, аз прегледах двата PDF-а набързо и определено не ги прочетох в детайли, но ми се струва, че Бойко не само ги е прочел, но и е повдигнал няколко съвсем уместни корекции (ключови думи: "струва ми се"). Да кажеш, че няма умението да прочете какво точно си написал е преувеличено и би трябвало да ти е ясно. Също, не виждам къде се представя за експерт. Ако прочетеш пак какво е написал, не мисля, че ще намериш изказване тип "аз ги разбирам тия неща, ти не". По-скоро ми се струва, че това е някаква представа, която ти имаш за него. Определено има изградено мнение по въпроса и определено го изразява. Но всички правим това. Може би той го прави една идея по-уверено от нас и е една идея по-скептичен към нашите идеи, но честно казано, се занимава с това отпреди да сме се родили, така че поне аз лично мога да го разбера. Но дотук става въпрос за тон, а не познания/умения.

И говорейки за тон, нещата вече стават твърде субективни. Ще си позволя да илюстрирам тезата си риторично:

<rhetoric>

Аз например, имам ужасно много забележки към твоя начин на изказ. Например:

• Твърде често, например, правиш Argument by authority (https://yourlogicalfallacyis.com/appeal-to-authority). Ако погледнеш последните си няколко писма, ще откриеш ужасно много name-dropping. Feynman, Wittgenstein и един тон други, които повечето хора в този списък (включително и аз) не сме чели или дори не сме чували.
• "Talk is cheap, show me code" е нахално, още повече когато не спориш от позиция в която ти самия си направил нещо кой знае какво. Бих разбрал да говориш така, ако беше издал книга по въпроса или имаше сериозен OpenSource проект над темата. Уви, и двете не са верни. За сметка на това, GitHub-а ти е пустина. Ако commit message-ите ти първия проект който отворих (https://github.com/skaslev/qi) е пример за това как ползваш version control, или дори как пишеш код (коментари с copy/paste от интерактивна конзола), то не знам къде си тръгнал ти да обясняваш нещо за програмиране (https://yourlogicalfallacyis.com/no-true-scotsman).
• Почти без пропуск успяваш да комбинираш рационален аргумент с лична нападка. Докато аргумента ти може би е смислен, винаги успяваш да вмъкнеш нещо обидно (https://yourlogicalfallacyis.com/ad-hominem). Бахти, толкова ли си неуверен в аргументите си, че трябва да наказваш събеседника си?

Сега, обърни внимание какво наприх с този списък:

• Пратих те да четеш yourlogicallfallacyis.com. Аз самия направих Appeal to authority, макар и малко мета. Можех да се опитам да ти обясня, че докато се възхищавам на общата ти култура и колко много си чел, не мога да разбера аргумента само от името на автора и че ще оценя, ако го изразиш без да правиш външни препратки, така че аз да мога да го разбера. Все пак, ако го разбираш добре, не би трябвало да ти е проблем.
  
• Питах те къде си тръгнал да говориш за код с тоя GitHub. Вероятно това, което си сложил в GitHub далеч не е индикативно за това колко добър програмист си, но тръгвайки да те съдя по аршин който аз си избирам, е много лесно да ти поставя етикета аматьор. Не е съвсем честно да съдиш хората така. Може би qi далеч не е пример за това как правиш commit съобщения. Може би е голяма грешка да си вадя изводи за качеството на работата ти от него.
• Струва ми се, че е очевидно, но все пак - смесих логичните си аргументи защо тона ти е неприятен с нападки ("бахти, толкова ли си неуверен").

С други думи, всеки от елементите от първия списък прави същата грешка, в която те обвинява.

Как те накара това да се почувстваш? Звучи ли ти като разумен аргумент? Ти как би реагирал, ако някой ти говори така?

Дотук с риориката се опитвах да ти илюстрирам и обясня как понякога твоите писания ми изглеждат на мен. Единственото, което липсва, е линк към видео, с което да обидя събеседника. Няма да включа такова дори за илюстрацията, защото не удрям толкова ниско.

</rhetoric>

Горното целеше само илюстрация. Съжалявам, ако тона е бил нападателен/обиден, просто се опитвах да илюстрирам по забавен начин как понякога ми звучат думите ти. По никакъкв начин не искам да влизам в словестна война. Просто искам да ти обърна внимание, че (1) всеки от нас си говори с някакъв тон, (2) ние си избираме дали да се засягаме и (3) когато отговорим както аз ти отговорих в <rhetoric> етикета, едва ли постигаме нещо различно от това да изглеждаме като малки деца в добрия случай и като неадекватни хора в лошия.

[Slavomir Kaslev]

Водих дискусия на същата тема в @math групата в гугъл със съвсем различен резултат. Коментарите бяха

конструктивни, с математически аргументи и много LaTeX из имейлите. В контраст с нивото на (мета-мета-)дискусията

в тази група пълна с глупави философско-лингвистични забележки и без никакво съществено съдържание.

Наказателния ми тон е преднамерен и личен. Нямам толерантност към престорена компентентеност. 

2013/12/7 Stefan Kanev <stefan...@gmail.com>

--
Slavomir Kaslev

[Slavomir Kaslev]

Когато написах преди известно време, че това е грешната група за тази тема, бях прав. Просто исках да се убедя,

за да мога да не повтарям тази грешка отново.

2013/12/7 Slavomir Kaslev <slavomi...@gmail.com>

--
Slavomir Kaslev

[Stefan Kanev]

Всички тези неща са чудесни, но продължавам да не виждам защо смяташ, че поведението ти е оправдано.

Ако темата не е подходяща за групата, просто не пиши тук. Ако си се убедил в нещо, кажи "мерси" и приключи дискусията. Ако групата не ти харесва заради "глупавите философско-лингвистични забележки" и липсата на "съществено съдържание", знаеш как да се отпишеш от нея. Ако нямаш толерантност към нещо, не го толерирай.

Каквато и да е групата, обаче, не е медия в която да "наказваш" хората за неща, в които ги подозираш. Съответно, ще те помоля да не го правиш.

2013/12/7 Slavomir Kaslev <slavomi...@gmail.com>

[Slavomir Kaslev]

Мерси, приключвам дискусията.

2013/12/7 Stefan Kanev <stefan...@gmail.com>

--
Slavomir Kaslev

[cutthroat]

http://curl.haxx.se/mail/etiquette.html#Do_Not_Top_Post

[Boyko Bantchev]

Слави,

Позволил си си да се държиш така, както никой уважаващ себе си форумец
не прави, дори когато е анонимен. Низко е да се опитваш да ме уязвиш
лично, още повече, че нямаш никакви основания.

Досега коментирах написаното от теб напълно добронамерено. Съвсем
учтиво посочих къде виждам недостатъци и това са основателни
забележки. Ако си очаквал възторзи, проблемът е твой. Освен, че
коментарът ми беше добронамерен и без никаква назидателност, каквато
ти се привижда, замисли се над това, че останалите колеги тук дори не
си дават труда да обсъждат „статиите“ ти. Нахвърляш се безобразно на
единствения, който се е опитал да те вземе насериозно.

„Глупавото философстване“ (твои думи) вместо отговори на конкретни
въпроси по темата е изцяло от твоя страна. Същото се отнася и за
назидателното големеене. Няма да коментирам на какво са белег тези
два вида изхвърляне. Само ще кажа, че дотук преднамерено и с известно
усилие се въздъ̀ржах дори да ги споменавам, но е лесно те да се
проследят, и то не само в последните дни.

Изобщо добре е, че написаното остава. В този спор аз няма от какво да
се срамувам, а ти реши за себе си.

[cutthroat]

Курс по HOTT от Роб Харпър.

http://www.cs.cmu.edu/~rwh/courses/hott/

Уводната лекция събужда апетита.

[Slavomir Kaslev]

Яко. Аз намерих видео лекции на сайта на Institute for Advanced Study: https://video.ias.edu/search/site/homotopy . Лекциите са основно от авторите на книгата; някои са от сбирките преди и докато пишат книгата. 

--
Slavomir Kaslev