Что означает слово "вычислить"?

[Sonic86]

Можно ли придать точный смысл задачам вида "Вычислить $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, ...$, которые я просто не читал? (я видел деревья только в книгах по информатике) Это очевидно, уныло и неинтересно? Это не дает ни одной полезной теоремы? Это излишняя формализация? Или еще какая-то причина?

[Xaositect]

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

Sonic86 в сообщении #1186821 писал(а):

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

По видимому излишняя формализация.

[arseniiv]

Добавить тут можно разве что описание разных часто используемых нормальных форм. В монографии Барендрегта описаны нормальная и головная нормальная формы для чистого λ-исчисления, «значениями» обычно считаются г. н. ф.; на большое число типизированных λ-исчислений определения этих форм, вроде, распространяются единственным образом; если взять термы арифметики, нормальными формами можно считать термы $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).

[Sonic86]

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]$. Или взять берущийся интеграл от элементарной функции. Или мне лучше попрактиковаться в этих правилах вычисления?

[arseniiv]

Sonic86 в сообщении #1186942 писал(а):

видимо все-таки придется Барендрегта читать в прошлый раз он вызвал у меня непреходящий ужас.

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

Sonic86 в сообщении #1186942 писал(а):

Тут даже с $\sqrt{2}$ что-то придется делать, чтобы считать, что оно вычислено.

Просто считать, что $\sqrt2$ уже есть значение и дальше не вычисляется. Т. е. не нужно пытаться охватить все вычисления каким-то одним понятием, т. к. в разных контекстах требуется вычислять «на разную глубину», и соответствующие множества нормальных форм и стратегии вычисления отличаются.

Sonic86 в сообщении #1186942 писал(а):

Например, вычислить $[100500\cdot e]$.

Ну, как мы вообще можем вычислить вещественнозначное выражение?

Sonic86 в сообщении #1186942 писал(а):

Или мне лучше попрактиковаться в этих правилах вычисления?

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

[Sonic86]

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

Sonic86 в сообщении #1186942 писал(а):

Например, вычислить $[100500\cdot e]$.

Ну, как мы вообще можем вычислить вещественнозначное выражение?

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

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

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

TaPL мне не помог, а ничего другого кроме Барендрегта я не знаю Другой русскоязычной литературы я не нагуглил.

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

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

Думаете, их очень много?

[Brukvalub]

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

[arseniiv]

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 писал(а):

Думаете, их очень много?

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

[arseniiv]

Вот модуль, с помощью которого на моём компьютере можно дождаться вычисления $\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 --

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

[arseniiv]

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

Используется синтаксис 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
 

[Sonic86]

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!}$, то границы отсюда так просто не получаются.

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

[arseniiv]

Да, конечно.

Sonic86 в сообщении #1187420 писал(а):

Если же дано, например, просто, что $e=\sum\limits_{k=0}^{+\infty}\frac{1}{k!}$, то границы отсюда так просто не получаются.

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

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

Sonic86 в сообщении #1187420 писал(а):

Я надеюсь, что реализация ее Вам принесла хоть какое-нибудь удовольствие и пользу

Ну, как сказать, но раз уж я дописал это до хоть какого-то результата, видимо, это было приемлемо. Особенно порадовало меня, когда получилась интригующая знакопеременная последовательность границ для $e$, причина чего спряталась почти в самом начале пути в перепутанном порядке аргументов в

minusN m n = unCNat n predN m

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