Тьюринг-полон ли данный язык

[arseniiv]

Может, потому что этот язык императивный, они решили не делать?

Кстати, бесконечные объекты в тех языках вроде бы обычно задаются генераторами? А здесь можно было бы сделать дополнительные «объекты» для них, у которых переопределены операции. Например, целочисленное множество, пересечённое с $\mathbb Z$, будет давать себя, при объединении — $\mathbb Z$, а при вычитании $\mathbb Z \setminus A$ даст специальный объект-разность. Свойства операций будут определять поведение таких объектов, и все дела. Скорее всего, такой способ тоже где-нибудь используется.

А вот в языке с одними только множествами вроде так просто не получится (или получится?), потому что нужно ещё счётные объединения/пересечения как-то сделать; что-то делать также с аксиомой выбора.

[_hum_]

А почему не пойти до конца и полностью не попробовать реализовть формальную теорию множеств, которая позволяет выразить через множества любой мат. объект, в том числе и функции (а значит, и алгоритмы)? :)

P.S. Кстати, вроде достаточно $\in, \subset, \cap, \cup$, двух базовых множеств - $\oslash, \infty$ и возможности исчисления логических предикатов, чтобы все остальное (по кр. мере дискретную математику) задать.

[Circiter]

2arseniiv

Цитата:

Кстати, бесконечные объекты в тех языках вроде бы обычно задаются генераторами?

Наверное и так можно (yield?). Изначально я представлял себе рекурсивные типы + ленивые вычисления.

Цитата:

А вот в языке с одними только множествами вроде так просто не получится

О как удобно иметь понятие "функция" в языке программирования. :) Похоже, что отождествление множества и его индикаторной функции решает все проблемы. Просто как-то это надо утопить в деталях реализации и пользователю не показывать...

Цитата:

что-то делать также с аксиомой выбора.

Там живут драконы... А нельзя ли её полностью игнорировать? Например, если какая-то функция будет выплевывать непустые множества, а мы будем строить из них декартово произведение, то можно считать (гарантировать), с аппеляцией к очевидности, что результат будет непустым. Т.е., в некоторых случаях действие аксиомы выбора будет проявляться само-собой... Могу и ошибаться; поэтому если у вас есть какие-нибудь соображения по этой проблеме -- был бы рад послушать.

Мне кажется, что генераторный или рекурсивно-ленивый подход определения бесконечных множеств естественным образом распространяет свойсва конечных множеств на бесконечные. Но можно попробовать и как-нибудь обходить аксиому выбора, примерно также, как её пытаются обходить математики в своих доказательствах. Например, можно при выборе элементов из множеств делать это через отношение порядка или ещё как-нибудь в явном виде. Наверное, это ограничивает декларативный потенциал языка, но само по себе все это очень интересно. Представил себе предупреждение компилятора, "banach_tarski.s1, at line 23, warning: declaration require the axiom of choice.". :)

____________________

Можно ещё какие-нибудь фичи в ваш язык надобавлять, например, из декларативного программирования. Вот интересная идея: J.Cai, R.Paige, Program Derivation by Fixed Point Computation.

В общем, не хотелось бы, чтобы вы забросили это замечательное начинание.

(Оффтоп)

Готов всячески поучаствовать в написании инфраструктуры парсера/компилятора. :) Есть небольшой опыт конструирования простых (студенческих) интерпретаторов $\lambda$ и forth'а, а также x86 компиляторов тех же диалектов (для $\lambda$-кода есть ещё secd-vm; форт-машина же сейчас преписывается на классический лад, т.е. в виде самостоятельной ОС) + компилятор подмножества C (кодогенератор как для vm, так и для железа); для углубления знаний ecmascript (js) пишу самодельный jit-движок (непортабельный, с генерацией нативного x86-кода для скорости). Вдруг пригожусь. :)

2_hum_

Цитата:

Кстати, вроде достаточно $\in, \subset, \cap, \cup$, двух базовых множеств - $\oslash, \infty$ и возможности исчисления логических предикатов

Похоже, что достаточно лишь "исчисления логических предикатов" или лишь теор-множественных объектов/операций. Потому что одно можно определить через другое. (?)

(Оффтоп)

$\oslash\ \to\ \varnothing$

[arseniiv]

Circiter в сообщении #479609 писал(а):

В общем, не хотелось бы, чтобы вы забросили это замечательное начинание.

Увы, кажется, я его забросил. (Может, на время? Не знаю.)

В генераторном подходе меня волнует то, что (1) мы так можем представить только счётные множества и (2) а если представлять несчётные, то порядок выдавания элементов «важен» (не знаю, как выразить конкретнее: то счётное подмножество, которое перечисляется, влияет на результат операций, в зависимости от способа перечисления могут получиться разные вещи (или нет?)).

[Lukin]

arseniiv в сообщении #349560 писал(а):

Они же не сойдут! Смотрите:

1. []                     (0) 
2. [[]]                 (1) 
3. [[[]]]             (2) 
4. [[], [[]]] 
5. [[[[]]]]         (3) 
6. [[], [[[]]]] 
7. [[[]], [[[]]]] 
8. [[], [[]], [[[]]]] 
9. [[[], [[]]]] 
10. [[], [[], [[]]]] 
11. [[[]], [[], [[]]]] 
12. [[], [[]], [[], [[]]]] 
13. [[[[]]], [[], [[]]]] 
14. [[], [[[]]], [[], [[]]]] 
15. [[[]], [[[]]], [[], [[]]]] 
16. [[], [[]], [[[]]], [[], [[]]]] 

— вот все множества ранга не больше 3. Не думаю, что будет удобно с ними управляться при помощи битовой шкалы/стро
ки.

А можно генерирующий код посмотреть
Интересует время построения всех множеств ранга 4.

[arseniiv]

Нету, да и именно код построения всех множеств одного ранга не задумывался к реализации (зачем он языку?).

-- Пт сен 02, 2011 20:28:20 --

Хотя алгоритм легко описывается. Думаю, вы без труда его получите.

[Circiter]

2Lukin
Cf. правильные скобочные последовательности.

[_hum_]

Circiter в сообщении #479609 писал(а):

2_hum_

Цитата:

Кстати, вроде достаточно $\in, \subset, \cap, \cup$, двух базовых множеств - $\oslash, \infty$ и возможности исчисления логических предикатов

Похоже, что достаточно лишь "исчисления логических предикатов" или лишь теор-множественных объектов/операций. Потому что одно можно определить через другое. (?)

Похоже, все-таки нельзя. Все те теории множеств, что я видел, опираются на исчисление предикатов.

[arseniiv]

Хотя вот она, в общем-то, формула (алгоритм из неё легко получается):

$$S_{n+1} = \left\{ U \cup V \left|\, U \in 2^{S_n} \wedge U \ne \varnothing \wedge V \in 2^{\bigcup_{i = 0}^{n - 1} S_i} \right.\right\}$$

где $S_n$ — множество множеств ранга $n$; $S_0 = \{\varnothing\}$.

[Circiter]

2arseniiv
А как быть с бесконечностью множеств одного ранга. Ну смотрите: [[]], [[],[]], [[],[],[]] -- у всех ранг 1, а количество их неограничено. :)

Набросок псевдокода:

f(level)
{
    if(level==4) return "()";
    s="";
    while(1)
    {
        s+="("+f(level+1)+")";
        yield s;
        s+=", ";
    }
}

f(0);

[Lukin]

arseniiv в сообщении #479766 писал(а):

Хотя вот она, в общем-то, формула (алгоритм из неё легко получается):

$$S_{n+1} = \left\{ U \cup V \left|\, U \in 2^{S_n} \wedge U \ne \varnothing \wedge V \in 2^{\bigcup_{i = 0}^{n - 1} S_i} \right.\right\}$$

