2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки


Правила форума


Посмотреть правила форума



Начать новую тему Ответить на тему
 
 Что означает слово "вычислить"?
Сообщение23.01.2017, 15:05 
Заслуженный участник


08/04/08
8556
Можно ли придать точный смысл задачам вида "Вычислить $f(a_1,...,a_n)$"?

Если обозначить множество значений функции $f$ как $D$, то сначала получается такое: вычислить $f(a_1,...,a_n)$ означает найти $d\in D$ такой, что $d=f(a_1,...,a_n)$. Смысл вроде бы ясен, однако формально получается ерунда: исходный терм $f(a_1,...,a_n)$ удовлетворяет условию задачи, действительно: $f(a_1,...,a_n) = f(a_1,...,a_n)$ и $f(a_1,...,a_n) \in D$. И любой равный ему терм тоже удовлетворяет условию. (например, при таком определении решением задачи "Вычислить $2+2$" будет $3+1$, поскольку $2+2=3+1$ и $3+1$ - натуральное число!)

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

Пусть $A$ - какой-то конечный алфавит, $A^+$ - множество непустых строк в нем. Множество $X$ назовем кодифицированным в $A$ $\Leftirghtarrow$ существует эффективно вычислимая в обе стороны биекция $\varphi$ из какого-то подмножества $A^+$ в $X$. Значения $\varphi^{-1}(x)$ будем называть меткой элемента $x\in X$.
Пусть $M$ - множество, $F(M)$ - некое подмножество функций $M\to M$, причем $M \cup F(M)$ кодифицированы.
Определение: простым синтаксическим деревом назовем граф, состоящий из одной вершины с меткой $s \in A^+$. Будем его обозначать $t(s)$.
Определение: 1. Простое синтаксическое дерево является синтаксическим деревом.
2. Если $t_1, ..., t_n$ - синтаксические деревья, $f$ - $n$-местная функция, $s$ - метка $f$, то ориентированное дерево с корнем $f$ и дугами, связывающими $f$ и корни $t_1,...,t_n$ в таком же порядке тоже является синтаксическим деревом (это я рисователь деревьев пока ниасилил)
3. Других синтаксических деревьев нет.
Далее я буду слово "синтаксическое" для простоты опускать.
Определение: пусть $T$ - дерево.
1. Если $T$ - простое: $T=t(s)$, то его значение $v(T)=\varphi(s)$.
2. Если $T$ - дерево с корнем с меткой $s=\varphi^{-1}(f)$, где $f$ - $n$-местная функция, а $t_1,...,t_n$ - непосредственные поддеревья корня, то его значение $v(T)=f(v(t_1),...,v(t_n))$.
Множество всех деревьев над $M, F(M)$ обозначим $W(M,F(M))$.
Отношение $=$ на $M$ порождает нетривиальное отношение эквивалентности $\simeq$ на $W(M,F(M))$ при $F(M)\not = \varnothing$: $T_1 \simeq T_2 \Leftrightarrow v(T_1)=v(T_2)$.

Таким образом, задача вида "Вычислить $f(a_1,...,a_n)$" означает "Для какого-нибудь дерева $T$, представляющего $f(a_1,...,a_n)$, найти простое дерево $t(s): T\simeq t(s)$ и $\varphi(s)\in D$". Т.е. пафос в том, что мы работает не с элементами $M$, а с деревьями.

Аналогично можно придать более точный смысл более общим задачам:
1. Задача "Упростить $f(a_1,...,a_n)$" означает "Для дерева $T$, представляющего $f(a_1,...,a_n)$, найти эквивалентное дерево с минимальным числом вершин".
2. Задача "Вычислить $e$ относительно множества функций/функционалов/еще-чего-то-более-страшного $F$" означает "Для дерева $T$, представляющего $f(a_1,...,a_n)$, найти эквивалентное дерево, не содержащее меток $f\in F$". Это задачи вычисления производных, определенных и неопределенных интегралов, нахождения суммы в замкнутом виде и т.п. - во всех них требуется найти представление в виде дерева, не содержащего функционалы.

