Сужение наборов алгебраических значений

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

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

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

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

История

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

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

Отложенное вычисление — важная особенность современных функциональных языков программирования, таких как Haskell . Haskell — последний из серии языков, основанных на лямбда-исчислении и let-выражениях . Эти языки обеспечивают богатую функциональность за счет отложенных вычислений и полиморфную систему типов, использующую вывод типов . Функциональные языки программирования также естественным образом поддерживают функции высшего порядка .

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

Языки логического программирования, хотя и обладают большими способностями к дедукции, никогда не обладали мощью и гибкостью функциональных языков.

Сужение — это метод, позволяющий осуществлять логический вывод с гибкостью функциональных языков.

Введение

В математике выражение представляет одно значение. Функция сопоставляет одно или несколько значений одному уникальному значению.

Обратные функции не всегда четко определяются как функции. Иногда требуются дополнительные условия, чтобы обратная функция соответствовала определению функции.

Некоторые логические операции, в частности, не имеют обратных операций, которые можно определить как функции. В частности, дизъюнкция «или» имеет обратные значения, допускающие два значения. В естественном языке «или» представляет альтернативные возможности.

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

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

Возможные миры принадлежат множествам миров. Набор миров — это набор всех взаимоисключающих миров. Объединение значений из разных возможных миров невозможно, потому что это означало бы объединение взаимоисключающих возможных миров.

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

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

Введение в наборы значений

Набор значений — это объект, который представляет набор значений, которые может иметь переменная. Набор значений математически ведет себя как одно значение, но внутренне представляет несколько значений. Для достижения этого набор значений отслеживает значения вместе с контекстом или миром, в котором они произошли.

Множественные решения уравнения

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

$x^{2}=4$

что подразумевает,

$x=2\lor x=-2$

Но это немного запутанно и не позволяет нам работать с несколькими значениями одновременно. Если к x добавляются дополнительные условия или ограничения, мы хотели бы рассмотреть каждое значение, чтобы увидеть, соответствует ли оно ограничению. Так наивно нам хотелось бы написать,

$x=\pm 2$

Тогда наивно,

$x+x\in \lbrace 4,0,-4\rbrace$

но это неправильно. Каждый x должен представлять одно значение в выражении. Либо x равно 2, либо x = −2. Эту проблему можно решить, отслеживая два значения, чтобы гарантировать, что значения используются последовательно, и именно это и делает набор значений.

Представительство

Значение, установленное для «x», записывается как:

$V(\{2::x_{1},-2::x_{2}\})$

Это контейнер V, который имеет набор пар тегов, значений,

• $2::x_{1}$
• $-2::x_{2}$

Значение 2 связано с возможным миром $x_{1}$. Значение −2 связано с возможным миром $x_{2}$. Это означает, что значение не может быть одновременно 2 и −2. В мире $x_{1}$ значение набора значений должно быть равно 2. В мире $x_{2}$ значение набора значений должно быть -2.

Решение уравнения,

$x^{2}=4$

является,

$x=V(\{2::x_{1},-2::x_{2}\})$

Возможные миры

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

Термин «возможный мир» используется для облегчения понимания описания наборов значений.

Мировые наборы

Набор миров — это набор возможных миров, которые представляют все возможности. Так $\{x_{1},x_{2}\}$ — это мир, заданный как x = 2 (в мире $x_{1}$) или x= −2 (в мире $x_{2}$). Других возможностей нет.

Миры из одного и того же набора миров являются взаимоисключающими, поэтому не возможно, чтобы предложения для обоих миров были взаимоисключающими. $x_{1}$ и $x_{2}$ верны одновременно.

$(x=2\land x=-2)={\text{false}}$

Применение функций

Правило применения функций к наборам значений таково:

$V(M)\ V(N)=V(\{(m_{v}\ n_{v},m_{l}\cap n_{l}):m_{v}::m_{l}\in M\land n_{v}::n_{l}\in N\})$

Например,

$x+x=V(\{2::x_{1},-2::x_{2}\})+V(\{2::x_{1},-2::x_{2}\})$

является,

$=V(\{-2+-2::x_{1}\cap x_{1},-2+2::x_{1}\cap x_{2},2+-2::x_{1}\cap x_{2},2+2::x_{2}\})$