где $S_n$ — множество множеств ранга $n$; $S_0 = \{\varnothing\}$.

Получилось громоздко и Очень медленно.
Нумерация начинается с $[]$, новые множества строятся рекурсивно (операцией взятия в скобки и объединения), по списку уже построенных и добавлением в этот же список. При построении каждому множеству приписывается номер и ранг. При построении следующих множеств берутся только множества ранга меньше или равно $3$ из предыдущих строк. Проблема в многократной прогонке основной функции по ранее построенному списку. Избежать этого не удалось. Деревья не проходят, т.к. растут не синхронно. Число множеств с ростом ранга растет убийственно быстро.

-- 02.09.2011, 18:11 --

Circiter в сообщении #479764 писал(а):

2Lukin
Cf. правильные скобочные последовательности.

Спасибо, но это ответ на другой вопрос.

[Circiter]

2Lukin
А зачем вам вообще их строить-то? Я вот вообще непонимаю, чем количество множеств одного ранга ограничено. Множеств нулевого ранга всего одно, первого -- уже бесконечность. Или я просто заблуждаюсь?

Цитата:

Спасибо, но это ответ на другой вопрос.

Я имел ввиду, что обсуждаемые выражения описываются грамматикой expr ::= [s], s ::= $\definecolor{xgreen}{HTML}{008000}\color{xgreen}\varepsilon$ | '[' s ']' | [s] ',' s. И мы можем выводить цепочки, случайным образом выбирая и примения очередное правило вывода если оно не приводит к переполнению ранга.

[arseniiv]

Circiter в сообщении #479767 писал(а):

Ну смотрите: [[]], [[],[]], [[],[],[]] -- у всех ранг 1, а количество их неограничено. :)

Но ведь как множества они равны.

-- Пт сен 02, 2011 21:31:26 --

Хотя о языке чистых списков я тоже думал.

-- Пт сен 02, 2011 21:33:47 --

В какой-то другой теме я даже спрашивал про формулу количества множеств одного ранга, а потом вывел (или вывел только рекуррентное соотношение, подобное составленному для множеств?). Оказалось, её разности есть в OEIS.

[Circiter]

2arseniiv

Цитата:

Но ведь как множества они равны.

А, понятно.

[Circiter]

Для настоящих множеств меня что-то совсем заклинило. Формулу arseniiv'а не понял, свою -- не вывел. :) Рассуждения такие были (для количеств). Обозначим количество множеств ранга $i$ через $N(i)$. Известно, что $N(0)=1$. Множество ранга $n$ должно содержать любое непустое подмножество из семейства множеств ранга $n-1$ и любое (возможно, пустое) подмножество семейства множеств ещё меньшего ранга $i<n-1$. Отсюда рекуррентное определение:

$$N(n+1)=\big(2^{N(n)}-1\big)\cdot\prod_{i=0}^{n-1}2^{N(i)}.$$

Похоже, что это вполне соответствует формуле для $S_n$...

Как его вычислять и тем более как эффективно генерировать соответствующие цепочки -- мне пока непонятно...

-- Сб сен 03, 2011 00:23:27 --

2_hum_

Цитата:

Похоже, все-таки нельзя. Все те теории множеств, что я видел, опираются на исчисление предикатов.

То есть вы считатете, что $\in,\subset,\cap,\cup,\varnothing,\infty$ недостаточно для построения вычислительного формализма? Я, честно-говоря, запутался, и с удовольствием послушаю, как же все есть на самом деле. Вот например, раз у нас есть $\subset$ (а лучше $\subseteq$) то нам не нужен квантор $\forall$... Или нет? (Вопрос в стиле arseniiv'а :) )

2arseniiv
А как вы собирались назвать свой язык? Вот я там выше файлик с воображаемым исходником от-фонаря назвал banach_tarski.s1, так может быть в качестве кодового рабочего названия пока S1 сгодится? :)