Расскажите, пожалуйста, про теорию массивов

такие темы только вокруг костра ночью

Массив. Ну…. это массив.

Погугли Theory of arrays.

Там непонятных слов много. Например в чем разница между «The theory of arrays» и «The extensional theory of arrays» ?

Массив. Ну…. это массив.

Это совсем не так. Оказывается было множество научных прорывов:

1962: John McCarthy formalizes arrays as first-order theory TA.
1969: James King describes and implements DP for QFF of TA.
1979: Nelson & Oppen describe combination method for QF theories sharing =.
1980s: Suzuki, Jefferson; Jaffar; Mateti describe DPs for QFF of theories of arrays with predicates for sorted, partitioned, etc.
1997: Levitt describes DP for QFF of extensional theory of arrays in thesis.
2001: Stump, Barrett, Dill, Levitt describe DP for QFF of extensional theory of arrays.
2006: Bradley, Manna, Sipma describe DP for array property fragment of TA, T Z A.

в чем разница между «The theory of arrays» и «The extensional theory of arrays» ?

Наверное в том, что первое, это обобщенное представление, а второе расширенное, так как массивы могут быть разными и многое зависит от реализации, но основа, это индексированная структура данных:

 pwsh $ & {
          $array = 1, "один", $(date +%H:%M:%S)
          'Сколько элементов в $array: {0}' -f $array.Count
          $array[0]
          $array[1]
          $array[2]
          }
Сколько элементов в $array: 3
1
один
11:08:48

Оказывается было множество научных прорывов:

Прорвало эту прорву. )

Ночь приближается. Как я понимаю, рассказывать тебе всё равно нечего.

Между тем, индийские обезьяны МОГУТ: https://www.youtube.com/watch?v=j2RWCnVdGd4

https://llbmc.org/files/papers/SMT12.pdf - вот статья про теорию массивов. Там такие аксиомы есть:

p=r    =>  read(write(a,p,b),r)=v
¬(p=r) =>  read(write(a,p,b),r)=read(a,r)

These axioms state that storing the value v into an array a at index p and subsequently reading a’s value at index q results in the value v if the indices p and q are identical. Otherwise, the write operation does not influence the result of the read operation.

Там еще упоминается такое вот

read : array × index → element
write : array × index × element → array

Т.е. функция чтения должна принимать массив и индекс, возвращая при этом значение по индексу. Можно это как-то так описать на чем-то вроде Си.

element_t read_arr(const array_t arr, const index_t i)
{
  ...
}

а функция записи в массив принимает на вход массив, индекс и записываемое значение, возвращает новый массив с записаным в него значением:

array_t write_arr(const array_t arr, const index_t i, const element_t elm)
{
  ...
}

Функциональщина какая-то

Можно примерно так реализовать:

#include <stdio.h>
#include <stdlib.h>
#include <inttypes.h>

typedef struct array_node
{
  struct array_node *prev;
  size_t i;
  uint32_t elm;
} array_node;

// Добавляем элемент в "массив"
array_node *write_arr(array_node *arr, const size_t i, const uint32_t elm)
{
  array_node *n = malloc(sizeof(array_node));
  if (n == NULL) exit(EXIT_FAILURE);
  *n = (array_node){arr, i, elm};
  return n;
}

// Пролистываем односвязный список до первого совпадения или пока не дойдем до NULL
uint32_t read_arr(array_node *arr, const size_t i)
{
  if (arr == NULL) return 0;
  if (arr->i == i) return arr->elm;
  return read_arr(arr->prev, i);
}

int main(void)
{
  array_node *a = NULL; // NULL тут считается бесконечным массивом, заполненным нулями
  a = write_arr(NULL, 0, 5);
  a = write_arr(a, 1, 10);
  a = write_arr(a, 2, 100500);
  a = write_arr(a, 2, 20);  // элемент по адресу 2 был как бы перезаписан
  a = write_arr(a, 3, 40);
  printf("%" PRIu32 "\n", read_arr(a, 2)); // выведет 20
  return EXIT_SUCCESS;
}

Для чего ты это (код на Си) написал? Тебе оно может и добавляет понимания, а мне - не добавляет.

Когда кто-то где-то упоминает о математической логике, значит в коде программы должны быть метаданные мегатоннами. И язык нужен соответствующий, с RTTI (например C++).

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

Но это всё фигня. Нефигня - объяснить, зачем это всё нужно в принципе.

Для чего ты это (код на Си) написал? Тебе оно может и добавляет понимания, а мне - не добавляет.

А что должно добавить понимания?