Если просмотреть типовые задачи на вычисление, то можно заметить, что из некоторых из них "торчат уши" подхода с деревьями. Те же формулировки типа "найти сумму в замкнутом виде", теоремы интегрирования некоторых классов функций ($\int R(\sqrt[n]{\frac{ax+b}{cx+d}}, x)dx$, способы упрощения диффуров, "не содержащих в явном виде" буквы $y'$ или $x$, формализация поиска области определения и т.п.).
С другой стороны, с формализацией смысла задачи типа вида "Вычислить $f(a_1,...,a_n)$" может оказаться не все так гладко.

Т.е. получается в математике часть задач на вычисление имеет "дырявые абстракции" - написано простое выражение, но за ним стоит сложное дерево, которое "не замечают", но иногда при необходимости к нему обращаются.
И вот это все к чему: а почему ничего подобного в книгах по математике нету? Это все давно известно и описано в книгах $B_1, B_2, ...$, которые я просто не читал? (я видел деревья только в книгах по информатике) Это очевидно, уныло и неинтересно? Это не дает ни одной полезной теоремы? Это излишняя формализация? Или еще какая-то причина?

 Профиль  
                  
 
 Re: Что означает слово "вычислить"?
Сообщение23.01.2017, 15:38 
Заслуженный участник
Аватара пользователя


06/10/08
6422
Ну, деревья и формулы - это разные представления одного и того же, так что это можно сформулировать так - есть выделенный класс термов (обычно называется "в нормальной форме"), по заданному терму найти терм в нормальной форме, эквивалентный ему. Похожие штуки изучаются в $\lambda$-исчислении и теории типов (нормализация), но я про это почти ничего не знаю.

Sonic86 в сообщении #1186821 писал(а):
И вот это все к чему: а почему ничего подобного в книгах по математике нету? Это все давно известно и описано в книгах $B_1, B_2, ...$, которые я просто не читал? (я видел деревья только в книгах по информатике) Это очевидно, уныло и неинтересно? Это не дает ни одной полезной теоремы? Это излишняя формализация? Или еще какая-то причина?
По видимому излишняя формализация.

 Профиль  
                  
 
 Re: Что означает слово "вычислить"?
Сообщение23.01.2017, 19:28 
Заслуженный участник


27/04/09
28128
Добавить тут можно разве что описание разных часто используемых нормальных форм. В монографии Барендрегта описаны нормальная и головная нормальная формы для чистого λ-исчисления, «значениями» обычно считаются г. н. ф.; на большое число типизированных λ-исчислений определения этих форм, вроде, распространяются единственным образом; если взять термы арифметики, нормальными формами можно считать термы $0,S0,SS0,\ldots$; и т. д., обычно более-менее ясно, что входит, а что не входит в это множество.

Sonic86 в сообщении #1186821 писал(а):
1. Задача "Упростить $f(a_1,...,a_n)$" означает "Для дерева $T$, представляющего $f(a_1,...,a_n)$, найти эквивалентное дерево с минимальным числом вершин".
Не думаю, что всегда с минимальным среди всех. Может накладываться условие наличия только какого-то подмножества функциональных символов (и вообще всяческих конструкторов термов и формул, если у нас язык посложнее), например, то есть, ещё и включать ваш второй пункт «выразить». Например, $\sin(\pi/10)$ содержит 4 вершины в дереве, а $(\sqrt5 - 1)/4$ — целых 6, но может много где считаться более простым, потому что не содержит синус.

Ещё тут, кажется, не упомянули разные стратегии вычисления (по имени, по значению, по необходимости — всё они) — ограничения на применение «вычисляющих» правил вывода, и разные нормальные формы можно определять как результаты последовательного применения конкретной стратегии (если оно заканчивается) к терму. Например, если я не ошибаюсь, при нормальном порядке вычислений в λ-исчислении получится, если получится, как раз г. н. ф. (если это то же самое, что головная редукция у Барендрегта — вроде то же, у меня сейчас не совсем удовлетворительное определение нормального порядка из TaPL).

 Профиль  
                  
 
 Re: Что означает слово "вычислить"?
Сообщение23.01.2017, 21:16 
Заслуженный участник


08/04/08
8556
Xaositect, arseniiv, спасибо, видимо все-таки придется Барендрегта читать :| в прошлый раз он вызвал у меня непреходящий ужас.

arseniiv в сообщении #1186910 писал(а):
если взять термы арифметики, нормальными формами можно считать термы $0,S0,SS0,\ldots$; и т. д., обычно более-менее ясно, что входит, а что не входит в это множество.
arseniiv в сообщении #1186910 писал(а):
Может накладываться условие наличия только какого-то подмножества функциональных символов (и вообще всяческих конструкторов термов и формул, если у нас язык посложнее), например, то есть, ещё и включать ваш второй пункт «выразить». Например, $\sin(\pi/10)$ содержит 4 вершины в дереве, а $(\sqrt5 - 1)/4$ — целых 6, но может много где считаться более простым, потому что не содержит синус.
Можно считать, что мы тут пытаемся исключить $\sin$. В конце концов, можно и $\sin \frac{2\pi}{17}$ выразить в радикалах, но.... Я это вообще пока не рассматривал. Элементарно - взять $\mathbb{R}$, оно несчетно, а деревьев - счетное число. Тут даже с $\sqrt{2}$ что-то придется делать, чтобы считать, что оно вычислено.

arseniiv в сообщении #1186910 писал(а):
Ещё тут, кажется, не упомянули разные стратегии вычисления (по имени, по значению, по необходимости — всё они) — ограничения на применение «вычисляющих» правил вывода, и разные нормальные формы можно определять как результаты последовательного применения конкретной стратегии (если оно заканчивается) к терму.
Чего-то я сомневаюсь, что они в общем случае возможны. Например, вычислить $[100500\cdot e]$. Или взять берущийся интеграл от элементарной функции. Или мне лучше попрактиковаться в этих правилах вычисления?

 Профиль  
                  
 
 Re: Что означает слово "вычислить"?
Сообщение23.01.2017, 21:47 
Заслуженный участник


27/04/09
28128
Sonic86 в сообщении #1186942 писал(а):
видимо все-таки придется Барендрегта читать :| в прошлый раз он вызвал у меня непреходящий ужас.
Не обязательно его. Просто у меня ничего другого столь же подробного под рукой нет, вот и пишу о нём.

Sonic86 в сообщении #1186942 писал(а):
Тут даже с $\sqrt{2}$ что-то придется делать, чтобы считать, что оно вычислено.
Просто считать, что $\sqrt2$ уже есть значение и дальше не вычисляется. Т. е. не нужно пытаться охватить все вычисления каким-то одним понятием, т. к. в разных контекстах требуется вычислять «на разную глубину», и соответствующие множества нормальных форм и стратегии вычисления отличаются.

Sonic86 в сообщении #1186942 писал(а):
Например, вычислить $[100500\cdot e]$.
Ну, как мы вообще можем вычислить вещественнозначное выражение? :-)

