From equations to distinctions:Two interpretations of effectful computations
Niels Voorneveld
Tallinn University of Technology

August 31st, 2020
MSFP 2020

MSFP 2020

Niels Voorneveld(Taltech)

From equations to distinctions for effectful computations

Introduction
Two sides to program equivalence. For any two programs, either:
I the two programs ‘simulate’ eachother,
I or there is an observable difference between the two programs.
Program equivalence for programs with algebraic effects starts withspecifying the behaviour of effects at base type in one of two ways:
I choosing axiomatic equations and inequations,
I or formulating distinction tests by EM-algebra.

Basic relation
Higher-order

MSFP 2020

Equations
Equational axioms
Applicative bisimilarity

Niels Voorneveld(Taltech)Distinctions
EM-algebra
Quantitative logic

From equations to distinctions for effectful computations

Effect operations

Algebraic effect operations:
Probabilistic choice
Global store
Cost counter

por : 2
lookup : Ntick : 1

updaten : 1

Property satisfaction tokens:
Failure (e.g. divergence)
Success (e.g. final termination)

MSFP 2020

Niels Voorneveld(Taltech)⊥:0>:0From equations to distinctions for effectful computations

Effect trees
Possibly infinite effects trees (monad T ):porupdate0lookup0>

tick12⊥⊥...

>
Monad in the category of sets and preorders.
Syntactic order where:∀t ∈ TX . ⊥ ≤ t ≤ >MSFP 2020

Niels Voorneveld(Taltech)

From equations to distinctions for effectful computations

Equations
Given a countable set of variables V, a tree e ∈ T V is an algebraic
expression.
Axiomatic effect-specific (in)equations A ⊆ (T V)2
Probability:por(x, x) =por(x, y ) =por(por(x, y ), por(z, w )) =por(x, por(x, por(x, ..))) =xpor(y , x)por(por(x, z), por(y , w ))x

Global store:upi (upj (x)) =upi (lo(x0 , x1 , . . . )) =lo(up0 (x0 ), up1 (x1 ), . . . ) =lo(x, x, . . . ) =upj (x)upi (xi )lo(x0 , x1 , . . . )x

MSFP 2020

Niels Voorneveld(Taltech)

From equations to distinctions for effectful computations

Algebraic relation
Induced algebraic relation RA ⊆ (T V)2 :- Reflexive and transitive- Compositional (and substitutional)- Preserves syntactic order- Admissable
Simple derivation in global store:updatei (>)≥updatei (updatej (>))

=updatej (>)> = lookup(>, >, >, . . . )= lookup(update0 (>), update1 (>), update2 (>), . . . )= lookup(updatei (>), updatei (>), updatei (>), . . . )= updatei (>)

MSFP 2020

Niels Voorneveld(Taltech)

From equations to distinctions for effectful computations

Algebras
Definition
An algebra α : T O → O of a monad T = (T , η, µ) is anEM-algebra if:OηO/ TOαOTT OµOTα /TOαα/OTO

We work in the category of preorders, with truth space O.
The algebra lifts each predicate P : X → O to α ◦ TP : TX → O.
Induces an algebraic relation Rα ⊆ (T V)2 as follows:
e1 Rα e2 ⇐⇒ ∀P : V → O. (α ◦ TP)(e1 ) ≤ (α ◦ TP)(e2 )MSFP 2020

Niels Voorneveld(Taltech)

From equations to distinctions for effectful computations

Equations =⇒ algebras
Suppose we have an algebraic relation I ⊆ (T V)2 .
Let B := I ∩ (T ∅)2 be the sub-relation on fundamental(continuation free) computations.
Consider the quotient [B] := T ∅/B with injection ι : T ∅ → [B].
Extracting an algebra:

O/ [B]
OTT ∅/ T∅

T [B]αι

TιµT∅

Lemma
If I is reflexive, transitive and compositional, then αI is awell-defined EM-algebra.

MSFP 2020

Niels Voorneveld(Taltech)

From equations to distinctions for effectful computations

Algebra for probability
Consider the axioms A for probability.
For probability, T ∅ are binary trees whose leaves are either ⊥ or >.
∀e1 , e2 ∈ T ∅, e1 RA e2 ⇔ P(e1 7→ >) ≤ P(e2 7→ >),so [B] = [0, 1] the real number interval.
Derived algebra is the expectations function Exp : T [0, 1] → [0, 1],
whereExp(por(x, y )) = (Exp(x) + Exp(y ))/2.

Implements the fundamental observational question:
What is the probability that the program ...?

MSFP 2020