$=V(\{-4::x_{1}\cap x_{1},0::x_{1}\cap x_{2},0::x_{2}\land x_{1},2+2::x_{2}\cap x_{1}\})$

Пересечение возможного мира с самим собой есть возможный мир,

$x_{1}\cap x_{1}=x_{1}$

$x_{2}\cap x_{2}=x_{2}$

Пересечение возможного мира с другим возможным миром из того же множества миров пусто,

$x_{1}\cap x_{2}=\{\}$

$x_{2}\cap x_{1}=\{\}$

Так,

$=V(\{-4::x_{1},0::\{\},0::\{\},4::x_{2}\})$

Правило пустых миров позволяет удалять отмеченные значения из пустых миров.

$V(K)=V(\{(v,l):(v,l)\in K\land l\neq \{\}\}$

предоставление,

$=V(\{-4::x_{1},4::x_{2}\})$

Давая результат, который $x+x$ равно либо −4, либо 4, как и ожидалось.

Применение к логическим значениям

$a\land b$

Это связь между a , b и true , которая подразумевает, что и a, и b должны быть истинными.

$a\lor b$

Допускает несколько значений для a и b . Если есть ,

$a=V(\{\operatorname {false} ::a_{1},\operatorname {true} ::a_{2}\})$

тогда для б

$b=V(\{\operatorname {true} ::a_{1},\operatorname {false} ::a_{2},\operatorname {true} ::a_{2}\})$

Это означает, что если a ложно , то b должно быть истинным .

Теперь рассмотрим,

$x=2\lor x=-2$

дает,

$x=V(\{\_::a_{1},2::a_{2}\})$

и

$x=V(\{-2::a_{1},\_::a_{2},-2::a_{2}\})$

объединение этих двух наборов значений дает:

$x=V(\{-2::a_{1},2::a_{2}\})$

Пара $-2::a_{2}$ удаляется из-за правила «утверждать равное»,

$\forall m_{v}\forall m_{l}\forall n_{v}\forall n_{l}((m_{v},m_{l})\in M\land (n_{v},n_{l})\in N)\to (m_{v}\neq n_{v}\to m_{l}\cap n_{l}=\{\})$

Его ценность $-2::a_{2}$ не совпало с $2::a_{2}$.

Зависимые миры

Рассмотрим проблему,

$X=V(\{1::x_{1},3::x_{2},4::x_{3}\})$

$Y=V(\{8::y_{1},9::y_{2}\})$

$X*Y<25$

$X+Y>10$

Сначала рассчитайте значение, установленное для $X*Y<25$,

$V(\{8::x_{1}\cap y_{1},24::x_{2}\cap y_{1},32::x_{3}\cap y_{1},9::x_{1}\cap y_{2},27::x_{2}\cap y_{2},36::x_{3}\cap y_{2}\})<25$

$V(\{8<25::x_{1}\cap y_{1},24<25::x_{2}\cap y_{1},32<25::x_{3}\cap y_{1},9<25::x_{1}\cap y_{2},27<25::x_{2}\cap y_{2},36<25::x_{3}\cap y_{2}\})<25$

$V(\{{\text{true}}::x_{1}\cap y_{1},{\text{true}}::x_{2}\cap y_{1},{\text{false}}::x_{3}\cap y_{1},{\text{true}}::x_{1}\cap y_{2},{\text{false}}::x_{2}\cap y_{2},{\text{false}}::x_{3}\cap y_{2}\})$

Поскольку это утверждение считается истинным, все ложные значения отбрасываются, что дает:

$V(\{{\text{true}}::x_{1}\cap y_{1},{\text{true}}::x_{2}\cap y_{2},{\text{true}}::x_{1}\cap y_{2}\})$

Миры,

$x_{3}\cap y_{1}$

$x_{2}\cap y_{2}$

$x_{3}\cap y_{2}$

невозможны. Миры пусты.

Если набор миров включен в расчет, то каждый мир из набора миров должен быть включен в результат. Если мир не найден, он называется зависимым миром и должен быть пустым. Мир $X_{3}$ не представлен в этом значении и поэтому должен быть пустым. Значение, установленное для $X$ теперь меньше,

$X=V(\{1::x_{1},3::x_{2}\})$

Второе условие теперь стало проще из-за меньшего набора значений.

$X+Y>10$

Тогда наборы значений будут такими:

$X=V(\{1::x_{1},3::x_{2}\})$

$Y=V(\{8::y_{1},9::y_{2}\})$

И расчет такой:

$V(\{1+8::x_{1}\cap y_{1},3+8::x_{2}\cap y_{1},2+9::x_{1}\cap y_{2},1+9::x_{2}\cap y_{2}\})>10$

Но $x_{2}\cap y_{2}$ пусто. Так,

$V(\{9>10::x_{1}\cap y_{1},11>10::x_{2}\cap y_{1},10>10::x_{1}\cap y_{2}\})$

Так $x_{1}\cap y_{1}$ и $x_{1}\cap y_{2}$ пусты,

$V(\{11>10::x_{2}\cap y_{1}\})$

Сейчас $X_{1}$ и $Y_{2}$ не представлены и удалены как зависимые миры. Так,

$X=V(\{3::x_{2}\})=3$

$Y=V(\{8::y_{1}\})=8$

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

Пицца, пиво, виски

После тяжелого рабочего дня в попытках уложиться в какой-то сумасшедший срок с адским проектом, в 22:00 наступает то отчаянное время, когда нам всем нужна пицца, пиво и виски. Пиццерии открыты по адресу:

${\text{PizzaShop}}(V(\{{\text{Carlton}}::p_{1},{\text{Richmond}}::p_{2},{\text{South Melbourne}}::p_{3},{\text{Footscray}}::p_{4},{\text{St Kilda}}::p_{5},{\text{Toorak}}::p_{6}\}))$

Пиво, которое ты можешь получить,

${\text{BottleshopWithBeer}}(V(\{{\text{South Melbourne}}::b_{1},{\text{St Kilda}}::b_{2},{\text{Carlton}}::b_{3},{\text{Docklands}}::b_{4}\}))$

Виски,

${\text{BottleshopWithWhiskey}}(V(\{{\text{Essendon}}::w_{1},{\text{South Melbourne}}::w_{2}\}))$

Копы рядом, а мы не становимся моложе. Куда пойти?

${\text{WhereToGo}}(x)={\text{PizzaShop}}(x)\land {\text{BottleshopWithBeer}}(x)\land {\text{BottleshopWithWhiskey}}(x)$

Если ограничения применяются в порядке слева направо ,

$x=V(\{{\text{Carlton}}::p_{1},{\text{Richmond}}::p_{2},{\text{South Melbourne}}::p_{3},{\text{Footscray}}::p_{4},{\text{St Kilda}}::p_{5},{\text{Toorak}}::p_{6}\})$

Тогда нам нужно объединить это с,

$x=V(\{{\text{South Melbourne}}::b_{1},{\text{St Kilda}}::b_{2},{\text{Carlton}}::b_{3},{\text{Docklands}}::b_{4}\})$

Это создаст 24 комбинации, из которых будут совпадающие,

$x=V(\{{\text{South Melbourne}}::b_{1}\cap p_{3},{\text{St Kilda}}::b_{2}\cap p_{5},{\text{Carlton}}::b_{3}\cap p_{1}\})$

Наконец, нам нужно объединиться с виски.

$x=V(\{{\text{Essendon}}::w_{1},{\text{South Melbourne}}::w_{2}\})$

Что дает 6 комбинаций. Соответствующий,

$x=V(\{{\text{South Melbourne}}::b_{1}\cap p_{3}\cap w_{2}\})$

Всего было создано 30 комбинаций.

Если ограничения применяются в порядке справа налево ,

$x=V(\{{\text{Essendon}}::w_{1},{\text{South Melbourne}}::w_{2}\})$

Тогда нам нужно объединить это с,

$x=V(\{{\text{South Melbourne}}::b_{1},{\text{St Kilda}}::b_{2},{\text{Carlton}}::b_{3},{\text{Docklands}}::b_{4}\})$

Это создаст 8 комбинаций, из которых совпадающая будет:

$x=V(\{{\text{South Melbourne}}::b_{1}\cap w_{2}\})$

Наконец, нам нужно объединиться с пиццей.

$x=\{{\text{Carlton}}::p_{1},{\text{Richmond}}::p_{2},{\text{South Melbourne}}::p_{3},{\text{Footscray}}::p_{4},{\text{St Kilda}}::p_{5},{\text{Toorak}}::p_{6}\}$

Что дает 6 комбинаций. Соответствующий,

$x=V(\{{\text{South Melbourne}}::b_{1}\cap w_{2}\ \cap p_{3}\})$

Результат тот же, но для получения вывода было создано всего 14 комбинаций.

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

Пусть выражения и несколько значений

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

$\operatorname {let} x\in X\operatorname {in} x$

В этом выражении $x\in X$ является ограничением. Ограничение — это логическое выражение, которому должна удовлетворять переменная. Выражение let позволяет представить ограничение в выражении. Если бы существовало общее правило применения функций выражений ограничений, то ограничение можно было бы рассматривать как значение.

При применении функции одного выражения let к другому,

$(\operatorname {let} x\in X\operatorname {in} x)\ (\operatorname {let} y\in Y\operatorname {in} y)$

$=\operatorname {let} x\in X\land y\in Y\operatorname {in} x\ y$

$=\operatorname {let} (x,y)\in X\times Y\operatorname {in} x\ y$

Но для применения выражения let к самому себе применяется другое правило. Выражение let не ограничивает область действия переменной x, поэтому x является одной и той же переменной в двух выражениях let.

$(\operatorname {let} x\in X\operatorname {in} x)\ (\operatorname {let} x\in X\operatorname {in} x)$

$=\operatorname {let} x\in X\operatorname {in} x\ x$

Кажется, не существует простого правила для объединения выражений let. Требуется общая форма выражения, представляющая переменную, значение которой является членом набора значений. Выражение должно быть основано на переменной и наборе.

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

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

Теория множеств ценностей

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

Функция состояния определяется тремя аксиомами:

1. Каждая пара $(v,l)$ означает, что значение набора значений $V(K)$ является v, если к списку применена функция условия, $C(l)$, это правда.
2. Одно из условий верно.
3. Только одно из условий верно.

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

Формально,

Имя	Определение
Функция условия	$C(l)=({\bigwedge _{(r,z,u)\in l}z=u}))=(\forall r\forall z\forall u(r,z,u)\in l\to z=u)$
Условие значения	$\forall v\forall l((v,l)\in K\land C(l)\to v=V(K)$
Полный комплект	$\exists v\exists l(v,l)\in K\land C(l)$
Исключение	$\forall v_{1}\forall l_{1}\forall v_{2}\forall l_{2}((v_{1},l_{1})\in K\land (v_{2},l_{2})\in K\land (v_{1},l_{1})\neq (v_{2},l_{2}))\to \neg (C(l_{1})\land C(l_{2}))$

Функция значения

Используя условие ценности и аксиомы полного набора,

$\exists v\exists l(v,l)\in K\land C(l)\land v=V(K)$

В качестве выражения let это выглядит так:

$V(K)=\operatorname {let} (v,l)\in K\land C(l)\operatorname {in} v$

Одно значение

Значение, заданное для представления одного значения:

$k=V(\{(k,\{\})\})$

Вывод такой:

$V(\{(k,\{\})\})$

$=\operatorname {let} (v,l)\in \{(k,\{\})\}\land C(l)\operatorname {in} v$

$=\operatorname {let} v=k\land C(\{\})\operatorname {in} v$

$=\operatorname {let} v=k\operatorname {in} v$

$=k$

Элемент набора

Набор значений для представления элемента набора:

$\forall x\forall X(\operatorname {let} x\in X\operatorname {in} x)=\operatorname {let} R=V(\{(w,\{(R,x,w)\}):w\in X\})\operatorname {in} R$

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

Значение выражения

$x=V(R)$.

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

Если пренебречь добавлением R к зависимому условию, выражение принимает более простой и понятный вид:

$\forall x\forall X(\operatorname {let} x\in X\operatorname {in} x)=V(\{(w,\{(\_,x,w)\}):w\in X\})$

Вывод такой:

$V(\{(w,\{(r,x,w):w\in X\})$

$=\operatorname {let} (v,l)\in \{(w,\{(r,x,w)\}):w\in X\}\land C(l)\operatorname {in} v$

$=\operatorname {let} v\in X\land ({\bigwedge _{(r,z,u)\in \{(\_,x,v)\}}z=u})\operatorname {in} v$

$=\operatorname {let} v\in X\land (\forall r\forall z\forall u(r,z,u)\in \{(\_,x,v)\}\to z=u)\operatorname {in} v$

$=\operatorname {let} v\in X\land x=v\operatorname {in} v$

$=\operatorname {let} x\in X\operatorname {in} x$

Применение функций

Применение функции наборов значений определяется формулой:

$V(M)\ V(N)=V(\{(m_{v}\ n_{v},m_{l}\cup n_{l}):(m_{v},m_{l})\in M\land (n_{v},n_{l})\in N\})$

Вывод,

$V(M)\ V(N)$

$=\operatorname {let} (m_{v},m_{l})\in M\land C(m_{l})\operatorname {in} m_{v})\ (\operatorname {let} (n_{v},n_{l})\in N\land C(n_{l})\operatorname {in} n_{v})$

$=\operatorname {let} (m_{v},m_{l})\in M\land (n_{v},n_{l})\in N\land C(n_{l})\land C(n_{l})\operatorname {in} m_{v}\ n_{v})$

Затем, используя

$C(m_{l})\land C(n_{l})$

$=({\bigwedge _{(z,u)\in m_{l}}z=u})\land ({\bigwedge _{(z,u)\in n_{l}}z=u})$

$=({\bigwedge _{(z,u)\in m_{l}\cup n_{l}}z=u})$

$=C(m_{l}\cup n_{l})$

получать,

$=\operatorname {let} (m_{v},m_{l})\in M\land (n_{v},n_{l})\in N\land C(n_{l}\cup n_{l})\operatorname {in} m_{v}\ n_{v})$