Когда кто-то где-то упоминает о математической логике, значит в коде программы должны быть метаданные мегатоннами. И язык нужен соответствующий, с RTTI (например C++).

RTTI это про хранение типов в рантайме, к теории массивов и матлогике это отношения не имеет. Чтобы через теорию массивов что-то статически доказывать (см cтатический анализ кода) относительно свойств программы, никакое RTTI не требуется. Могут потребоваться специальные аннотации, типа ACSL https://frama-c.com/html/acsl.html но это не RTTI

Когда кто-то где-то упоминает о математической логике, значит в коде программы должны быть метаданные мегатоннами.

нет.

И язык нужен соответствующий, с RTTI (например C++).

вообще нет. От слова совсем.

Если есть возможность реализовать алгоритмы разной сложности, надо выбирать с оптимальной сложностью

Оптимальной по какому критерию? Целевую функцию в тред.

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

Внезапно сложность вставки в список O(1) ниже чем сложность вставки в дерево, потому что дерево требует перебалансировки. Сложность произвольного доступа в вектор тоже O(1). Вы о сложности каких именно действий глаголете?

Но это всё фигня. Нефигня - объяснить, зачем это всё нужно в принципе.

Если Вы не понимаете зачем это нужно, то оно очевидно Вам ненужно. Ваш К.О.

Там непонятных слов много.

Потому что Вы не в теме наверное? Но с чсего Вы решили что ЛОР это то место где Вам дадут развернутые ответы на вопросы в которых Вы ничего не понимаете?

Например в чем разница между «The theory of arrays» и «The extensional theory of arrays» ?

extensional же.

Массив дуба бывает например, из него шкафы книжные хорошие получаются. В этих шкафах хорошо смотрятся книжки по теории массивов;-)

Сложность произвольного доступа в вектор тоже O(1).

Если бы ты прочитал предложенный код… Но ты не прочитал, а уже что-то говоришь.

Подсказка - там не вектор.

Я комментирую не код а Ваш нейроразнообразный поток сознания.

Вообще то, насколько я понял, теория массивов это часть математической логики позволяющая доказать средствами математической логики что алгоритм с массивом делает ровно то, что нужно. Вещь как мне кажется в себе - в тривиальных случаях пустая трата времени, в нетривиальных этой темой никто толком не владеет на нужном уровне для практического использования. М.б. есть какие то статические анализаторы кода где это юзается, я ХЗ.

SMT же вообще прекрасная как сферический конь в вакууме. Если SAT сейчас вовсю используют при разных оптимизациях (хотя свести практическую задачу к SAT тот еще гемор), то про успехи SMT я особо не слышал. Ну то есть где то может взлететь, но в общем виде оно чересчур сложное.

Я комментирую не код а Ваш нейроразнообразный поток сознания.

Вы комментируете свои фантазии.

Внезапно сложность вставки в список O(1) ниже чем сложность вставки в дерево
Сложность произвольного доступа в вектор тоже O(1).

Это Вы взяли из ваших фантазий. Формально все верно, только обсуждаемый код это односвязный список, и сложность поиска в нём O(N), что выше чем O(log(N)) при поиске в дереве.

Вы о сложности каких именно действий глаголете?

Я Вам ответил, я говорю о сложности действий, запрограммированных в представленном примере.

Мой поток создания адекватен контексту, а Ваш - нет. Но я понимаю, что только умные люди могут признать свою ошибку, лень или невнимательность.

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

обсуждаемый код это односвязный список, и сложность поиска в нём O(N), что выше чем O(log(N)) при поиске в дереве.

Сложность поиска обусловлена структурой данных, а структура данных подбирается с учётом многих факторов, которые в примере могут быть не показаны. Это пример а не боевой код.

Впрочем Вы как обычно за свои слова не отвечаете, что с Вас взять… успехов в «познании» теории массивов, продолжайте веселить народ.

насколько я понял

Судя по этим словам, Вы про эту тему вообще только что узнали.

оно чересчур сложное

Но не осилили.

Когда кто-то где-то упоминает о математической логике, значит в коде программы должны быть метаданные мегатоннами. И язык нужен соответствующий, с RTTI (например C++).

Это можно в мемориз, как пример наукообразного бреда от нейроразнообразного существа наслушавшегося красивых и непонятных слов. Попугаи и скворцы ведут себя примерно так же.

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

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

Но не осилили.

Но это всё фигня. Нефигня - объяснить, зачем это всё нужно в принципе.

Бугагашечки, что еще тут сказать…

Если вы о теме только что узнали, то Ваш уровень - новичок (джун). Такого не нужно стесняться.

