1How to Prove Your Calculus Is Decidable
Practical Applications ofSecond-Order Algebraic Theories and Computation

Makoto Hamana
Department of Computer Science,Gunma University, Japan
September 5, ICFP 2017, Oxford

2This Work
B Propose the system SOL: Second-Order Laboratory
B Haskell-based tool for analysing conﬂuence and termination of
second-order computatoin rules– HO version of Knuth and Bendix’s critical pair checking
using an extended HO pattern uniﬁcation (FCU) [Libal,Miller’16]– Powerful enough HO termination checker
B Conﬂuence + termination ⇒ Decidability of calculus
B Demonstrate usefulness through 8 sample HO PL calculi(global state, computational meta-lang., linear λ, π-calculus,· · · )3Example: MonadA monad T is a structure with two operations
return : a → T a

À--: T a → (a → T b) → T bsatisfying(unitL)

return(x) À-- λy.k y=kx(unitR)e À-- λy.return(y)=e(assoc)(e À-- λx.k x) À-- λy.` y=e À-- λx.(k x À-- λy.` y)

The theory of monad is decidable.
Q. Given two well-typed terms s, t consisting of return, À-- and variables,is an equation s = t derivable from the three laws?

4

Monad Laws as Rewrite Rules(unitL)

return(X) À-- y.K[y] ⇒ K[X]

(unitR)E À-- y.return(y) ⇒ E(assoc)(E À-- x.K[x]) À-- y.L[y] ⇒ E À-- x.(K[x] À-- y.L[y])B Write the free variables in capitals

5

Two Important Rewriting Properties

CRConﬂuence

SN
Strong Normalisation

Church-Rosser·ª 55∗ ªª55∗5½¥ªª. 77.
77¨¨¨∗ 77¾ ¤¨¨¨ ∗.

.
²: ﬁnite.²

6

Basic Idea
If a rewrite system C has the properties of CR & SN
1. There always exist unique normal forms

t0

*
©
©©
HHjH

t1

s1- t2- s2- ···

- ···

HHHj©
*
©©

v

(Normal form)

2. Gives a decidable proof method of arbitrary equation
C?

` s=t

⇔

proof by rewriting

7

Basic Idea: Proof by Rewriting
To proveC` s = tis equivalent to showingsC