$=\operatorname {let} (v,l)\in \{(m_{v}\ n_{v},m_{l}\cup n_{l}):(m_{v},m_{l})\in M\land (n_{v},n_{l})\in N\}\land C(l)\operatorname {in} v$

$=V(\{(m_{v}\ n_{v},m_{l}\cup n_{l}):(m_{v},m_{l})\in M\land (n_{v},n_{l})\in N\})$

Исключение

Исключение — это правило, определяющее, когда условия должны быть ложными,

$V(M)\in s\iff (\forall v\forall l((v,l)\in M\land v\not \in s)\to \neg C(l))$

Это может быть получено из того,

$V(M)\in s$

$\to \forall v\forall l((v,l)\in M\land C(l))\to (v=V[M]\land V(M)\in s)$

$\to \forall v\forall l((v,l)\in M\land C(l))\to v\in S$

$\to \forall v\forall l((v,l)\in M\land v\not \in S)\to \neg C(l)$

Упрощение

Правило упрощения позволяет отбрасывать значения, условие которых является ложным.

$V(K)=V(\{(v,l):(v,l)\in K\land C(l)\}$

Вывод

$V(\{(v,l):(v,l)\in K\land C(l)\})$

$=\operatorname {let} (v,l)\in \{(v,l):(v,l)\in K\land C(l)\}\land C(l)\operatorname {in} v$

$=\operatorname {let} (v,l)\in K\land C(l)\land C(l)\operatorname {in} v$

$=\operatorname {let} (v,l)\in K\land C(l)\operatorname {in} v$

$=V(K)$

Краткое изложение результатов

Имя	Правило
Функция значения	$V(K)=\operatorname {let} (v,l)\in K\land C(l)\operatorname {in} v$
Одно значение	$k=V(\{(k,\{\})\})$
Установить элемент	$\forall x\forall X(\operatorname {let} x\in X\operatorname {in} x)=\operatorname {let} R=V(\{(w,\{(R,x,w)\}):w\in X\})\operatorname {in} R$
Применение функции	$V(M)\ V(N)=V(\{(m_{v}\ n_{v},m_{l}\cup n_{l}):(m_{v},m_{l})\in M\land (n_{v},n_{l})\in N\})$
Исключение	$V(M)\in s\iff (\forall v\forall l((v,l)\in M\land v\not \in s)\to \neg C(l))$
Упрощение	$V(K)=V(\{(v,l):(v,l)\in K\land C(l)\})$
Утверждать равенство	$V(M)=V(N)\to (\forall v\forall l((v,l)\in N\land v\not \in S(M))\to \neg C(l))$

Значение устанавливает идентичность

Благодаря определению применения функций к наборам значений было также переопределено определение равенства наборов значений. Старое определение равенства все еще существует, поскольку наборы значений создаются как набор пар. Два множества равны, если они содержат одни и те же элементы. Такое определение равенства наборов значений в лучшем случае вводит в заблуждение.

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

В математике количественная оценка осуществляется по значениям, а не по формулам. Чтобы продолжить дальнейшее точное определение наборов значений, необходима количественная оценка формул таким образом, чтобы можно было сравнить идентичность формул. Различие между формулой, представляющей значение, и идентичностью формулы — это различие использования и упоминания . Обозначение,

$\forall x\#u$

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

Используя эту запись, элементом определения множества будет:

$\forall x\#u\forall X(\operatorname {let} x\in X\operatorname {in} x)=\operatorname {let} R=V((u,\{(w,\{(R,x,w)\}):w\in X\}))\operatorname {in} R$

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

Сужение

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

Сужение путем утверждения равенства

Утверждение о том, что два набора значений равны, дает правило сужения:

$\forall m_{v}\forall m_{l}\forall n_{v}\forall n_{l}((m_{v},m_{l})\in M\land (n_{v},n_{l})\in N)\to (m_{v}\neq n_{v}\to \neg (C(m_{l})\land C(n_{l})))$

Для вывода начнем с

$V(M)=V(N)$

Условие значения дает:

$(\forall m_{v}\forall m_{l}((m_{v},m_{l})\in M\land C(m_{l})\to v=V(M))\land (\forall n_{v}\forall n_{l}((n_{v},k)\in N\land C(n_{l}))\to n_{v}=V(N))\land V(M)=V(N)$

$\forall m_{v}\forall m_{l}\forall n_{v}\forall n_{l}(((m_{v},m_{l})\in M\land C(m_{l}))\to m_{v}=V(M))\land (((n_{v},n_{l})\in N\land C(n_{l}))\to n_{v}=V(N))\land V(M)=V(N)$

$\forall m_{v}\forall m_{l}\forall n_{v}\forall n_{l}((m_{v},m_{l})\in M\land (n_{v},n_{l})\in N)\to (C(j)\land C(k)\to v=u)$

$\forall m_{v}\forall m_{l}\forall n_{v}\forall n_{l}((m_{v},m_{l})\in M\land (n_{v},n_{l})\in N)\to (m_{v}\neq n_{v}\to \neg (C(m_{l})\land C(n_{l})))$

Сужение соединением

Если какое-либо базовое условие ложно, то все условия, полученные из него, ложны.

Это следует из определения функции Condition,

$C(l)=({\bigwedge _{(r,z,u)\in l}z=u}))$

Базовое условие для (r, z, u) таково:

$C(\{(r,z,u)\}=(z=u)$

Так что если это ложь $C(l)$ является ложным.

Сужение скрещенными условиями

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

Чтобы получить это, начните с правила исключения, которое гласит:

$\forall v_{1}\forall l_{1}\forall v_{2}\forall l_{2}((v_{1},l_{1})\in K\land (v_{2},l_{2})\in K\land (v_{1},l_{1})\neq (v_{2},l_{2}))\implies \neg (C(l_{1})\land C(l_{2}))$

Тогда для любого набора зависимых l условий

$((K,x,v_{1})\in l\ \land (K,x,v_{2})\in l\land v_{1}\neq v_{2}$

$\implies (v_{1},\{(K,x,v_{1})\})\in K\land (v_{2},\{(K,x,v_{2})\})\in K\land (v_{1},l_{1})\neq (v_{2},l_{2}))$

$\implies \neg (C(\{(K,x,v_{1})\})\land C(\{(K,x,v_{2})\}))$

$\implies \neg C(l)$

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

Сужение путем исключения зависимых значений

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

Чтобы получить это, начните с правила полного набора:

$\exists v\exists \ l(v,l)\in K\to C(l)$

Условная функция:

$C(l)=({\bigwedge _{(r,z,u)\in l}z=u}))$

Может быть выбрано конкретное зависимое условие, подразумеваемое всем условием.

$\forall L\ C(l)\to (L,z,u)\in l\to z=u$

Так

$\forall L\exists v\exists l\ (v,l)\in K\to C(l)\to (L,z,u)\in l\to z=u$

Здесь $z=V(L)$. Выражение можно изменить, чтобы определить набор значений, которые $V(L)$ может взять,

$E(K,L)=\{w:(v,l)\in K\land C(l)\land (L,z,w)\in l\}$

и так,

$V(L)\in E(K,L)$

Затем, используя правило исключения,

$V(M)\in s\iff (\forall v\forall l((v,l)\in M\land v\not \in s)\to \neg C(l))$

дает,

$(\forall K\forall L\forall v\forall l((v,l)\in L\land v\not \in E(K,L))\to \neg C(l))$

Это сужающее правило исключения. $E(K,L)$ представляет собой набор значений в наборе базовых значений L которые представлены в наборе значений K. , Условия для других значений должны быть ложными.

Наборы вероятностных значений

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

$C(l)=({\bigwedge _{(r,z,u)\in l}z=u}))$