Sonic86 в сообщении #1186942 писал(а):
Или мне лучше попрактиковаться в этих правилах вычисления?
Их набор зависит от теории. Это просто подмножество правил вывода, у которых «явно вычислительный смысл» — например, β-редукция, если сравнить её с правилами, скажем, образования λ-термов. В общем случае в неформальной теории набор всех правил, которые мы применяем при вычислении, вряд ли есть смысл перечислять.

 Профиль  
                  
 
 Re: Что означает слово "вычислить"?
Сообщение24.01.2017, 12:45 
Заслуженный участник


08/04/08
8556
arseniiv в сообщении #1186949 писал(а):
Sonic86 в сообщении #1186942 писал(а):
Например, вычислить $[100500\cdot e]$.
Ну, как мы вообще можем вычислить вещественнозначное выражение? :-)
Оно целое, и вычислить его руками легко, а вот можно ли его вычислить стратегиями вычисления лямбда-термов - сомневаюсь (я там только 2 стратегии помню - вычислять снаружи и изнутри. Просто снаружи сразу не сработает, а просто изнутри - тоже не сработает, т.к. под целой частью - действительное число, все знаки которого не вычислишь).

arseniiv в сообщении #1186949 писал(а):
Не обязательно его. Просто у меня ничего другого столь же подробного под рукой нет, вот и пишу о нём.
TaPL мне не помог, а ничего другого кроме Барендрегта я не знаю :-( Другой русскоязычной литературы я не нагуглил.

arseniiv в сообщении #1186949 писал(а):
В общем случае в неформальной теории набор всех правил, которые мы применяем при вычислении, вряд ли есть смысл перечислять.
Думаете, их очень много?

 Профиль  
                  
 
 Re: Что означает слово "вычислить"?
Сообщение24.01.2017, 17:40 
Заслуженный участник
Аватара пользователя


01/03/06
13626
Москва
Про смысл термина "вычислимость" размышлял Ю.И. Манин в книге "Вычислимое и невычислимое".

 Профиль  
                  
 
 Re: Что означает слово "вычислить"?
Сообщение24.01.2017, 19:11 
Заслуженный участник


27/04/09
28128
Sonic86 в сообщении #1187068 писал(а):
Оно целое, и вычислить его руками легко, а вот можно ли его вычислить стратегиями вычисления лямбда-термов - сомневаюсь (я там только 2 стратегии помню - вычислять снаружи и изнутри. Просто снаружи сразу не сработает, а просто изнутри - тоже не сработает, т.к. под целой частью - действительное число, все знаки которого не вычислишь).
Если вложить этот терм в λ-исчисление, надо сначала задать, как именно всё представлять. :-) Может, и нормально всё вычислится. Вот допустим, $100500$ и $e$ — функции, выдающие, скажем, по натуральному числу (закодированному по Чёрчу, скажем) пару рациональных границ (закодированных как тройки натуральных $(m,n,d)\mapsto(m-n)/d$). Также пусть тогда $\cdot$ — функция умножения таких чисел, в определении которой тоже проблем быть не должно, если мы наопределяли функций для натуральных и рациональных; и $\lfloor\cdot\rfloor$ будет функцией из вещественного числа в пару натуральных.