Niels Voorneveld(Taltech)

From equations to distinctions for effectful computations

Algebra for global store
Consider the axioms A for global store.
∀e ∈ T ∅, ∃!S ⊆ N: e RA lookup(0 ∈ S, 1 ∈ S, 2 ∈ S, . . . ).
so [B] := P(N) ' N → B, the order of state predicates.
The constructed algebra is the weakest precondition function
Wp : T (P(N)) → P(N) where,Wp(upi (x)){n ∈ N | i ∈ Wp(x)}=Wp(lo(x0 , x1 , . . . ))={n ∈ N | n ∈ Wp(xn )}Implements the fundamental observational question:
For which starting states does the program ...?
MSFP 2020

Niels Voorneveld(Taltech)

From equations to distinctions for effectful computations

Coincidence between algebra and equations
Lemma
I reflexive, transitive and compositional I ⊆ RαI .

Definition
I is base-valued if for any e1 , e2 ∈ T V,e1 I e2 ⇐⇒ ∀P : V → T ∅. P ∗ (e1 ) I P ∗ (e2 )Proposition
If I is reflexive, transitive, compositional and base-valued, thenI = R αI .

MSFP 2020

Niels Voorneveld(Taltech)

From equations to distinctions for effectful computations

Program equivalence: Quantitative logic
Going higher-order: Program equivalence/approximation.
We use O as the truth space for quantitative predicates.
If O is a complete lattice, Quantitative Distinction Logic:n ∈ N{n} ∈ formulas(N)φ ∈ formulas(C )U(φ) ∈ formulas(U(C ))V :A φ ∈ formulas(C )V 7→φ ∈ formulas(C )φ ∈ formulas(A)α(φ) ∈ formulas(F (A))Φ ⊆ formulas(E )WΦ ∈ formulas(E )Φ ⊆ formulas(E )VΦ ∈ formulas(E )a ∈ Oconstant(a) ∈ formulas(E )a ∈ O φ ∈ formulas(E )(φ≥a) ∈ formulas(E )This is an example of such a logic for a CBPV language.
MSFP 2020

Niels Voorneveld(Taltech)

From equations to distinctions for effectful computations

Program equivalence: Applicative simulation
On the equating side: Applicative bisimilarity/similarity.
If O is a complete lattice, we can define a relator
ΓαX ,Y : Relation(X , Y ) → Relation(TX , TY )
ΓαX ,Y (R) is the largest relation s.t.
for all P : X → O and Q : Y → O:XP O

R /| Y=⇒Γα
X ,Y(R)| / TYTXα(P)

Q| /O≤O|≤ α(Q)/O

Two programs are related if one “simulates” the other.
Applicative simulations generate program approximation.
MSFP 2020

Niels Voorneveld(Taltech)

From equations to distinctions for effectful computations

Algebra for cost
An operation for associating cost:tick : 1.

tick(x) ≤ x
Simple derivation:⊥ ≤ tick(⊥) ≤ ⊥ =⇒ ⊥ = tick(⊥)
Carrier [B] = N + {∞}.
Algebra is the Tally operation: Tally(tick(x)) = Tally(x) + 1.
Implements the fundamental observational question:
For which price does the program ...?

MSFP 2020

Niels Voorneveld(Taltech)

From equations to distinctions for effectful computations

Algebra for effect combinations
Probability + Global store, operations distribute:
updatei (por(x, y ))=por(updatei (x), updatei (y ))por(lookup(x0 , x1 , . . . ), y )=lookup(por(x0 , y ), por(x1 , y ), . . . )For all r ∈ [0, 1] let hr i ∈ T ∅ s.t. P(hr i 7→ >) = r .
∀e ∈ T ∅, ∃!p : N → [0, 1], e RA lookup(hp(0)i, hp(1)i, hp(2)i, . . . )Carrier: N → [0, 1].
Algebra: Weakest probabilistic precondition.
Implements the fundamental observational question:
For each starting state, what is the probability that the program...?
MSFP 2020

Niels Voorneveld(Taltech)

From equations to distinctions for effectful computations

Conclusion(I )+3 Algebraic relation ks(In)equation axioms!)

EM-algebra

(II )

nv

Applicative simulation+3 Behavioural Equivalence ks(II )

Quantitative formulas(I) Current work: ‘1-to-1’ construction for base-valued relations.
(II) Previous work: Formulation of a congruent program
equivalence if O is a complete lattice and algebra isω-continuous.
MSFP 2020

Niels Voorneveld(Taltech)

From equations to distinctions for effectful computations