Функция вероятности:

$P(l)=({\prod _{(r,z,u)\in l}P(z=u)}))$

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

Функция вероятности определяется тремя аксиомами:

1. Каждая пара $(v,l)$ означает, что вероятность набора значений $V(K)$ — v функция вероятности, примененная к списку, $P(l)$.
2. Сумма вероятностей по всему набору значений равна 1.
3. Вероятность появления любых двух пар в наборе значений равна нулю.

Функция вероятности дает вероятности результатов на основе начальных вероятностей, заданных булевым индуктивным выводом .

Формально,

Имя	Определение
Функция вероятности	$P(l)=({\prod _{(r,z,u)\in l}P(z=u)}))$
Условие значения	$\forall vP(v=V(K))=\sum _{(v,l)\in K}P(l)$
Complete set	$\sum _{(v,l)\in K}P(l)=1$
Allowed values	$\sum _{(v,l)\in K\land v\in \operatorname {gset} (V(K))}P(l)=1$
Exclusion	$\forall v_{1}\forall l_{1}\forall v_{2}\forall l_{2}((v_{1},l_{1})\in K\land (v_{2},l_{2})\in K\land (v_{1},l_{1})\neq (v_{2},l_{2}))\to P(C(l_{1})\land C(l_{2}))=0$

Probabilities for each value in a value set may be calculated from probabilities in base value sets using the probability function and the value condition. Base value sets are either for a single value, or multiple value value set.

