Пользователь
0,0
рейтинг
1 августа 2012 в 00:04

Разработка → Верифицированный QuickSort на Agda

Доброго времени суток, уважаемый хабраюзер!

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


Формальное описание



В этой части я приведу основные типы, которые будут далее использоваться, и некоторые вспомогательные функции. Также тут будут показаны некоторые интересные синтаксические прелести Agda. Для тех, кто не сильно знаком с Agda, рекомендую посмотреть видео/слайды Яна Малаховского на встрече SPbHUG/FProg 2012-07 — это по-моему единственное введение в Agda на русском (ну я больше не встречал). Или же пролистать мануал с сайта Agda (он не большой) или этот туториал.

Определения списка

data List {a} (A : Set a) : Set a where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A

[_] : ∀ {a} {A : Set a} → A → List A
[ x ] = x ∷ []

_++_ : ∀ {a} {A : Set a} → List A → List A → List A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

Тут у нас определен список. Определение взято из стандартной библиотеки. Как видно элементами списка могут быть значения любых типов, даже типы и типы типов и так далее. Это возможно из-за использования high-order полиморфизма: вводится параметр a, который отвечает за уровень, то есть обычные типы имеют тип Set 0, Set 0 имеет тип Set 1 и т.д.
Также в этом определении видно как в Agda объявляются операторы, а именно через нижние подчеркивания, на месте которых будут аргументы. Следует заметить, что этот способ разрешает определять самые разные и очень интересные формы, как например функция, возвращающая список с одного элемента [_].

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

Тип «отсортированный список»

data Sorted {A} (_≤_ : A → A → Set) : List A → Set where
  nil : Sorted _≤_ []
  one : {x : A} → Sorted _≤_ [ x ]
  two : {x : A} → ∀ {y l} → x ≤ y → Sorted _≤_ (y ∷ l) → Sorted _≤_ (x ∷ y ∷ l)

Это определение предиката «отсортированный список». Конструкторы стоит рассматривать как аксиомы. Имеем аксиомы nil и one которые говорят, что пустой список и список с одного элемента отсортированные. Также видим, что тип Sorted зависит от предиката _≤_, который отвечает за порядок — что-то вроде функции сравнения, но зависимо-типовая (аргументы — значения обычного типа, а результатом является некоторый тип, значением которого есть доказательство). Аксиома two говорит следующее: если мы имеем доказательство того, что x ≤ y (x ≤ y — это тип, а значение типа x ≤ y — это доказательство того, что x ≤ y. См. Изоморфизм Карри-Ховарда), и доказательство того, что некоторый список с головой y — отсортированный (этим доказательством есть значение типа Sorted _≤_ (y ∷ l)), то и список x ∷ y ∷ l тоже будет отсортированный.

Тип «перестановка»

data Permutation {A} : List A → List A → Set where
  refl : ∀ {l} → Permutation l l
  perm : ∀ {l} l₁ x₁ x₂ l₂ → Permutation l (l₁ ++ x₂ ∷ x₁ ∷ l₂) → Permutation l (l₁ ++ x₁ ∷ x₂ ∷ l₂)

Тип (предикат) «перестановка». Аргументы — два списка. Вводимые аксиомы: refl — список является перестановкой самого себя; perm — если имеем доказательство, что некоторый список l есть перестановкой другого списка l₁ ++ x₂ ∷ x₁ ∷ l₂ (доказательством этого будет значение типа Permutation l (l₁ ++ x₂ ∷ x₁ ∷ l₂)), то если переставить в другом списке два произвольных элемента местами, получим, что новый список является перестановкой первого.

Тип «сумма»

data _⊎_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

Ну тут все просто — это не зависимый тип — аналог Either в Haskell.

Произведение типов

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

syntax Σ A (λ x → B) = Σ[ x ∶ A ] B

_×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b)
A × B = Σ[ _ ∶ A ] B

Это — аналог кортежа. Используется record, поскольку у данного типа может быть только один конструктор. Это определение использует зависимый тип: первый элемент — это некоторое значение, а второй — доказательство исполнения некоторого предиката на этом элементе. Но, конечно, так его использовать не обязательно, можно просто как обычный кортеж (через _×_) — тогда зависимость между элементами игнорируется. syntax разрешает задавать новые синтаксические конструкции, если простых возможностей мало.

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

