Introduction

On the reduction ofthe type-freecomputational λ-calculus

Ugo de’Liguoro, Riccardo Treglia

University of Turin, Italy

IWC 2020 30/06/2020

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

1 / 21

Introduction

Overview
Moggi Computational Monadvia Wadler 1 s definition
Computational λ  calculus
SyntaxCalculus
Reduction relation
Contexts
Confluence
Factorization

Semantics
Intersection type assignment
Subject convertibility
Monadic Interpretation
D8 modelSoundness and Completeness via filter model

We study a notion of reduction and prove it is confluent and factorizes; also werelate our calculus to the original work by Moggi.
Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

1 / 21

Introduction

Why effects in functional languages

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

2 / 21

Introduction

Why effects in functional languages
Semantic theories are an established field providing foundations to software
analysis and verification

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

2 / 21

Introduction

Why effects in functional languages
Semantic theories are an established field providing foundations to software
analysis and verification
We have nice theories of the semantics for functional programming languages,
but procedural languages commonly used for both sequential and concurrent
programming have non-functional features, collectively called effects

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

2 / 21

Introduction

Why effects in functional languages
Semantic theories are an established field providing foundations to software
analysis and verification
We have nice theories of the semantics for functional programming languages,
but procedural languages commonly used for both sequential and concurrent
programming have non-functional features, collectively called effects
Since Algol’60 project various λ-calculi have been used as metalanguages
providing semantics to programming languages in general, and a successful
approach among others is based on the notion of computational monad[Moggi89, 91]

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

2 / 21

Introduction

Why effects in functional languages
Semantic theories are an established field providing foundations to software
analysis and verification
We have nice theories of the semantics for functional programming languages,
but procedural languages commonly used for both sequential and concurrent
programming have non-functional features, collectively called effects
Since Algol’60 project various λ-calculi have been used as metalanguages
providing semantics to programming languages in general, and a successfulapproach among others is based on the notion of computational monad[Moggi89, 91]
Monads have been studied and implemented mainly for typed languages;
here we address the issue of modelling effects in the untyped case.

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

2 / 21

Introduction

Computational Monads (after Wadler)
A monad is a triple pT, unit, q
Types
D is the type of values;
TD is the type of computations (with effects) over D.
Operators

unitD : D Ñ TD

(Haskell: return);

D,E : TD Ñ pD Ñ TE q Ñ TE (Haskell: ¡¡).
Axiomspunit d q  f  f da  unit  apa  f q  g  a  λλ d.pf d  g q

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

3 / 21

Calculus

Untyped computational λ-calculus: λuc
We consider Moggi’s call-by-value reflexive object:
D  D Ñ TD
hence there are two types, D and TD, and two kinds of terms:
Val :V,W

Com :L, M, N::::x | λx.Munit V | M  V(values)(computations)having types:
x :D$x :D$V :D$ unit V : TD
Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

x : D $ M : TD$ λx.M : D Ñ TD  D$ M : TD $ V : D  D Ñ TD$ M  V : TD
On the reduction of Comp. λ-Calc.

IWC 2020

4 / 21

Calculus

Reduction
Orienting monad axioms we get ÝÑ  Com  Com as the compatible closure of:βcidass