Probability for a single value

The value set to represent a single value is,

$k=V(\{(k,\{\})\})$

The complete set rule is,

$\sum _{(v,l)\in K}P(l)$

$=\sum _{(v,l)\in \{(k,\{\})\}}P(l)$

$=P(\{\})$

$=1$

Which is consistent with the axiom.

Probabilities for multiple values

The value set to represent multiple values is,

$\forall x\forall X(\operatorname {let} x\in X\operatorname {in} x)=V(\{(w,\{(\_,x,w)\}):w\in X\})$

The probability is given by the allowed values rule,

$\sum _{(v,l)\in K\land v\in \operatorname {gset} (V(K))}P(l)=1$

which simplifies to,

$\sum _{v\in \operatorname {gset} (V(K))}P(x=v)=1$

If prior estimates of probabilities for values are given then they will be proportional to the posterior probabilities, if the value is in the value set.

$\forall v\in \operatorname {gset} (V(K)),P(x=v)=w*P_{i}(x=v)$

If the value is not in the value set the probabilities will be zero,

$\forall v\not \in \operatorname {gset} (V(K)),P(x=v)=0$

So,

$\sum _{v\in \operatorname {gset} (V(K))}w*P_{i}(x=v)=1$

$w={\frac {1}{\sum _{v\in \operatorname {gset} (V(K))}P_{i}(x=v)}}$