sort : {A : Set} {_≤_ : A → A → Set} → (∀ x y → (x ≤ y) ⊎ (y ≤ x)) → (l : List A) → Σ[ l' ∶ List A ] (Sorted _≤_ l' × Permutation l l')

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

Реализация функции сортировки


Конечно же никакой реализации этой функции тут не будет — не то, что бы мне жалко было показывать код, мне жалко себя объяснять его. По-этому я приведу доказательства (реализации) некоторых вспомогательных функций, которые мне понадобились во время написания функции сортировки.
А рабочий исходник можно посмотреть здесь.
Использовалась Agda-2.3.1 и Standard Library-0.6
{-# OPTIONS --no-termination-check #-}

module QuickSort where

open import IO.Primitive using () renaming (putStrLn to putCoStrLn)
open import Data.String using (toCostring; String) renaming (_++_ to _+s+_)

open import Data.List
open import Data.Nat
open import Data.Nat.Show
open import Data.Sum
open import Data.Product
open import Relation.Binary.Core
open import Function

data Sorted {A} (_≤_ : A → A → Set) : List A → Set where
  nil : Sorted _≤_ []
  one : {x : A} → Sorted _≤_ [ x ]
  two : {x : A} → ∀ {y l} → x ≤ y → Sorted _≤_ (y ∷ l) → Sorted _≤_ (x ∷ y ∷ l)

data Permutation {A} : List A → List A → Set where
  refl : ∀ {l} → Permutation l l
  perm : ∀ {l} l₁ x₁ x₂ l₂ → Permutation l (l₁ ++ x₂ ∷ x₁ ∷ l₂) → Permutation l (l₁ ++ x₁ ∷ x₂ ∷ l₂)

≡-elim : ∀ {l} {A : Set l} {x y : A} → x ≡ y → (P : A → Set l) → P x → P y
≡-elim refl _ p = p

≡-sym : ∀ {l} {A : Set l} {x y : A} → x ≡ y → y ≡ x
≡-sym refl = refl

≡-trans : ∀ {l} {A : Set l} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
≡-trans refl refl = refl

++-assoc : ∀ {l} {A : Set l} (l₁ l₂ l₃ : List A) → (l₁ ++ l₂) ++ l₃ ≡ l₁ ++ (l₂ ++ l₃)
++-assoc [] l₂ l₃ = refl
++-assoc (h ∷ t) l₂ l₃ = ≡-elim (≡-sym $ ++-assoc t l₂ l₃) (λ x → h ∷ x ≡ h ∷ t ++ (l₂ ++ l₃)) refl

decNat : (x y : ℕ) → (x ≤ y) ⊎ (y ≤ x)
decNat zero y = inj₁ z≤n
decNat (suc x) (suc y) with decNat x y
... | inj₁ p = inj₁ (s≤s p)
... | inj₂ p = inj₂ (s≤s p)
decNat (suc x) zero = inj₂ z≤n

perm-trans : ∀ {A} {l₁ l₂ l₃ : List A} → Permutation l₁ l₂ → Permutation l₂ l₃ → Permutation l₁ l₃
perm-trans p refl = p
perm-trans p₁ (perm l₁ x₁ x₂ l₂ p₂) = perm l₁ x₁ x₂ l₂ $ perm-trans p₁ p₂

perm-sym : ∀ {A} {l₁ l₂ : List A} → Permutation l₁ l₂ → Permutation l₂ l₁
perm-sym refl = refl
perm-sym (perm l₁ x₁ x₂ l₂ p) = perm-trans (perm l₁ x₂ x₁ l₂ refl) (perm-sym p)

perm-del-ins-r : ∀ {A} (l₁ : List A) (x : A) (l₂ l₃ : List A) → Permutation (l₁ ++ x ∷ l₂ ++ l₃) (l₁ ++ l₂ ++ x ∷ l₃)
perm-del-ins-r l₁ x [] l₃ = refl
perm-del-ins-r l₁ x (h ∷ t) l₃ = perm-trans p₀ p₅
  where p₀ : Permutation (l₁ ++ x ∷ h ∷ t ++ l₃) (l₁ ++ h ∷ x ∷ t ++ l₃)
        p₀ = perm l₁ h x (t ++ l₃) refl

        p₁ : Permutation ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) ((l₁ ++ [ h ]) ++ t ++ x ∷ l₃)
        p₁ = perm-del-ins-r (l₁ ++ [ h ]) x t l₃

        p₂ : (l₁ ++ [ h ]) ++ t ++ x ∷ l₃ ≡ l₁ ++ h ∷ t ++ x ∷ l₃
        p₂ = ++-assoc l₁ [ h ] (t ++ x ∷ l₃)

        p₃ : (l₁ ++ [ h ]) ++ x ∷ t ++ l₃ ≡ l₁ ++ h ∷ x ∷ t ++ l₃
        p₃ = ++-assoc l₁ [ h ] (x ∷ t ++ l₃)

        p₄ : Permutation ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) (l₁ ++ h ∷ t ++ x ∷ l₃)
        p₄ = ≡-elim p₂ (λ y → Permutation ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) y) p₁

        p₅ : Permutation (l₁ ++ h ∷ x ∷ t ++ l₃) (l₁ ++ h ∷ t ++ x ∷ l₃)
        p₅ = ≡-elim p₃ (λ y → Permutation y (l₁ ++ h ∷ t ++ x ∷ l₃)) p₄

