Partiality

How can we model partial or non-terminating computations?

{-# OPTIONS --cubical-compatible --allow-unsolved-metas #-}
module _ where
private
  variable
    A B C : Set

Maybe

open import Data.Bool as B using (Bool; true; false; _∨_; _≟_)
open import Data.Unit
open import Data.Sum
open import Data.Maybe as Maybe renaming (_>>=_ to Maybe-bind)
open import Data.Nat
open import Data.Product
open import Data.List
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (Dec; yes; no; dec⇒maybe)
open import Function.Base

_⇀_ : Set → Set → Set
A ⇀ B = A → Maybe B

Maybe′ : Set → Set
Maybe′ B = ⊤ ⊎ B
Maybe′′ : Set → Set
Maybe′′ B = Σ[ l ∈ List B ] length l ≤ 

-- index ₘ = Maybe

_∘ₘ_ :  (B ⇀ C) → (A ⇀ B) → (A ⇀ C)
g ∘ₘ f = λ a → case (f a) of λ
  { (just b) → g b
  ; nothing → nothing
  }

Is-definedₘ : (A ⇀ B) → A → Set
Is-definedₘ f = (Is-just ∘ f)
  -- Σ[ a ∈ A ] ∃[ b ] f a ≡ just b

However, being defined is a decidable predicate on A, so we need a different description of partiality for modelling non-termination:

Spans

module version1 where
  record _⊇⟶_ (A B : Set) : Set₁ where
    field
      Is-defined : A → Set
      app : Σ A Is-defined → B

  guess : ∀ (B : Set) → ⊤ ⊇⟶ B
  guess B = record
    { Is-defined = λ _ → B
    ; app = λ { (_ , b) → b }
    }

record _⊇⟶_ (A B : Set) : Set₁ where
  field
    Is-defined : A → Set
    app : Σ A Is-defined → B
    well-defined : ∀ {x} {y} → proj₁ x ≡ proj₁ y
                             → app x ≡ app y
from-Maybe : (A ⇀ B) → (A ⊇⟶ B)
from-Maybe {A = A} {B = B} f =
  record
  { Is-defined = Is-definedₘ f
  ; app = app
    -- alternatively: λ { (x , just-b) → to-witness just-b }
  ; well-defined = well-defined
  }
  where
    app : Σ A (Is-definedₘ f) → B
    app (a , def-a) with (f a)
    ... | just b = b

    well-defined : {x y : Σ A (Is-definedₘ f)} →
                   proj₁ x ≡ proj₁ y → app x ≡ app y
    well-defined {(x , _)} {(_ , _)} refl with (f x)
    ... | just x₁ = refl

_∘ₚ_ : (B ⊇⟶ C) → (A ⊇⟶ B)  → (A ⊇⟶ C)
_∘ₚ_ {A = A} g f = record
  { Is-defined = Is-defined
  ; app = λ { (a , f[a]↓ , g[f[a]]↓) → g.app (f.app (a , f[a]↓) , g[f[a]]↓) }
  ; well-defined = g.well-defined ∘ f.well-defined
  }
  where
    module f = _⊇⟶_ f
    module g = _⊇⟶_ g
    Is-defined : A → Set
    Is-defined a = Σ[ f[a]↓ ∈ (f.Is-defined a) ]
                 g.Is-defined (f.app (a , f[a]↓))

[End of lecture on 6 July 2026]

Step-Indexing

is-mono : (ℕ → Maybe A) → Set
is-mono f = ∀ n → Is-just (f n) → f (suc n) ≡ f n

record Step-Indexed (A : Set) : Set where
  field
    f : ℕ → Maybe A
    f-mono :  is-mono f

_⊑ₘ_ : Maybe A → Maybe A → Set
x ⊑ₘ y = Is-just x → x ≡ y

monotone : (ℕ → Maybe A) → Set
monotone f = ∀ m n → m ≤ n → f m ⊑ₘ f n

contains-true? : (s s' : ℕ → Bool) → Step-Indexed (∃[ k ] s k ≡ s' k)
contains-true? s s' = record
  { f = f
  ; f-mono = f-mono
  }
  where
    f : ℕ → Maybe (∃[ k ] s k ≡ s' k)
    f zero = nothing
    f (suc k) =
      (f k) <∣> Maybe.map (k ,_) (dec⇒maybe (s k B.≟ s' k)) 
    f-mono : is-mono f
    f-mono n Is-just[f[n]] with (f n)
    ... | just (k , sk≡s'k) = refl

The results on Streams and Delay were moved to Delay.html. [End of lecture on 9 July 2026]

Additional lemmas

open import Data.Maybe.Relation.Unary.Any using (just)
open import Data.Maybe.Properties using (just-injective)
open import Data.Nat.Properties using (≤⇒≤′; m≤m⊔n; m≤n⊔m)
open import Data.Maybe.Relation.Unary.Any using (Any; just)


⊑ₘ-trans : ∀ { x y z : Maybe A } →  x ⊑ₘ y → y ⊑ₘ z → x ⊑ₘ z
⊑ₘ-trans {x = just x} x⊑ₘy y⊑ₘz x-is-just with (x⊑ₘy x-is-just)
... | refl = y⊑ₘz x-is-just

monotone′ : (ℕ → Maybe A) → Set
monotone′ f = ∀ {m} {n} → m ≤′ n → f m ⊑ₘ f n

is-mono⇒monotone′ : ∀ {f : ℕ → Maybe A} → is-mono f → monotone′ f
is-mono⇒monotone′ f-mono (≤′-reflexive refl) f-m-just = refl
is-mono⇒monotone′ f-mono {n = suc n} (≤′-step m≤n) f-m-just =
  ⊑ₘ-trans (is-mono⇒monotone′ f-mono m≤n) (sym ∘ f-mono n) f-m-just

is-mono⇒monotone : ∀ {f : ℕ → Maybe A} → is-mono f → monotone f
is-mono⇒monotone f-mono m n = is-mono⇒monotone′ f-mono ∘ ≤⇒≤′

module do-Step-Indexed where
  _>>=_ : Step-Indexed A → (A → Step-Indexed B) → Step-Indexed B
  _>>=_ {B = B} stepA g = record
    { f = f
    ; f-mono = f-mono
    }
    where
      module stepA = Step-Indexed stepA
      f : ℕ → Maybe B
      f k = Maybe-bind (stepA.f k) (λ a → Step-Indexed.f (g a) k)

      f-mono : is-mono f
      f-mono n Is-just[f[n]] with stepA.f n | stepA.f-mono n
      ... | just a | mono-n rewrite mono-n (just tt) =
        Step-Indexed.f-mono (g a) n Is-just[f[n]]

  return : A → Step-Indexed A
  return a = record
    { f = λ _ → just a
    ; f-mono = λ n x → refl
    }

  stepped-pair : Step-Indexed A
                 → Step-Indexed B
                 → Step-Indexed (A × B)
  stepped-pair {A = A} stepA stepB = do
    a ← stepA
    b ← stepB
    return (a , b)

mono⇒functional : ∀ {f : ℕ → Maybe A} → is-mono f
                  → ∀ {m} {v} → f m ≡ just v
                  → ∀ {n} {w} → f n ≡ just w
                  → v ≡ w
mono⇒functional {f = f} f-mono {m} {v} f[m]↓ {n} {w} f[n]↓ =
  just-injective (begin
    just v     ≡⟨ f[m]↓ ⟨
    f m        ≡⟨ f-monotone _ _ (m≤m⊔n m n) (subst Is-just (sym f[m]↓) (just tt)) ⟩
    f (m ⊔ n)  ≡⟨ f-monotone _ _ (m≤n⊔m m n) (subst Is-just (sym f[n]↓) (just tt)) ⟨
    f n        ≡⟨ f[n]↓ ⟩
    just w     ∎)
  where
    open ≡-Reasoning
    f-monotone : monotone f
    f-monotone _ _ = is-mono⇒monotone′ f-mono ∘ ≤⇒≤′

Step-Indexed-functional : {M₁ M₂ : Step-Indexed B}
                          {m n : ℕ} {v : B} {w : B}
                        → M₁ ≡ M₂
                        → Step-Indexed.f M₁ m ≡ just v
                        → Step-Indexed.f M₂ n ≡ just w
                        → v ≡ w
Step-Indexed-functional {M₁ = M} refl eq1 eq2 =
  mono⇒functional (Step-Indexed.f-mono M) eq1 eq2

Agda Quellcode herunterladen