$\forall v\in \operatorname {gset} (V(K)),P(x=v)={\frac {P_{i}(x=v)}{\sum _{v\in \operatorname {gset} (V(K))}P_{i}(x=v)}}$

$\forall v\not \in \operatorname {gset} (V(K)),P(x=v)=0$

If the prior probabilities are all the same the probabilities are,

$\forall v\in \operatorname {gset} (V(K)),P(x=v)={\frac {1}{|\operatorname {gset} (V(K))|}}$

Probabilities of general value sets

A general value set is created out of the application of base value sets. The value condition rule and the probability function may be combined to give,

$\forall vP(v=V(K))=\sum _{(v,l)\in K\land v\in \operatorname {gset} (V(K))}({\prod _{(r,z,u)\in l}P(z=u)}))$

Accessing the value set

Narrowing allows the elimination of values that do not satisfy a variable's constraints. Considered as the basis for an algorithm for solving equations, this narrowing gives a set of values consistent with the constraints on a variable. However in mathematics there is no way to access this set of values.

If $E(x)$ is an expression constraining a variable x then the set of values that the variable may take is,

$\{z:E(z)\}$

Define the gset of x to be the set of values that satisfy the constraints on x. Consider defining gset as,

$\operatorname {gset} (x)=\{z:E(z)\}$