Еще одно 4.2. Интересно, Вы вообще в принципе способны хотя бы раз выдать утверждение имеющее хоть какое то отношение к действительности?

Хотя…

Мой поток создания адекватен контексту

Это тоже в мемориз.

Так что, собственно, такое теория массивов, о которой вы второй день срётесь?

Пока выяснить это не удалось. Некоторые с умным видом говорят слова SAT и SMT, но как это работает, они объяснить не могут (вероятно потому что сами не понимают). Или, там DPLL(T).

теория массивов это часть математической логики, позволяющая доказать средствами математической логики что алгоритм с массивом делает ровно то, что нужно.

ЗЫ одна из первых ссылок по запросу «теория массивов математическая логика».

https://mk.cs.msu.ru/images/archive/d/d1/20190421171710%21Mathlog_318_lecture_12.pdf

А складывать эти ваши массивы можно, то есть определена ли над ними операция сложения?

Божечки, ну это такие мелочи. Если не определена - возьми да определи.

Расскажите, пожалуйста про теорию массивов.

Учитесь перемножать матрицы!

Но как это сделать правильно? А то вдруг получится, что сложение - это обратимая операция, и из суммы и одного слагаемого можно будет получить другое слагаемое.

Ой вэй, а ведь сложение строк некоммутативно, а строка это тот же массив! Боюсь что солнце завтра не взойдет…

алгоритм с массивом делает ровно то, что нужно.
делает ровно то, что нужно.

Вы дважды повторили эту фразу. Это показывает, что именно в этом месте у вас в мозгу «щелкнуло» и снизошло какое-то озарение. Но высокий вес именно этой нейросвязи именно у вас никак не говорит, что это что-то важное в целом для человечества.

Повторение акцентирует внимание на чём-то, но не даёт понимания.

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

Повторять одно и то же - не поможет пониманию другими людьми.

сложение строк некоммутативно

При чём тут некоммутативность, когда вопрос был про обратимость (другое свойство)?

Вы однозначно не можете быть сеньёром. Умение объяснять - важный для них навык.

Ой, Вы кроме неумения ванговать и базовых вещей в ИТ еще и в преподавании ничего не понимаете? Ну надо же какая Вы разностронне неразвитая личность, можно сказать феномен!

Повторять одно и то же - не поможет пониманию другими людьми.

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

ЗЫ но, каюсь - меня забавляет Ваш баттхерт.

Мой поток создания адекватен контексту

Это тоже в мемориз

Очевидная опечатка (создания -> сознания). Но я способен признать ошибку.

Так или иначе, пока никто не написал ни определения, ни обоснования нужности (значимости).

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

И это странно, если такой раздел есть в курсе матлогики из МГУ.

Базовая теория массивов позволяет нам моделировать массивы и операции над ними, включая чтение и запись элементов. Она обеспечивает средства для определения и работы с массивами в рамках математической логики.

Расширенная теория массивов, с другой стороны, добавляет дополнительные аксиомы, которые обеспечивают «extensionality» или «расширяемость» массивов. Согласно принципу extensionality, два массива считаются равными, если они имеют одинаковые значения для всех соответствующих индексов. Это позволяет формально моделировать и рассматривать операции и свойства, которые требуют сравнения массивов.

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

И тут я решил, что сложение строк коммутативно. Выкатывай Солнце обратно!

ab + c = b
c + ab = b

Ну кто же изложит теорию массивов. Жду жду, а тут сплошное кидание какашками.

Хочешь чтобы что-то было сделано хорошо - сделай это сам…

А то, вон, Wizard_ запостил ответ ChatGPT, но там такаая фигня!

Например:

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

Есть мне и что ответить на ненужность RTTI, но пока не пришло время.

А индексная арифметика при реализации многомерных массивов куда относится? Всякие Z-кривые Мортона и пр способы обхода.

Z-кривая была введена в 1966 году Гаем Макдональдом Мортоном
кривая Лебега была изучена французским математиком Анри Лебегом в 1904 году

В чём между ними разница, и если разницы нет, то где уважение к научному первенству? Плохо учиться по википедии…

Мортон предложил эффективную индексную арифметику для Z-кривой, поэтому в программировании Z-кривую обычно называют его именем. Хотя саму кривую придумал конечно не он.

Плохо учиться по википедии…

Сочувствую, но в Вашем случае дело не в Википедии.

предложил эффективную индексную арифметику для Z-кривой

Ему просто повезло, что в компьютерах двоичная система счисления. Была бы троичная - хрен бы он что предложил…

Вы путаете алгоритм с особенностями его реализации.