Стратегий в λ-исчислении больше двух: аппликативный порядок, нормальный, по имени, по значению, и возможны какие-нибудь ещё менее известные. Аппликативный порядок и по значению — не нормализующие стратегии. Но возьмём вычисление по значению. Эта стратегия считает значениями λ-абстракции и переменные и редуцирует самый внешний редекс, не находящийся внутри λ-абстракции и имеющий аргументом значение.

Итак, $100500$ и $e$ — λ-абстракции и не редуцируются. Первым шагом редукции в $\operatorname{floor}(\operatorname{times} 100500\; e)$ редуцируется $\operatorname{times} 100500$ и после какого-то количества редукций примет вид λ-абстракции $\operatorname{times_{100500}}$, в которой редуцировать нельзя, так что дальше редуцируется $\operatorname{times_{100500}}e$, и после некоторого числа редукций это снова станет λ-абстракцией $A$, после чего, наконец, редуцируется $\operatorname{floor}A$, и т. д.. Тут нигде не должно появляться расходящихся термов, если всё определили правильно, так что вычисление по значению сойдёт.

Sonic86 в сообщении #1187068 писал(а):
TaPL мне не помог, а ничего другого кроме Барендрегта я не знаю :-( Другой русскоязычной литературы я не нагуглил.
А ссылки из §5.4 TaPL (кроме Б.) на русском языке не нашлись?

Sonic86 в сообщении #1187068 писал(а):
Думаете, их очень много?
Не знаю, но их набор точно будет отличаться в зависимости от контекста. Потом, стратегия вычисления для человека будет, думаю, весьма заковыристая из-за того, как вообще устроена голова. Это будет какое-то в общем случае вероятностное применение правил в сложной зависимости от вида выражения и вида задачи.

 Профиль  
                  
 
 Re: Что означает слово "вычислить"?
Сообщение25.01.2017, 00:03 
Заслуженный участник


27/04/09
28128
Вот модуль, с помощью которого на моём компьютере можно дождаться вычисления $\lfloor2\cdot e\rfloor$, хотя с множителями побольше уже всё плохо, мне лень было ждать.

код: [ скачать ] [ спрятать ]
Используется синтаксис Haskell
{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances, RankNTypes #-}
module LambdaNumbers where

import Prelude hiding (not, and, or, fst, snd)
import Data.Ratio ((%))

fix :: (a -> a) -> a
--fix f = let a = (\x -> f (\y -> x x y)) in a a -- for by value
fix f = let x = f x in x

class HumanReadable a b where
  humanize :: a -> b

newtype CBool = CBool { unCBool :: forall a. a -> a -> a }

true = CBool $ \t f -> t
false = CBool $ \t f -> f

and, or :: CBool -> CBool -> CBool
and a b = unCBool a b false
or a b = unCBool a true b

not :: CBool -> CBool
not a = unCBool a false true

--ifthenelse :: CBool -> a -> a -> a
--ifthenelse = unCBool

instance HumanReadable CBool Bool where
  humanize b = unCBool b True False

newtype CPair a b = CPair { unCPair :: forall c. (a -> b -> c) -> c  }

pair :: a -> b -> CPair a b
pair a b = CPair $ \f -> f a b

fst :: CPair a b -> a
fst p = unCPair p (\a1 a2 -> a1)

snd :: CPair a b -> b
snd p = unCPair p (\a1 a2 -> a2)

instance (HumanReadable a a', HumanReadable b b') => HumanReadable (CPair a b) (a',b') where
  humanize p = unCPair p $ \a1 a2 -> (humanize a1, humanize a2)

newtype CNat = CNat { unCNat :: forall a. (a -> a) -> a -> a }

zeroN = CNat $ \s z -> z
unitN = CNat $ id

succN, predN :: CNat -> CNat
succN n = CNat $ \s z -> s (unCNat n s z)
predN n = CNat $ \s z -> unCNat n (\g h -> h (g s)) (const z) id

--repeat :: CNat -> (a -> a) -> (a -> a)
--repeat = unCNat

isZeroN :: CNat -> CBool
isZeroN n = unCNat n (const false) true

plusN, minusN, timesN, powN :: CNat -> CNat -> CNat
plusN m n = unCNat m succN n
minusN m n = unCNat n predN m
timesN m n = CNat $ unCNat m . unCNat n
powN m n = CNat $ unCNat n $ unCNat m

leN, ltN, eqN :: CNat -> CNat -> CBool
leN m n = isZeroN (minusN m n)
eqN m n = and (leN m n) (leN n m)
ltN m n = and (leN m n) (not (leN n m))

factorial :: CNat -> CNat
factorial = fix (\fac n -> unCBool (isZeroN n) unitN (timesN n (fac (predN n))))

-- 100500 = (100 * 10 + 5) * 100
twoN = succN unitN
fourN = plusN twoN twoN
fiveN = succN fourN
tenN = plusN fiveN fiveN
hundredN = timesN tenN tenN
stopitsotN = timesN hundredN $ plusN fiveN $ timesN hundredN tenN

instance HumanReadable CNat Integer where
  humanize n = unCNat n (+1) 0

newtype CInt = CInt { unCInt :: CPair CNat CNat }

posPart, negPart :: CInt -> CNat
posPart = fst . unCInt
negPart = snd . unCInt

fromPartsI :: CNat -> CNat -> CInt
fromPartsI m n = CInt $ pair m n

fromNatI, fromNatNegI :: CNat -> CInt
fromNatI n = fromPartsI n zeroN
fromNatNegI = fromPartsI zeroN

zeroI, unitI :: CInt
zeroI = fromNatI zeroN
unitI = fromNatI unitN

isZeroI, isPosI, isNegI :: CInt -> CBool
isZeroI n = eqN (posPart n) (negPart n)
isPosI n = ltN (negPart n) (posPart n)
isNegI n = ltN (posPart n) (negPart n)

absIN :: CInt -> CNat
absIN n = unCBool (isPosI n) (minusN (posPart n) (negPart n)) (minusN (negPart n) (posPart n))

negI, normalizeI :: CInt -> CInt
negI n = fromPartsI (negPart n) (posPart n)
normalizeI n = unCBool (isPosI n) id negI $ fromPartsI (absIN n) zeroN

plusI, minusI, timesI :: CInt -> CInt -> CInt
plusI m n = normalizeI $ fromPartsI pp np where
  pp = plusN (posPart m) (posPart n)
  np = plusN (negPart m) (negPart n)
minusI m n = normalizeI $ plusI m (negI n)
timesI m n = fromPartsI pp np where
  pp = plusN (timesN (posPart m) (posPart n)) (timesN (negPart m) (negPart n))
  np = plusN (timesN (posPart m) (negPart n)) (timesN (negPart m) (posPart n))

leI, ltI, eqI :: CInt -> CInt -> CBool
eqI m n = isZeroI $ minusI m n
leI m n = not $ isPosI $ minusI n m
ltI m n = isNegI $ minusI m n

divIN, modIN :: CInt -> CNat -> CInt
divIN m n = fix h m (fromNatI n) where
  h div m n = unCBool base zeroI $ unCBool less lessCase moreCase where
    base = and (not $ isNegI m) (ltI m n)
    less = isNegI m
    lessCase = minusI (div (plusI m n) n) unitI
    moreCase = plusI (div (minusI m n) n) unitI
modIN m n = fix h m (fromNatI n) where
  h mod m n = unCBool base m $ unCBool less lessCase moreCase where
    base = and (not $ isNegI m) (ltI m n)
    less = isNegI m
    lessCase = mod (plusI m n) n
    moreCase = mod (minusI m n) n

instance HumanReadable CInt Integer where
  humanize n = humanize (posPart n) - humanize (negPart n)

newtype CRat = CRat { unCRat :: CPair CInt CNat }

nom :: CRat -> CInt
nom = fst . unCRat

den :: CRat -> CNat
den = snd . unCRat

fromPartsR :: CInt -> CNat -> CRat
fromPartsR n d = CRat $ pair n d

fromIntR :: CInt -> CRat
fromIntR n = fromPartsR n unitN

fromNatR, fromNatAliquoteR :: CNat -> CRat
fromNatR = fromIntR . fromNatI
fromNatAliquoteR = fromPartsR unitI

zeroR, unitR :: CRat
zeroR = fromIntR zeroI
unitR = fromIntR unitI

isZeroR, isPosR, isNegR :: CRat -> CBool
isZeroR = isZeroI . nom
isPosR = isPosI . nom
isNegR = isNegI . nom

leR, ltR, eqR :: CRat -> CRat -> CBool
eqR q r = isZeroR $ minusR q r
leR q r = not $ isPosR $ minusR q r
ltR q r = isNegR $ minusR q r

negR, invR :: CRat -> CRat
negR r = fromPartsR (negI $ nom r) (den r)
invR r = unCBool (isZeroI n) zeroR $ unCBool (isPosI n) invpos invneg where
  n = nom r
  d = den r
  invpos = fromPartsR (fromNatI d) (absIN n)
  invneg = fromPartsR (fromNatNegI d) (absIN n)

plusR, minusR, timesR, divR :: CRat -> CRat -> CRat
plusR q r = fromPartsR (plusI (timesI a (fromNatI d)) (timesI c (fromNatI b))) (timesN b d) where
  a = nom q
  b = den q
  c = nom r
  d = den r
minusR q r = plusR q (negR r)
timesR q r = fromPartsR (timesI a c) (timesN b d) where
  a = nom q
  b = den q
  c = nom r
  d = den r
divR q r = timesR q (invR r)

minR, maxR :: CRat -> CRat -> CRat
minR q r = unCBool (ltR q r) q r
maxR q r = unCBool (ltR q r) r q

floorRI :: CRat -> CInt
floorRI r = divIN (nom r) (den r)

instance HumanReadable CRat Rational where
  humanize r = humanize (nom r) % humanize (den r)

newtype CReal = CReal { unCReal :: CNat -> CPair CRat CRat }

lbound, ubound :: CReal -> CNat -> CRat
lbound x n = fst $ unCReal x n
ubound x n = snd $ unCReal x n

fromRatX :: CRat -> CReal
fromRatX r = CReal $ const $ pair r r

negX :: CReal -> CReal
negX x = CReal $ \n -> pair (negR $ ubound x n) (negR $ lbound x n)

plusX, minusX, timesX :: CReal -> CReal -> CReal
plusX x y = CReal h where
  h n = pair lb ub where
    lb = plusR (lbound x n) (lbound y n)
    ub = plusR (ubound x n) (ubound y n)
minusX x y = plusX x (negX y)
timesX x y = CReal h where
  h n = pair lb ub where
    xl = lbound x n
    xu = ubound x n
    yl = lbound y n
    yu = ubound y n
    lb = minR (minR (timesR xl yl) (timesR xl yu)) (minR (timesR xu yl) (timesR xu yu))
    ub = maxR (maxR (timesR xl yl) (timesR xl yu)) (maxR (timesR xu yl) (timesR xu yu))

floorXI :: CReal -> CInt
floorXI x = startWith zeroN where
  startWith = fix $ \sw n -> unCBool (partialFloorsEqual n) (lfloor n) (sw $ succN n)
  lfloor n = floorRI (lbound x n)
  ufloor n = floorRI (ubound x n)
  partialFloorsEqual n = eqI (lfloor n) (ufloor n)

partialE :: CNat -> CRat
partialE = fix h where
  h pe n = plusR overFactorial $ unCBool (isZeroN n) zeroR (partialE (predN n)) where
    overFactorial = fromNatAliquoteR $ factorial n

eX = CReal h where
  h n = pair lb ub where
    n' = succN n
    overFactorial = fromNatAliquoteR $ factorial n'
    lb = partialE n'
    ub = plusR lb $ timesR overFactorial $ fromNatAliquoteR n'

-- finally!

cnat :: Int -> CNat
cnat n = h n zeroN where
  h n cn | n == 0    = cn
         | n > 0     = h (n - 1) (succN cn)
         | otherwise = error "nat: negative argument"

bounds :: CReal -> Int -> (Rational, Rational)
bounds x n = humanize $ unCReal x (cnat n)

expr :: CReal
expr = timesX (fromRatX $ fromNatR twoN) eX

expr2 :: CInt
expr2 = floorXI expr

main :: IO Integer
main = return $ humanize expr2
 

Код так себе, там оказалось много ненужного. Типы же пусть не пугают, я их сделал для удобства разработки, и на вычислениях функции CNat, unCNat и т. п. никак не сказываются. Конструкции let и where тоже ничего нового к выразительности λ-исчисления не добавляют, и комбинатор фиксированной точки в самом верху можно написать честно. Стратегия вычислений здесь везде будет call by need, потому что я нигде не добавлял строгости. Типокласс с инстансами и директивы компилятора — тоже для упрощения моей жизни и выведения того, что там навычислялось, в человеческом виде (не совсем доделанно: приходится писать тип результата для функции humanize, а введение функциональной зависимости между параметрами класса не срабатывает из-за инстанса для пар, и я там решил не разбираться, можно ли его исправить).

Можно оптимизировать представления и добиться убыстрения. Видимо, начинать стоит с представления натуральных чисел, взяв вместо чёрчевских функций свёртки какие-нибудь списки двоичных разрядов, например. Результаты операций с рациональными числами тоже не упрощаются, потому что для этого пришлось бы писать GCD, а я вечно не помню алгоритм, а искать лень. :-)

-- Ср янв 25, 2017 02:07:30 --

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

-- Ср янв 25, 2017 02:08:06 --

(Ах да, похвалите меня. :mrgreen: Молодец, arseniiv, велосипед написал.)

 Профиль  
                  
 
 Re: Что означает слово "вычислить"?
Сообщение25.01.2017, 01:07 
Заслуженный участник


27/04/09
28128
Вот теперь чуть подчищенная версия, где всё до рациональных чисел — хаскелевское. Код мне всё равно не нравится, но в любом случае для вычислимых вещественных есть уже библиотеки, где всё хорошо, а написать такую здесь цели и не было.

код: [ скачать ] [ спрятать ]
Используется синтаксис Haskell
module ComputableReals where

import Data.Ratio

type Nat = Integer
type Bounds = (Rational, Rational)

newtype CReal = CReal { bounds :: Nat -> Bounds }

instance Num CReal where
  (+) = plusX
  (-) = minusX
  (*) = timesX
  negate = negX
  abs = error "no abs"
  signum = error "no signum"
  fromInteger = fromRatX . fromInteger

instance Fractional CReal where
  (/) = error "no div"
  recip = error "no recip"
  fromRational = fromRatX

lbound, ubound :: CReal -> Nat -> Rational
lbound x n = fst $ bounds x n
ubound x n = snd $ bounds x n

fromRatX :: Rational -> CReal
fromRatX r = CReal $ const (r, r)

negX :: CReal -> CReal
negX x = CReal $ \n -> (negate $ ubound x n, negate $ lbound x n)

plusX, minusX, timesX :: CReal -> CReal -> CReal
plusX x y = CReal h where
  h n = (lb, ub) where
    lb = (lbound x n) + (lbound y n)
    ub = (ubound x n) + (ubound y n)
minusX x y = plusX x (negX y)
timesX x y = CReal h where
  h n = (lb, ub) where
    (xl, xu) = bounds x n
    (yl, yu) = bounds y n
    values = [xl * yl, xl * yu, xu * yl, xu * yu]
    lb = minimum values
    ub = maximum values

floorX :: CReal -> Integer
floorX x = startWith 0 where
  startWith n | lfloor == ufloor = lfloor
              | otherwise        = startWith (n + 1) where
    lfloor = floor $ lbound x n
    ufloor = floor $ ubound x n

eX = CReal h where
  h n = (lb, ub) where
    n' = n + 1
    lb = sum [ 1 % product [1..i] | i <- [0..n'] ]
    ub = lb + 1 % (n' * product [1..n'])

test :: [Integer]
test = [floorX (100500 * eX), floor (100500 * exp 0)] -- наше и стандартное

main :: IO [Integer]
main = return test
 

 Профиль  
                  
 
 Re: Что означает слово "вычислить"?
Сообщение25.01.2017, 21:41 
Заслуженный участник


08/04/08
8556
arseniiv в сообщении #1187123 писал(а):
А ссылки из §5.4 TaPL (кроме Б.) на русском языке не нашлись?
Кроме SICPа не нашел ничего. SICP читал несколько лет назад, но у меня не осталось ощущения, что там лямбда-исчисление описано очень подробно.

arseniiv в сообщении #1187123 писал(а):
Потом, стратегия вычисления для человека будет, думаю, весьма заковыристая из-за того, как вообще устроена голова. Это будет какое-то в общем случае вероятностное применение правил в сложной зависимости от вида выражения и вида задачи.
Вот как раз такого результата совсем бы не хотелось, хотелось бы какое-нибудь ограниченное, хорошо классифицированное множество вариантов.

arseniiv в сообщении #1187123 писал(а):
Если вложить этот терм в λ-исчисление, надо сначала задать, как именно всё представлять. :-) Может, и нормально всё вычислится. Вот допустим, $100500$ и $e$ — функции, выдающие, скажем, по натуральному числу (закодированному по Чёрчу, скажем) пару рациональных границ (закодированных как тройки натуральных $(m,n,d)\mapsto(m-n)/d$). Также пусть тогда $\cdot$ — функция умножения таких чисел, в определении которой тоже проблем быть не должно, если мы наопределяли функций для натуральных и рациональных; и $\lfloor\cdot\rfloor$ будет функцией из вещественного числа в пару натуральных.
Я прочитал вторую программу, насколько это было мне доступно. Я надеюсь, что реализация ее Вам принесла хоть какое-нибудь удовольствие и пользу :-) Задание действительного числа последовательностью сходящихся границ - это еще ладно. Но можно было сразу сказать, что последовательность границ Вы как программист сами вписываете в код программы - тогда оно конечно все просто считается. И, наверное, стратегия вычисления сработает любая. Если же дано, например, просто, что $e=\sum\limits_{k=0}^{+\infty}\frac{1}{k!}$, то границы отсюда так просто не получаются.

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

 Профиль  
                  
 
 Re: Что означает слово "вычислить"?