This definition depends on knowing the expression E, which is the condition giving all the constraints on x. Within mathematics E may not be obtained from x. So there is no mathematical function that may be applied to a variable to request the set of values. So may the gset function be added to mathematics?

Meta math definition

A meta-mathematical definition of gset may be possible. Imagine that what we know of as mathematics is actually implemented by a meta function called math. math takes an abstract syntax tree and gives meaning to the variables and mathematical structures and adds existential quantifiers for variables not explicitly quantified.

math would be an expression in a meta mathematical environment with its own variables. To distinguish these meta-variables from math variables represent them by capital letters and the mathematical variables by lower case letters.

Now suppose there is an extended implementation of mathematics implemented by the xmath function, defined as,

$\operatorname {xmath} [E]=\forall M,\operatorname {let} T[M]=\operatorname {math} [E]\operatorname {in} T[\_]$

Using xmath, gset may be defined by,

$\forall x\#u,\exists N,\operatorname {gset} (x)=\operatorname {let} M[u]=x\operatorname {in} \{z:z=N[u]\land T[N]\}$

Here again the notation,

$\forall x\#u$

is used to mean quantification over variables x where x refers to the value, and u refers to the unique identity of the variable.

Example

For example take the constraint expression $x^{2}=4$. Then,

$x^{2}=4$