t{{{{{{{{}

CCCCCCC!

· · · OO

OOO
OOO
OOO'?

oooooooow ooon= n0Normal forms.
.
How to prove CR and SN?

···

8

How to Prove Monad Laws are SN (i.e. Terminating)(unitL)

return(X) À-- y.K[y] ⇒ K[X]

(unitR)E À-- y.return(y) ⇒ E(assoc)(E À-- x.K[x]) À-- y.L[y] ⇒ E À-- x.(K[x] À-- y.L[y])B Bad: No simple “weight” for term
B Standard: Reducibility method [Tait, Girard; Lindley, Stark’05. . . ]– how to ﬁnd suitable reducibility predicate
B SOL: The General Schema criterion by Blanqui [RTA’00,TCS’16]– based on computability– just checks (various) syntactic conditions
positivity, accessibility, safe use of recursive calls, metavariables

9

How to Prove Monad Laws are SN by SOL
Step 1. Write a Haskell script for describing rewrite rules and.
signature using SOL’s DSL (by Template Haskell)monad = [rule|(unitL) return(X) >>= y.K[y]=> K[X](unitR) E >>= y.return(y)=> E(assoc) (E >>= x.K[x]) >>= y.L[y] => E >>= x.(K[x] >>= y.L[y])|]10

How to Prove Monad Laws are SN by SOLStep 2. Invoke the SOL’s command sn in GHCi

*SOL> sn monad sigm
Found constructors: return
Checking type order >>OK
Checking positivity of constructors >>OK
Checking function dependency >>OK
Checking (unitL) return(X) >>=y.K[y] => K[X]
(meta K)[is acc in return(X),y.K[y]] [is positive in return(X)] [is acc in K[y]](meta X)[is acc in return(X),y.K[y]] [is positive in return(X)] [is acc in X] >>True
Checking (unitR) N >>=y.return(y) => N(meta N)[is acc in N,y.return(y)] [is acc in N] >>True
Checking (assoc) (N >>=x.K[x]) >>=y.L[y] => N >>=x.(K[x] >>=y.L[y])(fun bind=bind) subterm comparison of args w. lexLR(meta N)[is acc in N >>=x.K[x],y.L[y]] [is positive in N >>=x.K[x]] [is acc in N](fun bind=bind) subterm comparison of args w. lexLR(meta K)[is acc in N >>=x.K[x],y.L[y]] [is positive in N >>=x.K[x]] [is acc in K[x]](meta L)[is acc in N >>=x.K[x],y.L[y]] [is positive in N >>=x.K[x]] [is acc in L[y]] >>True#SN!

This shows termination.

11

How to Prove Monad Laws are CR by SOL
Step 3. Invoke the command cri for critical pair checking*SOL> cri monad

1: Overlap (unitL)-(unitR)--- N’|-> return(X), K|-> z1.return(z1) ---------------L: (return(X) >>=y.K[y]) => K[X]
R: N’ >>=y’.return(y’) => N’return(X) >>=y.return(y)return(X) <-(unitL)-∧-(unitR)-> return(X)---> return(X) =OK= return(X) <--..
5: Overlap (assoc)-(assoc)--- N|-> N’ >>=x’.K’[x’], L’|-> z1.K[z1] --------------L: (N >>=x.K[x]) >>=y.L[y] => N >>=x.(K[x] >>=y.L[y])R: (N’ >>=x’.K’[x’]) >>=y’.L’[y’] => N’ >>=x’.(K’[x’] >>=y’.L’[y’])((N’ >>=x’.K’[x’]) >>=x.K[x]) >>=y.L[y](N’ >>=x’.K’[x’]) >>=x.(K[x] >>=y.L[y]) <-(assoc)-∧-(assoc)-> (N’ >>=x’.(K’[x’] >>=y’.K[y’]))---> N’ >>=x.(K’[x] >>=y.(K[y] >>=y.L[y])) =E= N’ >>=x.(K’[x] >>=x.(K[x] >>=y.L[y])) <--#Joinable! (Total 5 CPs)

12
1: return(X) À-- y.return(y)yyy(unitL) yyyy
|yreturn(X)=EEEE (unitR)
EE
EE"
return(X)3: (return(X’) À-- x.K[x]) À-- y.L[y]|||(assoc) |||~||return(X’) À-- x.
(K[x] À-- y.L[y])BBBBBB(unitL)BBBÃ∗/ K[X’] À-- y.L[y]2: (E’ À-- x’.K’[x’]) À-- y.return(y)||(unitR) |||||}||∗
E’ À-- x’.K’[x’] oBBBBBB(assoc)
BB!

E’ À-- x’.
(K’[x’] À-- y’.return(y’))

4: (E À-- x.return(x)) À-- y.L[y]|||(assoc) |||~||E À-- x.(return(x)À-- y.L[y])BBBBBB(unitR)BBBÃ∗/ E À-- y.L[y]5: ((E’ À-- x’.K’[x’]) À-- x.K[x]) À-- y.L[y]vvv(assoc) vvv
v
zvv(E’ À-- x’.K’[x’]) À-x.(K[x] À-- y.L[y])HH
HH
HH(assoc)
HH
H$(E’ À-- x’.(K’[x’] À-y’.K[y’])) À-- y.L[y]

JJt
JJtt
Jt∗
t
∗ JJt
JJ
J$ ztttt·This shows local conﬂuence, and with SN and Newman’s lemma, we have CR.

13

Example: MonadA monad T is a structure with two operations
return : a → T a

À--: T a → (a → T b) → T bsatisfying(unitL)

return(x) À-- λy.k y=kx(unitR)e À-- λy.return(y)=e(assoc)(e À-- λx.k x) À-- λy.` y=e À-- λx.(k x À-- λy.` y)

The theory of monad is decidable.

14Results: Decidability of Various Calculi — ICFP side
B Monad laws
B Algebraic theory of global state [Plotkin,Power’02]
B Various λ-calculus: Call-by-name, Call-by-value [Plotkin TCS’75]
Computational meta-language λml [Moggi’88]
Monadic calculus λml∗ [Sabry,Wadler TOPLAS’97]
B Hasegawa’s linear λ-calculus [Ohta,Hasegwa RTA’06]
B Linear Term Calculus [Benton JFP’95]
B Algebraic theory of π-calculus [Stark TCS’08]
B Asymmetric lens laws [Foster et al. TOPLAS’07]

15

How to Prove Your Calculus Is Decidable

16Let’s Prove Your Calculus is Decidable usingSOL– I’m happy to assist you. Ask me directly, by email or Slack –