LINUX.ORG.RU

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

 , ,


0

2

Читал страницу
https://ru.wikipedia.org/wiki/Задача_выполнимости_формул_в_теориях
там написано
«SMT включает также теории массивов и списков (часто используемые для моделирования и верификации программ)»

Ничего не понял. Расскажите, пожалуйста про теорию массивов.

Ответ на: комментарий от symon2014

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

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

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.

Shushundr ★★★
() автор топика
Ответ на: комментарий от Shushundr

в чем разница между «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

dmitry237 ★★★★
()
Ответ на: комментарий от safocl

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

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

Shushundr ★★★
() автор топика
Последнее исправление: Shushundr (всего исправлений: 1)

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.

SZT ★★★★★
()
Ответ на: комментарий от SZT

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

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;
}
SZT ★★★★★
()
Ответ на: комментарий от SZT

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

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

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

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

Shushundr ★★★
() автор топика
Ответ на: комментарий от Shushundr

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

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

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

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

SZT ★★★★★
()
Последнее исправление: SZT (всего исправлений: 2)
Ответ на: комментарий от Shushundr

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

нет.

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

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

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

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

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

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

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

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

AntonI ★★★★★
()
Последнее исправление: AntonI (всего исправлений: 1)
Ответ на: комментарий от Shushundr

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

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

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

extensional же.

AntonI ★★★★★
()
Ответ на: комментарий от symon2014

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

AntonI ★★★★★
()
Последнее исправление: AntonI (всего исправлений: 1)
Ответ на: комментарий от AntonI

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

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

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

Shushundr ★★★
() автор топика
Последнее исправление: Shushundr (всего исправлений: 1)
Ответ на: комментарий от SZT

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

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

AntonI ★★★★★
()
Последнее исправление: AntonI (всего исправлений: 1)
Ответ на: комментарий от AntonI

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

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

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

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

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

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

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

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

Shushundr ★★★
() автор топика
Последнее исправление: Shushundr (всего исправлений: 2)
Ответ на: комментарий от Shushundr

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

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

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

AntonI ★★★★★
()
Ответ на: комментарий от Shushundr

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

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

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

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

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

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

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

AntonI ★★★★★
()
Последнее исправление: AntonI (всего исправлений: 1)
Ответ на: комментарий от Shushundr

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

Хотя…

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

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

AntonI ★★★★★
()
Последнее исправление: AntonI (всего исправлений: 1)
Ответ на: комментарий от bo4ok

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

Shushundr ★★★
() автор топика
Ответ на: комментарий от bo4ok

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

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

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

AntonI ★★★★★
()
Последнее исправление: AntonI (всего исправлений: 1)
Ответ на: комментарий от AntonI

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

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

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

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

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

Shushundr ★★★
() автор топика
Последнее исправление: Shushundr (всего исправлений: 1)
Ответ на: комментарий от AntonI

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

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

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

Shushundr ★★★
() автор топика
Ответ на: комментарий от Shushundr

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

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

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

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

AntonI ★★★★★
()
Последнее исправление: AntonI (всего исправлений: 1)
Ответ на: комментарий от AntonI

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

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

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

Shushundr ★★★
() автор топика
Последнее исправление: Shushundr (всего исправлений: 2)

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

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

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

Shushundr ★★★
() автор топика
Последнее исправление: Shushundr (всего исправлений: 1)
Ответ на: комментарий от Shushundr

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

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

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

Wizard_ ★★★★★
()
Ответ на: комментарий от Psilocybe

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

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

Например:

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

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

Shushundr ★★★
() автор топика
Последнее исправление: Shushundr (всего исправлений: 2)
Ответ на: комментарий от AntonI

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

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

Shushundr ★★★
() автор топика
Ответ на: комментарий от Shushundr

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

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

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

AntonI ★★★★★
()
Ответ на: комментарий от AntonI

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

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

Shushundr ★★★
() автор топика