$\land s=\operatorname {gset} (x)$

$\land (\forall x\#u,\exists N\operatorname {gset} (x)=\operatorname {let} M[u]=x\operatorname {in} \{z:z=N[u]\land T[N]\})$

Then the xmath expression is,

$\forall M,\operatorname {let} T[M]=$

$\exists x,\exists s,(x^{2}=4$

$\land s=\operatorname {gset} (x)$

$\land (\forall x\#u,\exists N,\operatorname {gset} (x)=\operatorname {let} M[u]=x\operatorname {in} \{z:z=N[u]\land T[N]\})$

$\operatorname {in} T[\_]$

Then where u is the unique identity of the variable x, represented here as the number 1 (for the first variable used in a call to gset),

$M[1]=x\land s=\{z:z=N[1]\land T[N]\}$

Here $T[N]$ invokes T with M as N.

$s=\{z:z=N[1]\land x^{2}=4\land x=N[1]\}$

$s=\{z:z^{2}=4\}$

See also

• Functional programming
  • Lazy evaluation
  • Polymorphic type system
  • Type inference
  • Higher-order function
  • Haskell
• Lambda calculus
  • Deductive lambda calculus
  • Let expression
• Logic programming
  • Resolution (logic)
  • Constraint logic programming
  • constraints
  • ECLiPSe
• Mathematics
  • Function (mathematics)
  • Algebra
  • Disjunction
• Relational programming