unit V  pλx.M qM  λx.unit xpL  λx.M q  λy .NÝÑ M rV {x sÝÑ M
ÝÑ L  λx.pM  λy .N q

for x R FV pN q

where M rV {x s denotes the capture avoiding substitution of V for all freeoccurrences of x in M.
To have extensionality we add:p ηc qunit λx.punit x  V q ÝÑ unit V

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

if x R FV pV q

IWC 2020

5 / 21

WRT Moggi’s calculus

λuc versus type free λc : translation
let is definable:

let x  M in N  M  λx.NNo primitive functional application but

pλx.M qV  punit V q  pλx.M q
VM  M  VMN  M  λz.pN  z q for some fresh z
By this we retrieve ordinary call-by-value reduction rule:pβv qpλx.M qV  punit V q  pλx.M q ÝÑβ M rV {x s

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

cOn the reduction of Comp. λ-Calc.

IWC 2020

6 / 21

WRT Moggi’s calculus

λuc versus type free λc : translation
let is definable:

let x  M in N  M  λx.NNo primitive functional application but

pλx.M qV  punit V q  pλx.M q
VM  M  V
MN  M  λz.pN  z q for some fresh zBonus track: shuffling calculus
V ppλx.LqN q ÞÑσ3 pλx.VLqN
that translatedpN  λx.Lq  V ÞÑσ N  λx.pL  V qpN  λx.Lq  V ÞÑass N  λx.pL  V q if V is a variable
3andUgo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

6 / 21

WRT Moggi’s calculus

λuc versus type free λc : mutual interpretation
Theorem

There exists an interpretation z{ from λC into λuc that preserves reductions.
There exists an interpretation xy from λuc into λC that preserves theconvertibility relation.
The reduction relation λC is confluent.
This has been shown by Makoto Hamana, Polymorphic Rewrite Rules:
Confluence, Type Inference, and Instance Validation, 2018.
It is done by checking critical pair using his tool.

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

7 / 21ConfluenceM-ConfluenceL-DP

NReduction in λuc has three basic rules whose left-hand sides may overlap (notorthogonal).
We split the proof in three steps:
1+2. proving confluence of βc Y id and ass separately,
3. eventually combining by means of the commutativity of these relations.
Adopted strategy:
call-by-need calculi with the let construct (see [AFM 95, MOTW99])
variant of call-by-value λ-calculus in [CG14],

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

8 / 21

Confluence

ExampleExamplepunit V  λx. M q  λy . Nass- unit V  λx. pM  λy . N qβc?
M rV {x s  λy . NβcpM  λy . N qrV {x s?

where x R FVpN q, which is the side condition to rule ass; therefore the two terms
in the lower line of the diagram are syntactically identical.

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

9 / 21

Confluence

ExampleExamplepM  λy N q  λx. unit x

ass- M  λy . pN  λx. unit x q

id

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

idM  λy . N

On the reduction of Comp. λ-Calc.

IWC 2020

9 / 21

Confluence

ExampleExampleHere the outer reduction by ass overlaps with an inner reduction by id. This isrecovered by means of an inner reduction by βc :pM  λx. unit x q  λy . N

ass- M  λx. punit x  λy N qβcid?
M  λy . N

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

αOn the reduction of Comp. λ-Calc.

?
M  λx. N rx {y sIWC 2020

9 / 21ÝÑConfluence

βc ,id confluence

Define the following relationÝÑ , as in the book [Ter03] ch. 10.

DefinitionÝÑ  Term  Term is inductively defined by:ÝÑ xM ÝÑ N ñ λx.M ÝÑ λx.NV ÝÑ V ñ unit V ÝÑ
 unit VM ÝÑ M and V ÝÑ
 V ñ M  V ÝÑ
 M VM ÝÑ M and V ÝÑ
 V ñ unit V  λx.M ÝÑ M rV {x sM ÝÑ M ñ M  λx.unit x ÝÑ
 M

The relation
123456x111111111111Lemma (Substitutivity lemma)

For M, M 1 P Com and V , V 1 P Val and every variable x,if M ÝÑ
 M 1 and V ÝÑ V 1 , then M rV {x s ÝÑ
 M 1 rV 1 {x s.

ÝÑβ ,id  ÝÑ  ÝÑβ ,idUgo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

cOn the reduction of Comp. λ-Calc.

cIWC 202010 / 21βc ,id confluence

The next step in the proof is to show thatthe relation ÝÑ satisfies the triangle
property TP:TP implies the diamond property
P-PNL-Q-DP ?

ÝÑ

Confluence

DP 1In fact, if TP holds then we can take P 1  P  in DP, since the latter onlydepends on P. We then define P  in terms of P as defining an adapted version ofTakahashi translation.
Lemma
For all P, Q P Term, if P ÝÑ
 Q then Q ÝÑ
 P  , namely ÝÑ satisfies TP.

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

11 / 21

Confluenceass confluence
To prove confluence of ass, we use Newman Lemma (see [Bar84], Prop. 3.1.24).
A notion of reduction R is weakly Church-Rosser, shortly WCR, if-

MN

-DP

LLemmaThe notion of reduction ass is WCR.

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

12 / 21

Confluenceass confluence
Recall that a notion of reduction R is strongly normalizing, shortly SN, if there
exists no infinite reduction M ÝÑR M1 ÝÑR M2 ÝÑR    out of any M P Com.
Lemma
The notion of reduction ass is SN.
Proof idea
Given M P Com. Let’s decorate eachoccurrence of  in M with a naturalnumber.
Define i left to j in M iff

DpL j V q subterm of M
i occurs in Ldef
7M  | tpxi , xj q | xi left to xj u |It’s easy to see that
7M ¡ 7N if M ÝÑass N

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

2
1

1
V

assλx

N

2N λxLOn the reduction of Comp. λ-Calc.

LVIWC 202013 / 21

Confluenceass confluence
Corollary
The notion of reduction ass is CR.
Proof.
By the previous lemma and by Newman Lemma, stating thata notion of reduction which is WCR and SN is CR.

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

14 / 21ÝÑ

βc ,idandÝÑ

Confluence

asscommute

The following definitions are from [BN98], Def. 2.7.9.
Relations ÝÑ1 and ÝÑ2 strongly commute if, for all M, N, L:

2
1MN

DP2-

1L

where ÝÑ2 is ÝÑ2 Y , namely at most one reduction step.
Lemma
Reductions ÝÑβc ,id and ÝÑass strongly commute, then commute.

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

15 / 21

Confluence

Complete proof recap#ÝÑβ ,id ÝÑ ÝÑβ ,id has TPTakahashi traslation ÝÑParallel reductioncc

ass is WCR
ass is SN

βc Y id is CR
ass is CR

βc Y idstrongly commutes with ass
βc Y id and ass
commuteUgo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

Newman lemmaHyndley Rosen lemma

βc Y id Y ass is CR

On the reduction of Comp. λ-Calc.

IWC 2020

16 / 21

Factorization

Factorization
An abstract reduction system pTerm, ÝÑq factorizes via ÝÑe , ÝÑ e ifÝÑ  ÝÑe Y ÝÑ eand for all M, N P Term, M ÝÑ N implies that there exists L P Term such thatM ÝÑe L ÝÑ e N.

We abbreviate the last condition by M ÝÑe  ÝÑ e N.
Factorized reduction example

 ppq

pqq qMunit λy .unit yλw . unit λx.unit xλz.unit zunit λy .unit y λw . unit λx.unit x λz.unit zunit λy .unit y λw . unit λz.unit zunit λx.unit x ppppq

p
qMunit λy .unit yλw . unit λx.unit xunit λx.unit x λz.unit zunit λx.unit xp



Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

q

ÝÑass
ÝÑβ
ÝÑβccqq  λz.unit z ÝÑβÝÑβ

On the reduction of Comp. λ-Calc.

cc

IWC 2020

17 / 21

Factorization

Essential vs. Inessential Contexts
Take ÝÑ  ÝÑλCConstruct the relations ÝÑe , ÝÑ e , called the essential and inessential in[AFG19], by closing ÞÑλC under two sorts of contexts:
Inessential contexts:
Essential contexts:

::
::

EExC y | unit λx. E | M  λx. E | E  VxC y | E  V

where the hole xC y can be filled by terms in Com only.
Then ÝÑe and ÝÑ e are the least relations including ÞÑλC such that for all
M, N P Com:M ÞÑλC N ùñ E xM y ÝÑe E xN yandM ÞÑλC N ùñE xM y ÝÑ e

E xN yWe highlight that relations ÝÑe and ÝÑ e are actually not disjoint, as essentialsteps are also inessential.

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

18 / 21

Factorization

Techniques in between
One of the strengths of the method in [AFG19] is the fact that it does not rely on
the DP of the parallel reduction ñλC but on the substitutivity property of ann 1
indexed refined ùùñλC
Definition (Indexed parallel reduction)ùñn  Term  Term is inductively defined by:1 x ù
ñx2 M ùñn N ñ λx.M ùñn λx.N3 V ùñn V 1 ñ unit V ùñn unit V 1n mm
4 M ùñn M 1 and V ùñV 1 ñ M  V ùùùñ M 1  V 1n |M 1 |x m 1m5 M ùñn M 1 and V ùñV 1 ñ unit V  λx.M ùùùùùùùùùùù
ñ M 1 r V 1 {x s6 M ùñn M 1 ñ M  λx.unit x ùñn M 1n m p 1m7 L ùñn L1 and M ùñ
M 1 and N ùñp N 1 ñ pL  λx.M q  λy .N ùùùùùù
ñ L  λx.pM 1  λy .N 1 q

The relation

0and of another auxiliary relations ñ e , roughly the parallel reduction built overÝÑ e

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

19 / 21

Factorization

Factorization proof
Proposition (λC Macro-step system)
123Merge: if M ñ e  ÝÑe M 1 then M ñλC M 1Indexed split: if M ñù M 1 , then M ñ e M 1 , or n ¡ 0 and M ÝÑe  ùùñ M 1nn 1Split: If M ñλC M 1 , then M ÝÑe  ñ e M 1 .

Then pTerm, ÝÑe Y ÝÑ e q is a macro-step system with respect to ñλC andñ e.

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

20 / 21

Factorization

Factorization proof
Proposition (λC Macro-step system)
123Merge: if M ñ e  ÝÑe M 1 then M ñλC M 1

Indexed split: if M ñù M 1 , then M ñ e M 1 , or n ¡ 0 and M ÝÑe  ùùñ M 1nn 1

Split: If M ñλC M 1 , then M ÝÑe  ñ e M 1 .

Then pTerm, ÝÑe Y ÝÑ e q is a macro-step system with respect to ñλC andñ e.
By Split and Merge ññλC ÝÑe e ññ e  ÝÑe ÝÑeeWe have

By construction

ñλC ÝÑ λC
ñ e ÝÑe  ñ  ÝÑ  ÝÑpÝÑe Y ÝÑ e q  ÝÑeeee

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

20 / 21

Factorization

Factorization proof
Proposition (λC Macro-step system)
1

2
3

Merge: if M ñ e  ÝÑe M 1 then M ñλC M 1

Indexed split: if M ñù M 1 , then M ñ e M 1 , or n ¡ 0 and M ÝÑe  ùùñ M 1nn 1

Split: If M ñλC M 1 , then M ÝÑe  ñ e M 1 .

Then pTerm, ÝÑe Y ÝÑ e q is a macro-step system with respect to ñλC andñ e.
Every Macro-step system satisfies factorization:
Theorem (Factorization)

The reduction system pTerm, ÝÑλC q factorizes via ÝÑe , ÝÑ eM ÝÑλC M 1 ñ M ÝÑe  ÝÑ e M 1

Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

20 / 21

Factorization

References IZ.M. Ariola and Arvind.
Properties of a First-order Functional Language with Sharing.
Theoretical Computer Science, 146:69–108, 1995.
E. Albert, P. Arenas, M. Codish, S. Genaim, G. Puebla, and D. Zanardini.
Termination Analysis of Java Bytecode.
In G. Barthe and F. de Boer, editors, Proceedings of Formal Methods forOpen Object-Based Distributed Systems (FMOODS’08), Oslo, Norway, 2008,
volume 5051 of Lecture Notes in Computer Science, pages 2–18. Springer
Verlag, 2008.
Arvind, L. Augusston, J Hicks, R. S. Nikhil, S. Peyton-Jones, J. Stoy, andW Williams.
pH: A Parallel Haskell.
Technical report, MIT Laboratory for Computer Science, September 1993.
F. Alessi, F. Barbanera, and M. Dezani-Ciancaglini.
Intersection Types and Computational Rules.
Electronic Notes in Theoretical Computer Science, 84, 2003.
Ugo de’Liguoro, Riccardo Treglia (University of Turin, Italy)

On the reduction of Comp. λ-Calc.

IWC 2020

21 / 21