perm-del-ins-l : ∀ {A} (l₁ l₂ : List A) (x : A) (l₃ : List A) → Permutation (l₁ ++ l₂ ++ x ∷ l₃) (l₁ ++ x ∷ l₂ ++ l₃)
perm-del-ins-l l₁ l₂ x l₃ = perm-sym $ perm-del-ins-r l₁ x l₂ l₃

perm-++ : ∀ {A} {x₁ y₁ x₂ y₂ : List A} → Permutation x₁ y₁ → Permutation x₂ y₂ → Permutation (x₁ ++ x₂) (y₁ ++ y₂)
perm-++ refl refl = refl
perm-++ (perm {x₁} l₁ e₁ e₂ l₂ p) (refl {z₂}) = perm-trans p₅ p₇
  where p₁ : Permutation (x₁ ++ z₂) ((l₁ ++ e₂ ∷ e₁ ∷ l₂) ++ z₂)
        p₁ = perm-++ p refl

        p₂ : (l₁ ++ e₂ ∷ e₁ ∷ l₂) ++ z₂ ≡ l₁ ++ (e₂ ∷ e₁ ∷ l₂) ++ z₂
        p₂ = ++-assoc l₁ (e₂ ∷ e₁ ∷ l₂) z₂

        p₃ : l₁ ++ (e₂ ∷ e₁ ∷ l₂) ++ z₂ ≡ l₁ ++ e₂ ∷ (e₁ ∷ l₂) ++ z₂
        p₃ = ≡-elim (++-assoc [ e₂ ] (e₁ ∷ l₂) z₂) (λ x → l₁ ++ (e₂ ∷ e₁ ∷ l₂) ++ z₂ ≡ l₁ ++ x) refl

        p₄ : l₁ ++ e₂ ∷ (e₁ ∷ l₂) ++ z₂ ≡ l₁ ++ e₂ ∷ e₁ ∷ l₂ ++ z₂
        p₄ = ≡-elim (++-assoc [ e₁ ] l₂ z₂) (λ x → l₁ ++ e₂ ∷ (e₁ ∷ l₂) ++ z₂ ≡ l₁ ++ e₂ ∷ x) refl

        g₂ : (l₁ ++ e₁ ∷ e₂ ∷ l₂) ++ z₂ ≡ l₁ ++ (e₁ ∷ e₂ ∷ l₂) ++ z₂
        g₂ = ++-assoc l₁ (e₁ ∷ e₂ ∷ l₂) z₂

        g₃ : l₁ ++ (e₁ ∷ e₂ ∷ l₂) ++ z₂ ≡ l₁ ++ e₁ ∷ (e₂ ∷ l₂) ++ z₂
        g₃ = ≡-elim (++-assoc [ e₁ ] (e₂ ∷ l₂) z₂) (λ x → l₁ ++ (e₁ ∷ e₂ ∷ l₂) ++ z₂ ≡ l₁ ++ x) refl

        g₄ : l₁ ++ e₁ ∷ (e₂ ∷ l₂) ++ z₂ ≡ l₁ ++ e₁ ∷ e₂ ∷ l₂ ++ z₂
        g₄ = ≡-elim (++-assoc [ e₂ ] l₂ z₂) (λ x → l₁ ++ e₁ ∷ (e₂ ∷ l₂) ++ z₂ ≡ l₁ ++ e₁ ∷ x) refl

        p₅ : Permutation (x₁ ++ z₂) (l₁ ++ e₂ ∷ e₁ ∷ l₂ ++ z₂)
        p₅ = ≡-elim (≡-trans p₂ $ ≡-trans p₃ p₄) (Permutation (x₁ ++ z₂)) p₁

        p₆ : Permutation (l₁ ++ e₂ ∷ e₁ ∷ l₂ ++ z₂) (l₁ ++ e₁ ∷ e₂ ∷ l₂ ++ z₂)
        p₆ = perm l₁ e₁ e₂ (l₂ ++ z₂) refl

        p₇ : Permutation (l₁ ++ e₂ ∷ e₁ ∷ l₂ ++ z₂) ((l₁ ++ e₁ ∷ e₂ ∷ l₂) ++ z₂)
        p₇ = ≡-elim (≡-sym $ ≡-trans g₂ $ ≡-trans g₃ g₄) (Permutation (l₁ ++ e₂ ∷ e₁ ∷ l₂ ++ z₂)) p₆