Сообщение25.01.2017, 23:04 
Заслуженный участник


27/04/09
28128
Да, конечно. :-)

Sonic86 в сообщении #1187420 писал(а):
Если же дано, например, просто, что $e=\sum\limits_{k=0}^{+\infty}\frac{1}{k!}$, то границы отсюда так просто не получаются.
Я ещё не очень разбираюсь в эквивалентных определениях вычислимых вещественных чисел, но, вроде, если позволять брать просто сходящиеся последовательности рациональных без всяких границ, то чего-то будет нельзя посчитать, что принято возможным.

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

Sonic86 в сообщении #1187420 писал(а):
Я надеюсь, что реализация ее Вам принесла хоть какое-нибудь удовольствие и пользу :-)
Ну, как сказать, но раз уж я дописал это до хоть какого-то результата, видимо, это было приемлемо. :D Особенно порадовало меня, когда получилась интригующая знакопеременная последовательность границ для $e$, причина чего спряталась почти в самом начале пути в перепутанном порядке аргументов в

minusN m n = unCNat n predN m

из-за чего, например, натуральная 1 считалась меньше нуля, а суммой двух целых единиц оказывалось −2 :D (что наследовалось рациональными и приводило к знакопеременности в частичных суммах ряда для экспоненты). Множество ошибок отловил компилятор благодаря оборачиванию всего в типы.

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 12 ] 

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: Gevin Magnus, Vladimir Pliassov


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group