The calf language is a cost-aware logical framework for studying quantitative aspects of functional programs.
This repository contains the Agda implementation of calf, as well as some case studies of varying complexity.
The source code may be viewed interactively with (semantic) syntax highlighting in the browser using the HTML files in the ./html
directory.
These files were generated by running:
agda --html --html-dir=html src/index.agda
You may want to start by opening html/index.html
.
To view a specific module M
, open html/M.html
in a web browser.
For example, open html/Examples.Sorting.Parallel.html
to view the module Examples.Sorting.Parallel
.
This implementation of calf has been tested using:
- Agda v2.6.3, with
agda-stdlib
v2.0 experimental
Installation instructions may be found in INSTALL.md
.
calf is parameterized by a cost monoid (ℂ, +, zero, ≤)
.
The formal definition, CostMonoid
, is given in Algebra.Cost
.
The definition of a parallel cost monoid (ℂ, ⊕, 𝟘, ⊗, 𝟙, ≤)
is given, as well, as ParCostMonoid
.
Some common cost monoids and parallel cost monoids are given in Algebra.Cost.Instances
; for example, ℕ-CostMonoid
simply tracks sequential cost.
Note that every ParCostMonoid
induces a CostMonoid
via the additive substructure (ℂ, ⊕, 𝟘, ≤)
.
The language itself is implemented via the following files, which are given in a dependency-respecting order.
The following modules are not parameterized:
Calf.Prelude
contains commonly-used definitions.Calf.CBPV
defines the basic dependent Call-By-Push-Value (CBPV) language, using Agdapostulate
s and rewrite rules.Calf.Directed
defines a preorder on each type, per the developments in decalf.Calf.Phase
defines the phase distinction of extension and intension:Calf.Phase.Core
postulates a proposition,ext
, for the extensional phase.Calf.Phase.Open
defines the open/extensional modality◯
forext
.Calf.Phase.Closed
defines the closed/intensional modality●
forext
.Calf.Phase.Directed
postulates the decalf law that underext
, inequality coincides with equality.Calf.Phase.Noninterference
contains theorems related to the phase distinction/noninterference.
The following modules are parameterized by a CostMonoid
:
Calf.Step
defines the computational effectstep
and the associated coherence laws via rewrite rules.
The following modules are parameterized by a ParCostMonoid
:
Calf.Parallel
defines the parallel execution operation_∥_
whose cost structure is given by the product operation of aParCostMonoid
(i.e.,_⊗_
).
In src/Calf/Data
, we provide commonly-used data types.
The following modules are not parameterized and simply internalize the associated Agda types via the meta⁺
primitive:
Calf.Data.Bool
Calf.Data.Equality
Calf.Data.List
Calf.Data.Maybe
Calf.Data.Nat
Calf.Data.Product
Calf.Data.Sum
The following modules define custom, calf-specific data types for cost analysis and are parameterized by a CostMonoid
:
Calf.Data.IsBoundedG
defines a generalized notion of cost bound,IsBoundedG
, where a bound is a program of typeF unit
. Additionally, it provides lemmas for proving the boundedness of common forms of computations.Calf.Data.IsBounded
instantiatesIsBoundedG
for cost bounds of the formstep (F unit) c (ret triv)
.Calf.Data.BoundedFunction
defines cost-bounded functions usingIsBounded
.Calf.Data.BigO
gives a definition of "big-O" asymptotic bounds viaIsBounded
. In particular, an element of the typegiven A measured-via size , f ∈𝓞(g)
(i.e., "given an input of typeA
and a size measuresize
onA
,f
is in𝓞(g)
) is a lower bound on input sizesn'
and a constant multiplierk
along with a proofh
that for all inputsx
withn' ≤ size x
,f x
is bounded byk
multiples ofg (size x)
, denotedn' ≤n⇒f[n]≤ k g[n]via h
.
We provide a variety of case studies in src/Examples
.
module Easy
- Definition of the program
id
that trivially returns its input. - Definition of the cost bound program
id/bound
, which here is the same asid
. - Theorem
id/is-bounded
showing thatid
is bounded byid/bound
. - Theorem
id/correct
stating the extensional correctness ofid
as a corollary ofid/is-bounded
. - Theorem
id/asymptotic : given nat measured-via (λ n → n) , id ∈𝓞(λ n → 0)
stating thatid
is in𝓞(0)
.
- Definition of the program
module Hard
- Definition of the program
id
that reconstructs its input via induction. - Definition of the cost bound program
id/bound
, which incursn
cost before returningn
. - Theorem
id/is-bounded
showing thatid
is bounded byid/bound
. - Theorem
id/correct
stating the extensional correctness ofid
as a corollary ofid/is-bounded
. - Theorem
id/asymptotic : given nat measured-via (λ n → n) , id ∈𝓞(λ n → n)
stating thatid
is in𝓞(n)
, wheren
is the input number.
- Definition of the program
- A proof that
Easy.id
andHard.id
are extensionally equivalent,easy≡hard : ◯ (Easy.id ≡ Hard.id)
, as a corollary of theid/correct
proofs.
- Definition of the program
sum
that sums the elements of a tree, incurring unit cost when performing each addition operation. At each node, the recursive calls are computed in parallel. - Definition of the cost bound program
sum/bound
, which incurssize t , depth t
cost before returning the sum of the tree via a value-level function. - Theorem
sum/has-cost
stating thatsum
andsum/bound
are equivalent. - Theorem
sum/is-bounded
stating that the cost ofsum t
is bounded bysum/bound
, as a corollary ofsum/has-cost
.
module Slow
- Definition of the program
exp₂
that computes the exponentation of two by its input by performing two identical recursive calls. Since two identical recursive calls are made in parallel, the work is exponential, but the span is still linear. - Definition of the cost bound program
exp₂/bound
, incurring2 ^ n - 1 , n
cost before returning result2 ^ n
. - Theorem
exp₂/is-bounded
showing thatexp₂
is bounded byexp₂/bound
. - Theorem
exp₂/correct
stating the extensional correctness ofexp₂
as a corollary ofexp₂/is-bounded
. - Theorem
exp₂/asymptotic : given nat measured-via (λ n → n) , exp₂ ∈𝓞(λ n → 2 ^ n , n)
stating thatexp₂
is in𝓞(2 ^ n , n)
.
- Definition of the program
module Fast
- Definition of the program
exp₂
which computes the exponentation of two by its input via a standard recursive algorithm. - Definition of the cost bound program
exp₂/bound
, incurringn , n
cost before returning result2 ^ n
. - Theorem
exp₂/is-bounded
showing thatexp₂
is bounded byexp₂/bound
. - Theorem
exp₂/correct
stating the extensional correctness ofexp₂
as a corollary ofexp₂/is-bounded
. - Theorem
exp₂/asymptotic : given nat measured-via (λ n → n) , exp₂ ∈𝓞(λ n → n , n)
stating thatexp₂
is in𝓞(n , n)
.
- Definition of the program
- A proof that
Slow.exp₂
andFast.exp₂
are extensionally equivalent,slow≡fast : ◯ (Slow.exp₂ ≡ Fast.exp₂)
.
First, we develop a common collection of definitions and theorems used in both sequential and parallel sorting.
Examples.Sorting.Comparable
- Record
Comparable
describing the requirements for a type to be comparable, includingh-cost
, a hypothesis that each comparison is bounded by unit cost. This serves as the cost model for sorting.
- Record
Examples.Sorting.Core
- Predicates for correctness of sorting, based on
Sorted
and the permutation relation↭
fromagda-stdlib
. The predicateIsSort sort
states thatsort
is a correct sorting algorithm. - Theorem
IsSort⇒≡
, which states that any two correct sorting algorithms are extensionally equivalent.
- Predicates for correctness of sorting, based on
Here, we use cost monoid ℕ-CostMonoid
, tracking the total number of sequential steps incurred.
Examples.Sorting.Sequential.InsertionSort
- Definition of the program
sort
implementing insertion sort. - Theorem
sort/correct : IsSort sort
verifying the correctness ofsort
. - Theorem
sort≤sort/cost/closed
stating that the cost ofsort l
is bounded bysort/cost/closed l = length l ²
. - Theorem
sort/asymptotic : given (list A) measured-via length , sort ∈𝓞(λ n → n ²)
stating thatsort
is in𝓞(n ²)
, wheren
is the length of the input list.
- Definition of the program
Examples.Sorting.Sequential.MergeSort
Examples.Sorting.Sequential.MergeSort.Split
- Definition of the program
split
, which splits a list in halves. - Theorem
split/correct
verifying correctness properties ofsplit
. - Theorem
split≤split/cost
stating that the cost ofsplit l
is bounded byzero
, since splitting a list into halves requires no comparisons.
- Definition of the program
Examples.Sorting.Sequential.MergeSort.Merge
- Definition of the program
merge
, which merges a pair of sorted lists. - Theorem
merge/correct
verifying correctness properties ofmerge
. - Theorem
merge≤merge/cost/closed
stating that the cost ofmerge (l₁ , l₂)
is bounded bylength l₁ + length l₂
.
- Definition of the program
- Definition of the program
sort
implementing merge sort. - Theorem
sort/correct : IsSort sort
verifying the correctness ofsort
. - Theorem
sort≤sort/cost/closed
stating that the cost ofsort l
is bounded bysort/cost/closed l = ⌈log₂ length l ⌉ * length l
. - Theorem
sort/asymptotic : given (list A) measured-via length , sort ∈𝓞(λ n → n * ⌈log₂ n ⌉)
stating thatsort
is in𝓞(n * ⌈log₂ n ⌉)
, wheren
is the length of the input list.
Theorem isort≡msort : ◯ (ISort.sort ≡ MSort.sort)
states that InsertionSort.sort
and MergeSort.sort
are extensionally equivalent.
Amortized data structures, via coinduction.
Examples.Amortized.Simple
provides an amortized implementation of a simple amortized stream abstract data type.Examples.Amortized.Queue
provides an implementation of amortized queues.Examples.Amortized.DynamicArray
provides an implementation of dynamically-growing arrays.
The examples introduced in decalf are included in Examples.Decalf
.
We implement and analyze the basic double
example.
We introduce the branch
and fail
primitives for nondeterminism and give the corresponding examples.
module QuickSort
includes the nondeterministic quicksort algorithm using primitives fromExamples.Sorting.Sequential.Core
.module Lookup
includes the list lookup function that fails on out-of-bounds indices.module Pervasive
includes a simple example of pervasive (non-benign) nondeterminism.
We introduce the probabilistic flip
primitive and give the corresponding example, showing how the cost of sublist
is bounded by the binomial
distribution.
We introduce the get
and set
primitives for global state and show a simple imperative program whose cost bound involves get
and set
.
We define the twice
and map
higher-order functions and analyze them under assumptions about their input costs.