perm-++ {_} {x₁} {y₁} .{_} .{_} p₁ (perm {x₂} l₁ e₁ e₂ l₂ p₂) = ≡-elim p₇ (Permutation (x₁ ++ x₂)) p₆
  where p' : Permutation (x₁ ++ x₂) (y₁ ++ l₁ ++ e₂ ∷ e₁ ∷ l₂)
        p' = perm-++ p₁ p₂

        p₃ : y₁ ++ l₁ ++ e₂ ∷ e₁ ∷ l₂ ≡ (y₁ ++ l₁) ++ e₂ ∷ e₁ ∷ l₂
        p₃ = ≡-sym $ ++-assoc y₁ l₁ (e₂ ∷ e₁ ∷ l₂)

        p₄ : Permutation (x₁ ++ x₂) ((y₁ ++ l₁) ++ e₂ ∷ e₁ ∷ l₂)
        p₄ = ≡-elim p₃ (Permutation (x₁ ++ x₂)) p'

        p₅ : Permutation ((y₁ ++ l₁) ++ e₂ ∷ e₁ ∷ l₂) ((y₁ ++ l₁) ++ e₁ ∷ e₂ ∷ l₂)
        p₅ = perm (y₁ ++ l₁) e₁ e₂ l₂ refl

        p₆ : Permutation (x₁ ++ x₂) ((y₁ ++ l₁) ++ e₁ ∷ e₂ ∷ l₂)
        p₆ = perm-trans p₄ p₅

        p₇ : (y₁ ++ l₁) ++ e₁ ∷ e₂ ∷ l₂ ≡ y₁ ++ l₁ ++ e₁ ∷ e₂ ∷ l₂
        p₇ = ++-assoc y₁ l₁ (e₁ ∷ e₂ ∷ l₂)

++-[] : ∀ {l} {A : Set l} (l : List A) → l ++ [] ≡ l
++-[] [] = refl
++-[] (h ∷ t) = ≡-trans p₀ p₁
  where p₀ : (h ∷ t) ++ [] ≡ h ∷ t ++ []
        p₀ = ++-assoc [ h ] t []

        p₁ : h ∷ t ++ [] ≡ h ∷ t
        p₁ = ≡-elim (++-[] t) (λ x → h ∷ t ++ [] ≡ h ∷ x) refl

data ConstrainedList {A} (P : A → Set) : List A → Set where
  []  : ConstrainedList P []
  _∷_ : {x : A} {xs : List A} (p : P x) → ConstrainedList P xs → ConstrainedList P (x ∷ xs)

infix 2 _∈_

data _∈_ {A} : A → List A → Set where
  exact : ∀ h t → h ∈ h ∷ t
  cons : ∀ h {x l} → x ∈ l → x ∈ h ∷ l

create-∈ : ∀ {A} (l₁ : List A) (x : A) (l₂ : List A) → x ∈ (l₁ ++ x ∷ l₂)
create-∈ [] x l₂ = exact x l₂
create-∈ (h₁ ∷ t₁) x l₂ = cons h₁ $ create-∈ t₁ x l₂

