deniok | Обратная функция на Агде

Как можно конструктивно доказать, что число 4 является полным квадратом некоторого натурального числа? Предъявив такое число n, для которого n * n = 4. ~~И мы знаем такое число, но никому не скажем, что это 2.~~ Обобщим это наблюдение, введя бинарное отношение принадлежности величины образу функции f как тип данных Агды

data Image_∋_ {X Y : Set}(f : X → Y) : Y → Set where
  im : (x : X) → Image f ∋ f x

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

square : ℕ → ℕ
square n = n * n

cube  : ℕ → ℕ
cube n = n * n * n

легко заметить, что im 2 может выступить свидетельством того, что образ square содержит 4

lem-4-is-square : Image square ∋ 4
lem-4-is-square = im 2

или того, что образ cube содержит 8

lem-8-is-cube : Image cube ∋ 8
lem-8-is-cube = im 2

Перейдём теперь к построению обратной функции. Обратная к f функция может иметь в качестве области определения не все значения из Y, а только те, что принадлежат образу f. Чтобы Агда могла проконтролировать этот факт, мы должны, помимо самой функции и аргумента, передать ещё и соответствующий объект-свидетельство про этот аргумент

inv : {X Y : Set}(f : X → Y)(y : Y) → Image f ∋ y → X
inv f .(f x) (im x) = x

Теперь можно посчитать значение функции, обратной к квадрату в точке 4

my-value-is-2 : ℕ
my-value-is-2 = inv square 4 lem-4-is-square

и функции, обратной к кубу в точке 8

my-value-is-2-too : ℕ
my-value-is-2-too = inv cube 8 lem-8-is-cube

Если же мы попробуем написать

i-am-not-a-nat = inv square 5 {! !}

то Агда затребует от нас сконструировать для дырки объект ?0 : Image square ∋ 5, необитаемость которого очевидна.

Ремарка. Точечный образец в определении inv необходим для подсказки компилятору о том, что после связывания f в первом аргументе и x - в третьем единственное корректное значение второго аргумента это (f x).

Flat | Top-Level Comments Only

From:

thedeemon.livejournal.com

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

Вопрос: а можно ли сделать таблицу - массив/список, где n-ный элемент будет содержать Image f ∋ n? В ATS я подобное делал, но через хак по сути.

From:

deni-ok.livejournal.com

А что этот массив будет содержать для ненаселенных Image f ∋ n? Например, для Image square ∋ 5?

From:

thedeemon.livejournal.com

Тут я плохо сформулировал, имелось в виду скорее Image f ∋ (f n).

From:

deni-ok.livejournal.com

Ну проще всего воспользоваться квантором существования (то есть зависимой парой, если размышлять на уровне термов):

list-by-hand : List (∃ λ n → Image square ∋ n) 
list-by-hand = (4 , im 2) ∷ (1 , im 1) ∷ (0 , im 0) ∷ []

Теперь обобщаем до заказываемой пользователем длины

list-of-squares : ℕ → List (∃ λ n → Image square ∋ n) 
list-of-squares = Data.List.map ( λ x  → square x , im x) ∘ downFrom

Ну и, абстрагируясь от square, получим

list-of-images : {Y : Set}(f : ℕ → Y) → ℕ → List (∃ λ n → Image f ∋ n) 
list-of-images f = Data.List.map ( λ x  → f x , im x) ∘ downFrom

From:

thedeemon.livejournal.com

Могу ли я теперь из него получить Image f ∋ (f n), взяв n-ый элемент? А за О(1)? Фактически, мне нужна мемоизация доказательств, чтобы получать Image f ∋ (f n), не вычисляя f n каждый раз.

From:

deni-ok.livejournal.com

Расскажу, что знаю, хотя знаю немного.

Собственно в паре как раз и хранится (f n , n), если убрать все типовые украшательства. А дальше все асимптотики зависят от контейнера и бэкенда. У списка в Агдочке ты фиг возьмёшь n-ый элемент, ибо нетотально. Остаётся вектор (ну или что-то более эффективное из Х. поднять, но я это не очень пробовал).

Теперь бэкенды, говорят, что их три: (1) MAlonzo - это компиляция в Хаскель (GHC),
(2) JavaScript, (3) Epic - бэкенд общий для Idris и Epigram от Edwin Brady.

Цитата из Nils Anders Danielsson (http://comments.gmane.org/gmane.comp.lang.agda/3424):
Agda compilers are free to choose whatever evaluation order they like,
as long as they don't change the meaning of the program. The JavaScript
and Epic backends currently use strict evaluation (for inductive types),
whereas the MAlonzo backend uses lazy evaluation (modulo whatever
strictness optimisations GHC applies).

From:

thedeemon.livejournal.com

Просто мне показалось, что в типе того списка потерялось соответствие индексов содержанию. Как вообще записывается тип списка или вектора, где тип элемента зависит от его индекса?

From:

deni-ok.livejournal.com

Так тип-то для элементов один: ∃ λ n → Image square ∋ n. Он утверждает "существует n, такое что оно принадлежит образу square" (и мы их знаем много 0, 1, 4, 9, ...). А дальше мы оформляем в виде списка семейство разных доказательств этого факта, индексированное натуральными, чтобы автоматизировать добавление доказательств, а не писать их ручками по одному. Причём элементы списка - это зависимые пары из числа, населяющего образ square, и объекта-свидетельства, что высказывание верно для этого числа, например, (9 , im 3).

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

test : Image square ∋ 0 × Image square ∋ 1 × Image square ∋ 4
test = im 0 , im 1 , im 2

Обратная функция на Агде

Page Summary

Style Credit

Expand Cut Tags