perm-∈ : ∀ {A l l'} {x : A} → x ∈ l → Permutation l' l → x ∈ l'
perm-∈ p refl = p
perm-∈ {A} .{l₁ ++ x₁ ∷ x₂ ∷ l₂} {l'} {x} p₁ (perm l₁ x₁ x₂ l₂ p₂) = perm-∈ (loop l₁ x₁ x₂ l₂ p₁) p₂
  where loop : ∀ l₁ x₁ x₂ l₂ → x ∈ l₁ ++ x₁ ∷ x₂ ∷ l₂ → x ∈ l₁ ++ x₂ ∷ x₁ ∷ l₂
        loop [] .x x₂ l₂ (exact .x .(x₂ ∷ l₂)) = cons x₂ $ exact x l₂
        loop [] .x₁ .x .l₂ (cons x₁ (exact .x l₂)) = exact x (x₁ ∷ l₂)
        loop [] .x₁ .x₂ l₂ (cons x₁ (cons x₂ p)) = cons x₂ $ cons x₁ p
        loop (.x ∷ t₁) x₁ x₂ l₂ (exact .x .(t₁ ++ x₁ ∷ x₂ ∷ l₂)) = exact x (t₁ ++ x₂ ∷ x₁ ∷ l₂)
        loop (.h₁ ∷ t₁) x₁ x₂ l₂ (cons h₁ p) = cons h₁ $ loop t₁ x₁ x₂ l₂ p

constr-∈ : ∀ {A l} {x : A} → ∀ {P} → ConstrainedList P l → x ∈ l → P x
constr-∈ [] ()
constr-∈ (p ∷ _) (exact _ _) = p
constr-∈ (_ ∷ cl) (cons _ p) = constr-∈ cl p

sortedHelper₂ : ∀ {A _≤_} {h : A} → ∀ {l'} → Sorted _≤_ l' → ∀ {l} → Permutation l l' → ConstrainedList (λ x → x ≤ h) l → ∀ {g'} → Sorted _≤_ (h ∷ g') → Sorted _≤_ (l' ++ h ∷ g')
sortedHelper₂ {_} {_≤_} {h} {l'} sl' pll' cl {g'} sg' = loop [] l' refl sl'
  where loop : ∀ l₁ l₂ → l₁ ++ l₂ ≡ l' → Sorted _≤_ l₂ → Sorted _≤_ (l₂ ++ h ∷ g')
        loop _ .[] _ nil = sg'
        loop l₁ .(x ∷ []) p (one {x}) = two (constr-∈ cl $ perm-∈ x∈l' pll') sg'
                where x∈l' : x ∈ l'
                      x∈l' = ≡-elim p (λ l → x ∈ l) (create-∈ l₁ x [])
        loop l₁ .(x ∷ y ∷ l) p≡ (two {x} {y} {l} x≤y ps) = two x≤y $ loop (l₁ ++ [ x ]) (y ∷ l) p' ps
                where p' : (l₁ ++ [ x ]) ++ y ∷ l ≡ l'
                      p' = ≡-trans (++-assoc l₁ [ x ] (y ∷ l)) p≡

sortedHelper₁ : ∀ {A _≤_} {h : A} → ∀ {l'} → Sorted _≤_ l' → ∀ {l} → Permutation l l' → ConstrainedList (λ x → x ≤ h) l → ∀ {g'} → Sorted _≤_ g' → ∀ {g} → Permutation g g' → ConstrainedList (λ x → h ≤ x) g → Sorted _≤_ (l' ++ h ∷ g')
sortedHelper₁ sl' pll' cl nil _ _ = sortedHelper₂ sl' pll' cl one
sortedHelper₁ sl' pll' cl {h ∷ t} sg' pgg' cg = sortedHelper₂ sl' pll' cl $ two (constr-∈ cg $ perm-∈ (exact h t) pgg') sg'

quickSort : {A : Set} {_≤_ : A → A → Set} → (∀ x y → (x ≤ y) ⊎ (y ≤ x)) → (l : List A) → Σ[ l' ∶ List A ] (Sorted _≤_ l' × Permutation l l')
quickSort _ [] = [] , nil , refl
quickSort {A} {_≤_} _≤?_ (h ∷ t) = loop t [] [] [] [] refl
  where loop : ∀ i l g → ConstrainedList (λ x → x ≤ h) l → ConstrainedList (λ x → h ≤ x) g → Permutation t ((l ++ g) ++ i) → Σ[ l' ∶ List A ] (Sorted _≤_ l' × Permutation (h ∷ t) l')
        loop [] l g cl cg p  = l' ++ h ∷ g' , sortedHelper₁ sl' pll' cl sg' pgg' cg , perm-trans p₃ p₄
          where lSort = quickSort _≤?_ l
                gSort = quickSort _≤?_ g
                l' = proj₁ lSort
                g' = proj₁ gSort
                sl' = proj₁ $ proj₂ lSort
                sg' = proj₁ $ proj₂ gSort
                pll' = proj₂ $ proj₂ lSort
                pgg' = proj₂ $ proj₂ gSort

                p₁ : Permutation (l ++ g) (l' ++ g')
                p₁ = perm-++ pll' pgg'

                p₂ : Permutation t (l' ++ g')
                p₂ = perm-trans (≡-elim (++-[] (l ++ g)) (λ x → Permutation t x) p) p₁

                p₃ : Permutation (h ∷ t) (h ∷ l' ++ g')
                p₃ = perm-++ (refl {_} {[ h ]}) p₂

                p₄ : Permutation (h ∷ l' ++ g') (l' ++ h ∷ g')
                p₄ = perm-del-ins-r [] h l' g'
        loop (h' ∷ t) l g cl cg p with h' ≤? h
        ... | inj₁ h'≤h = loop t (h' ∷ l) g (h'≤h ∷ cl) cg (perm-trans p p')
                        where p' : Permutation ((l ++ g) ++ h' ∷ t) (h' ∷ (l ++ g) ++ t)
                              p' = perm-del-ins-l [] (l ++ g) h' t
        ... | inj₂ h≤h' = loop t l (h' ∷ g) cl (h≤h' ∷ cg) (perm-trans p p')
                        where p₁ : l ++ g ++ h' ∷ t ≡ (l ++ g) ++ h' ∷ t
                              p₁ = ≡-sym $ ++-assoc l g (h' ∷ t)

                              p₂ : l ++ (h' ∷ g) ++ t ≡ (l ++ h' ∷ g) ++ t
                              p₂ = ≡-sym $ ++-assoc l (h' ∷ g) t

                              p₃ : (h' ∷ g) ++ t ≡ h' ∷ g ++ t
                              p₃ = ++-assoc [ h' ] g t

                              p₄ : l ++ h' ∷ g ++ t ≡ l ++ (h' ∷ g) ++ t
                              p₄ = ≡-sym $ ≡-elim p₃ (λ x → l ++ x ≡ l ++ h' ∷ g ++ t) refl

                              p₅ : Permutation (l ++ g ++ h' ∷ t) (l ++ h' ∷ g ++ t)
                              p₅ = perm-del-ins-l l g h' t

                              p₆ : Permutation ((l ++ g) ++ h' ∷ t) (l ++ h' ∷ g ++ t)
                              p₆ = ≡-elim p₁ (λ x → Permutation x (l ++ h' ∷ g ++ t)) p₅

                              p' : Permutation ((l ++ g) ++ h' ∷ t) ((l ++ h' ∷ g) ++ t)
                              p' = ≡-elim (≡-trans p₄ p₂) (λ x → Permutation ((l ++ g) ++ h' ∷ t) x) p₆

showl : List ℕ → String
showl [] = "[]"
showl (h ∷ t) = show h +s+ "∷" +s+ showl t

l₁ : List ℕ
l₁ = 19 ∷ 6 ∷ 13 ∷ 2 ∷ 8 ∷ 15 ∷ 1 ∷ 10 ∷ 11 ∷ 2 ∷ 17 ∷ 4 ∷ [ 3 ]
l₂ = quickSort decNat l₁

main = putCoStrLn ∘ toCostring $ showl $ proj₁ l₂



Пропозициональная эквивалентность

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

≡-cong : ∀ {a b} {A : Set a} {B : Set b} {x y} → x ≡ y → (f : A → B) → f x ≡ f y
≡-cong refl _ = refl

≡-elim : ∀ {l} {A : Set l} {x y : A} → x ≡ y → (P : A → Set l) → P x → P y
≡-elim refl _ p = p

≡-sym : ∀ {l} {A : Set l} {x y : A} → x ≡ y → y ≡ x
≡-sym refl = refl

≡-trans : ∀ {l} {A : Set l} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
≡-trans refl refl = refl

Как видим тут все просто: только одна аксиома, которая говорит, что два объекта равны, если они одно и то же. Также здесь определены вспомогательные функции для работой с доказательствами эквивалентности. Я думаю, тут более-мение все понятно. Поясню лишь на примере ≡-elim: единственным значением аргумента типа x ≡ y можеть быть refl, у которого есть один неявный параметр, который в строке ≡-elim refl _ p равный одновременно и x и y, по-этому и значение p имеет одновременно тип и P x и P y, а если значение p имеет тип P y, то в этой ситуации это и будет результат функции ≡-elim.

Ассоциативность операции конкатенации

++-assoc : ∀ {l} {A : Set l} (l₁ l₂ l₃ : List A) → (l₁ ++ l₂) ++ l₃ ≡ l₁ ++ (l₂ ++ l₃)
++-assoc [] l₂ l₃ = refl
++-assoc (h ∷ t) l₂ l₃ = ≡-cong (++-assoc t l₂ l₃) (λ x → h ∷ x)

Тут $ — ни что иное как оператор аппликации, как в Haskell. Из определения понятно, что эта функция (или можно сказать лемма) доказывает для трех произвольных списков ассоциативность операции конкатенации. Хочу заметить, что во время компиляции термы частично редуцируются с использованием существующих определений. В данной функции происходит следующее:
терм
≡-cong (++-assoc t l₂ l₃) (λ x → h ∷ x)

имеет тип
h ∷ (t ++ l₂) ++ l₃ ≡ h ∷ t ++ (l₂ ++ l₃)

а нам нужен тип
(l₁ ++ l₂) ++ l₃ ≡ l₁ ++ (l₂ ++ l₃)

или
((h ∷ t) ++ l₂) ++ l₃ ≡ (h ∷ t) ++ (l₂ ++ l₃)

это с учетом, что
l₁ = h ∷ t

далее компилятор, используя определение конкатенации редуцирует данные термы к некоторому общему виду.
Попробуйте с терма, используя определение конкатенации,
((h ∷ t) ++ l₂) ++ l₃ ≡ (h ∷ t) ++ (l₂ ++ l₃)

получить терм
h ∷ (t ++ l₂) ++ l₃ ≡ h ∷ t ++ (l₂ ++ l₃)

Также нужно учитывать, что операция конкатенации правоассоциативна — но это для понимания не принципиально.

Транзитивность и симметричность перестановки

perm-trans : ∀ {A} {l₁ l₂ l₃ : List A} → Permutation l₁ l₂ → Permutation l₂ l₃ → Permutation l₁ l₃
perm-trans p refl = p
perm-trans p₁ (perm l₁ x₁ x₂ l₂ p₂) = perm l₁ x₁ x₂ l₂ $ perm-trans p₁ p₂

perm-sym : ∀ {A} {l₁ l₂ : List A} → Permutation l₁ l₂ → Permutation l₂ l₁
perm-sym refl = refl
perm-sym (perm l₁ x₁ x₂ l₂ p) = perm-trans (perm l₁ x₂ x₁ l₂ refl) (perm-sym p)


«Длинная» перестановка влево и вправо

perm-del-ins-r : ∀ {A} (l₁ : List A) (x : A) (l₂ l₃ : List A) → Permutation (l₁ ++ x ∷ l₂ ++ l₃) (l₁ ++ l₂ ++ x ∷ l₃)
perm-del-ins-r l₁ x [] l₃ = refl
perm-del-ins-r l₁ x (h ∷ t) l₃ = perm-trans p₀ p₅
  where p₀ : Permutation (l₁ ++ x ∷ h ∷ t ++ l₃) (l₁ ++ h ∷ x ∷ t ++ l₃)
        p₀ = perm l₁ h x (t ++ l₃) refl

        p₁ : Permutation ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) ((l₁ ++ [ h ]) ++ t ++ x ∷ l₃)
        p₁ = perm-del-ins-r (l₁ ++ [ h ]) x t l₃

        p₂ : (l₁ ++ [ h ]) ++ t ++ x ∷ l₃ ≡ l₁ ++ h ∷ t ++ x ∷ l₃
        p₂ = ++-assoc l₁ [ h ] (t ++ x ∷ l₃)

        p₃ : (l₁ ++ [ h ]) ++ x ∷ t ++ l₃ ≡ l₁ ++ h ∷ x ∷ t ++ l₃
        p₃ = ++-assoc l₁ [ h ] (x ∷ t ++ l₃)

        p₄ : Permutation ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) (l₁ ++ h ∷ t ++ x ∷ l₃)
        p₄ = ≡-elim p₂ (λ y → Permutation ((l₁ ++ [ h ]) ++ x ∷ t ++ l₃) y) p₁

        p₅ : Permutation (l₁ ++ h ∷ x ∷ t ++ l₃) (l₁ ++ h ∷ t ++ x ∷ l₃)
        p₅ = ≡-elim p₃ (λ y → Permutation y (l₁ ++ h ∷ t ++ x ∷ l₃)) p₄

perm-del-ins-l : ∀ {A} (l₁ l₂ : List A) (x : A) (l₃ : List A) → Permutation (l₁ ++ l₂ ++ x ∷ l₃) (l₁ ++ x ∷ l₂ ++ l₃)
perm-del-ins-l l₁ l₂ x l₃ = perm-sym $ perm-del-ins-r l₁ x l₂ l₃

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

Порядок на натуральных числах

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

data _≤_ : ℕ → ℕ → Set where
  z≤n : ∀ {n} → zero  ≤ n
  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n

decNat : (x y : ℕ) → (x ≤ y) ⊎ (y ≤ x)
decNat zero y = inj₁ z≤n
decNat (suc x) (suc y) with decNat x y
... | inj₁ p = inj₁ (s≤s p)
... | inj₂ p = inj₂ (s≤s p)
decNat (suc x) zero = inj₂ z≤n


Ну и наконец разрешающая процедура для определения порядка на натуральных числах. (Обратите внимание как именуются переменные — все, что без пробелов есть терм.) Используется предикат _≤_. Вводятся две аксиомы, одна из которых говорит, что любое число больше или равно нуля, а другая, что если одно число больше равно другого, то соотношение сохранится, если к ним прибавить по единице.
Также тут используется конструкция with — но я думаю ее использование предельно ясно.

Вот и все:)

От себя скажу, что писать такие программы ну очень интересно.
Дмитрий @dima_mendeleev
карма
–1,0
рейтинг 0,0
Реклама помогает поддерживать и развивать наши сервисы

Подробнее
Реклама

Самое читаемое Разработка

Комментарии (23)

  • +2
    Ух ты, статья по Agda, спасибо большое!

    Интересно бы попробовать доказать аналогичное на обычной сортировке. Т.е. для функций
    sort : ∀ {l} {a : Set l} → (a → a → bool) → list a → list a
    sorted : ∀ {l} {a : Set l} → (a → a → bool) → list a → bool
    

    доказать утверждение
    sort-sorts : ∀ {l} {a : Set l} {cmp : a → a → bool} {xs : list a} → sorted (sort xs) ≡ true
    
    • +1
      В данной ситуации обязательно нужно иметь определения функций sort и sorted, потому как с описанного типа много информации получить нельзя. И после уже можно проступать к доказательству — это весьма реально.
    • +2
      Как минимум, в sort-sorts необходимо передавать еще доказательство того, что cmp образует полный порядок
      • 0
        Вообще то не обязательно. На эти функции нужно смотреть абстрагируясь от названий: задача доказать — а это значить построить терм. Обязательное тут, как я писал — это определения функций sort и sorted, пока этого не будет, ничего точно сказать нельзя. Вот например если так:
        -- sort - любой
        sorted _ _ = true
        sort-sorts = refl
        

        То есть без определений никак.
        • +1
          Без доказательства что cmp образует линейный порядок тоже ничего не получится — иначе отсортированная последовательность может не существовать (например если cmp всегда возвращает false)

          А то что без определений никак это очевидно)
          • 0
            Вы не абстрагируетесь… Забудьте о том, что это функции сортировки.
            > Без доказательства что cmp образует линейный порядок тоже ничего не получится
            Это нельзя утверждать — и доказательство этому мой пример с предыдущего комментария.
            • 0
              Ну мы всё-таки о вполне понятном и очевидном sorted, написать который можно разными путями, но это никак не просто true. И, на всякий случай, такой вариант тоже исключается
              sorted cmp xs = xs == sort cmp xs
              

              по понятным причинам.
              • 0
                Все правильно, но все же мой пример не единственный при котором не нужно доказательство линейного порядка.
                То есть, я только хочу сказать, что следующее утверждать нельзя:
                > Без доказательства что cmp образует линейный порядок тоже ничего не получится
            • +1
              Я рассматриваю случай когда реализации sort и sorted действительно соответствуют своим названиям — и утверждаю что в этом случае для доказательства их корректности обязательно потребуется еще один аргумент.
              • 0
                В этом случае согласен. Наверное зависимые типы и суровая жизнь заставили меня больше верить типу функции чем ее названию.
                Действительно без определенных ограничений на функцию сравнения ничего не получится.
              • 0
                А как такой вариант?
                sort _ [] = []
                sort _<_ (h :: t) = filter (\x -> x < h) t ++ h ++ filter (\x -> not (x < h)) t
                
                sorted _ []  = true
                sorted _ (_ :: [])  = true
                sorted _<_ (x :: y :: t)  = ((x < y) || not (y < x)) && sorted _<_ (y :: t)
                
  • +8
    Как вы набираете тест программы? Особенно эти кванторы, нижние индексы?
    • +2
      Для agda есть замечательный emacs agda-mode, в нем есть сочетания для набора математических символов и goals, существенно облегчающие разработку/доказательства.
      Goal, грубо говоря, «дырка» в программе, для которой agda показывает необходимый тип выражения и все выражения которые есть в контексте с их типами.
    • +2
      … пишешь \_1 получается ₁, пишешь \<=, получается ≤, пишешь \all или \forall, получается ∀.
      Еще классно, что в agda-mode есть подсказки, типа intellisense.
      • 0
        Почти TeX :)
        • 0
          Это и есть ТеХ ;)
          А еще Unicode можно:
          \название_символа
          
  • +2
    github.com/winger/agda-stuff/blob/master/Splay.agda — реализация splay-дерева с доказательствами, правда пока есть пара пробелов, не хватает времени дописать
  • 0
    «Прочитав несколько книг по типизированном лямбда исчисление»

    «И я шепчу дрожащие губами
    Велик могучим русский языка» (с) А. Иванов

    Возможно:
    «Прочитав несколько книг по типизированному лямбда исчислению»?
    • 0
      Кэп в ударе?
      • 0
        Простите, я имел ввиду, спасибо:)
    • 0
      Простите, это сюда… пиво=)
  • +1
    Можно ещё взглянуть на статью Why Dependent Types Matter МакБрайда et al, там приводится верифицированный merge sort на Epigram.
    • 0
      Спасибо! Интересный материал, у меня кстати был выбор, что писать: merge или quck sort.
      Но если честно мне синтаксис Agda больше нравиться чем Epigram. На самом деле я не сразу на Agda подсел. Была попытка с ATS, и длительное время сидел на Coq. Но Agda все же привлекает больше всего. Плюс заманчивая возможность через Haskell подключить C/C++ — боюсь даже представить, что может выйти.

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