Amortised Resource Analysis for Lazy Functional Programs
Full text
Hugo Miguel Oli ei a Romualdo Sim˜
oes
Amo ised Resou ce Analysis
o
Lazy Func ional P og ams
Depa amen o de Ciˆ
encia de Compu ado es
Faculdade de Ciˆ
encias da Uni e sidade do Po o
Fe e ei o de 2014
Hugo Miguel Oli ei a Romualdo Sim˜
oes
Amo ised Resou ce Analysis
o
Lazy Func ional P og ams
Tese subme ida `
a Faculdade de Ciˆ
encias da Uni e sidade do Po o
pa a ob enc¸ ˜
ao do g au de Dou o em Ciˆ
encia de Compu ado es
Supe iso s: P o . M´
a io Flo ido and P o . Ke in Hammond
Depa amen o de Ciˆ
encia de Compu ado es
Faculdade de Ciˆ
encias da Uni e sidade do Po o
Fe e ei o de 2014
To my wi e and sons.
Acknowledgemen s
I would like o exp ess my deepes hanks o he people who di ec ly con ibu ed o he
conclusion o his hesis. Fi s , I would like o hank my supe iso s M´
a io Flo ido and Ke in
Hammond o hei encou agemen , suppo and op imism. I especially hank Ke in and his
wi e o a wa m welcome and making me eel a home du ing my s ay in bonnie S And ews
oge he wi h my wi e.
My hanks ex end o he unc ional p og amming g oup in S And ews o aluable discus-
sions and, in pa icula , I would also like o hank S e en Jos and A melle Bonen an , and
hei espec i e amilies, o ou hiking ips ac oss Sco land and o pu ing ou sha ed
in e es s in boa d gaming in o p ac ice.
A e y special hanks goes o my iends and colleagues S e en Jos and Ped o Vascon-
celos o hei con inuous help in pu suing a p ac ical app oach o he p oblem o esou ce
analysis o lazy unc ional p og ams. Ou long collabo a ion o med he basis o his hesis.
I would like o hank M´
a io, Ke in, S e en and Ped o o e iewing d a s o his hesis, wi h
special hanks o Sand a Al es and Oli ie Dan y o also ac ually olun ee ing o ha ask.
Many hanks o he ex e nal examine s p esen a my i a, Vasco Thudichum Vasconcelos
and Rica do Pe˜
na, o hei kind commen s and in e es ing obse a ions.
A e my esea ch g an was o e , I was able o egula ly wo k on my hesis, while de-
eloping mobile applica ions, hanks o Lu´
ıs Damas and Michel Fe ei a a Geolink Lda.
Simila ly, I would like o hank Edua do Ca queja a AppGene a ion o g ace ully handling
my indecision o e se ing he end da e o my lea e o absence while I was inishing w i ing
his hesis.
Financial suppo is acknowledged om he “Fundac¸ ˜
ao pa a a Ciˆ
encia e Tecnologia”, o he
Ph.D. g an SFRH/BD/17096/2004 and o a esea ch g an a p ojec RESCUE (REliable
and Sa e Code execU ion o Embedded sys ems) PTDC/EIA/65862/2006, and also om
he LIACC (Labo a o y o A i icial In elligence and Compu e Science) o he Uni e si y o
Po o, Po ugal.
Finally, I hank my wi e, no only o he uncondi ional suppo du ing his long Ph.D. pe iod,
bu also o sha ing he happies days o my li e oge he wi h ou h ee sons. To happiness!
ii
Resumo
Es a ese desc e e a p imei a en a i a bem-sucedida, de que emos conhecimen o, de
de ini uma an´
alise es ´
a ica, au oma izada e baseada em sis emas de ipos, capaz de en-
con a majo an es ela i os `
a quan idade de ecu sos u ilizados em p og amas uncionais
lazy. A a aliac¸ ˜
ao lazy pe mi e melho a a composic¸ ˜
ao de p og amas, mas di icul a quase
semp e as p e is˜
oes de ecu sos. A nossa an´
alise u iliza a abo dagem de amo izac¸ ˜
ao
au oma izada desen ol ida po Ho mann e Jos , que es a a an e io men e es ingida `
a
a aliac¸ ˜
ao eage . Nes a ese, es endemos es e abalho a sis emas lazy a a ´
es da cap-
u a em ano ac¸ ˜
oes de ipos dos cus os de exp ess˜
oes po a alia e da amo izac¸ ˜
ao do
pagamen o des es cus os u ilizando uma noc¸ ˜
ao de po encial lazy. Ap esen amos a nossa
an´
alise como um sis ema de demons ac¸ ˜
ao que p e ˆ
e (em empo de compilac¸ ˜
ao) a quan-
idade o al de alocac¸ ˜
oes de mem´
o ia heap de uma linguagem uncional m´
ınima (incluindo
unc¸ ˜
oes de o dem supe io e ipos de dados ecu si os) e de inimos um modelo de cus os
o mal baseado na semˆ
an ica de Launchbu y pa a a aliac¸ ˜
ao lazy. P o amos a co ec¸ ˜
ao
da nossa an´
alise ace ao modelo de cus os. A nossa abo dagem ´
e ilus ada a a ´
es
de de i ac¸ ˜
oes de ipos de exemplos ep esen a i os e n˜
ao i iais, que o am analisados
u ilizando um p o ´
o ipo da implemen ac¸ ˜
ao da nossa an´
alise.
Pala as-cha e: a aliac¸ ˜
ao lazy, an´
alise amo izada, an´
alise de ecu sos, sis ema de ipos,
call-by-need, an´
alise es ´
a ica
iii
Abs ac
This hesis desc ibes he i s success ul a emp , o which we a e awa e, o de ine an
au oma ic, ype-based s a ic analysis o esou ce bounds o lazy unc ional p og ams. Lazy
e alua ion allows imp o ed modula i y o p og ams, bu o en makes esou ce usage di icul
o p edic . Ou analysis uses he au oma ic amo isa ion app oach de eloped by Ho mann
and Jos , which was p e iously es ic ed o eage e alua ion. In his hesis, we ex end his
wo k o a lazy se ing by cap u ing he cos s o une alua ed exp essions in ype anno a ions
and by amo ising he paymen o hese cos s using a no ion o lazy po en ial. We p esen
ou analysis as a p oo sys em o p edic ing (a compile- ime) o al heap alloca ions o a
minimal unc ional language (including highe -o de unc ions and ecu si e da a ypes) and
de ine a o mal cos model based on Launchbu y’s na u al seman ics o lazy e alua ion.
We p o e he soundness o ou analysis wi h espec o he cos model. Ou app oach is
illus a ed by ype de i a ions o a numbe o ep esen a i e and non- i ial examples ha
ha e been analysed using a p o o ype implemen a ion o ou analysis.
Keywo ds: lazy e alua ion, amo ized analysis, esou ce analysis, ype sys em, call-by-
need, s a ic analysis
ix
A.3 Anno a ed ypes ..................................104
A.4 Sha ing ela ion...................................104
A.5 Syn ax di ec ed ype ules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
A.6 S uc u al ype ules ................................105
A.7 Po en ial.......................................106
B.1 Type de i a ion o a non-s ic e alua ion example . . . . . . . . . . . . . . . 115
B.2 Type de i a ion o a lazy-e alua ion example . . . . . . . . . . . . . . . . . . 116
B.3 Type de i a ion o map applied o a lis wi h po en ial . . . . . . . . . . . . . . 117
B.4 Auxilia y ype de i a ion o map applied o a lis wi h po en ial . . . . . . . . . 118
B.5 Auxilia y ype de i a ion o map applied o a lis wi h po en ial (con .) . . . . . 119
B.6 Type de i a ion o map applied o a lis wi h no po en ial . . . . . . . . . . . . 120
B.7 Auxilia y ype de i a ion o map applied o a lis wi h no po en ial . . . . . . . 121
B.8 Auxilia y ype de i a ion o map applied o a lis wi h no po en ial (con .) . . . 122
x i
Lis o Theo ems and De ini ions
4.1 De ini ion (Bound Va iables o Fun Exp essions) . . . . . . . . . . . . . . . . 19
4.2 De ini ion(F eshness) ............................... 20
4.3 Lemma (In a ian Loca ions Unde E alua ion) . . . . . . . . . . . . . . . . . 22
5.1 De ini ion (Idempo en Types and Idempo en Con ex s) . . . . . . . . . . . . 31
5.2 Lemma(Subs i u ion) ............................... 37
5.3 Lemma (CONS In e sion) ............................. 37
5.4 Lemma (ABS In e sion) .............................. 38
5.5 Lemma (Con ex Spli ing) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
5.6 De ini ion(Po en ial) ................................ 39
5.7 Lemma (Po en ial Spli ing) . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
5.8 Co olla y (Po en ial Remaining) . . . . . . . . . . . . . . . . . . . . . . . . . . 41
5.9 Co olla y (Po en ial Sub ype) . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
5.10 De ini ion (Type Consis ency o Loca ions) . . . . . . . . . . . . . . . . . . . . 41
5.11 De ini ion (Type Consis ency o Heaps) . . . . . . . . . . . . . . . . . . . . . 42
5.12 De ini ion (Global Compa ibili y) . . . . . . . . . . . . . . . . . . . . . . . . . . 42
5.13Theo em(Soundness)............................... 42
5.14 Lemma (Sub yping is a pa ial o de ) . . . . . . . . . . . . . . . . . . . . . . . 45
x ii
5.15 Lemma (Idempo en Sub ypes) . . . . . . . . . . . . . . . . . . . . . . . . . . 45
5.16 De ini ion (Reachabili y) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
5.17 Lemma (Idempo en Cycles) . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
5.18 Theo em (Soundness o he Eage Sys em) . . . . . . . . . . . . . . . . . . . 70
A.1 De ini ion (Type Consis ency o Loca ions) . . . . . . . . . . . . . . . . . . . . 106
A.2 De ini ion (Type Consis ency o Heaps) . . . . . . . . . . . . . . . . . . . . . 106
x iii
1. In oduc ion
Non-s ic unc ional p og amming languages, such as Haskell [PAB+99], o e impo an
bene i s o e mo e con en ional eage ly-e alua ed languages in e ms o modula i y and
abs ac ion [Hug89] h ough exploi ing lazy e alua ion. A key p ac ical obs acle o hei
wide use, howe e , is ha ex a- unc ional p ope ies, such as ime- and space-beha iou ,
a e o en di icul o de e mine p io o ac ually unning he p og am. This is la gely because
he e ec s o lazy e alua ion a e ha d o p edic wi hou ac ually unning a p og am, since
e alua ion o de is de e mined dynamically: educ ion is ca ied ou i and when i is ound
o be needed and consequen ly memo y is alloca ed only i and when needed. Gi en
his di icul y, p o iding gua an ees abou memo y usage o ime pe o mance would bo h
inc ease con idence in so wa e eliabili y and pe o mance o lazily-e alua ed p og ams,
and open new esou ce-c i ical applica ions such as eal- ime, memo y-limi ed sys ems.
Recen ad ances in s a ic cos analyses, such as sized ypes [VH05, SHFV07, Vas08] and
ype-based amo isa ion [HJ03, HAH11] ha e enabled he au oma ic p edic ion o esou ce
bounds o eage unc ional p og ams, including uses o highe -o de unc ions [JLHH10].
This hesis de elops a new mechanism, lazy po en ial, ha allows execu ion cos s o be
ans e ed om one poin o a p og am o ano he , as pa o an amo ised analysis.
By exploi ing his mechanism, we a e hen able o ex end ype-based amo isa ion o
lazy e alua ion, desc ibing a s a ic analysis o de e mining a-p io i wo s -case bounds on
execu ion cos s (speci ically, dynamic memo y alloca ions).
Ou amo ised analysis de i es cos s wi h espec o a cos seman ics o lazy e alua ion
ha de i es om Launchbu y’s na u al ope a ional seman ics o g aph educ ion [Lau93]. I
deals wi h bo h i s -o de and highe -o de unc ions, bu does no conside polymo phism.
Mo eo e , he analysis is composi ional, i.e. i can be applied o p og am agmen s as well
as o comple e p og ams. Fo simplici y, we es ic ou a en ion o o al heap alloca ion,
bu p e ious esul s ha e shown ha he amo ised analysis app oach also ex ends o o he
1
2FCUP
999. 1. In oduc ion
coun able esou ces, such as wo s -case execu ion ime [JLH+09]. In o de o ensu e
a good sepa a ion o conce ns, ou analysis assumes he a ailabili y o Hindley-Milne
ype in o ma ion [Mil78]. We ex end Ho mann and Jos ’s ype anno a ions o cap u ing
po en ial cos s [HJ03] wi h in o ma ion abou he la en cos s o une alua ed exp essions.
The analysis p oduces a se o cons ain s o e cos a iables ha we sol e in ou p o o ype
implemen a ion using an ex e nal LP-sol e . We ha e hus demons a ed all he s eps ha
a e necessa y o p oduce a ully-au oma ic analysis o de e mining bounds on esou ce
usage o lazily-e alua ed p og ams.
Al hough we do no di ec ly add ess he issue o algo i hmic ype econs uc ion in his
hesis, a p o o ype implemen a ion∗and p e ious wo k in he s ic se ing [HJ03, JLHH10,
HAH11] sugges s ha ou analysis should be ully au oma able, e.g. by pe o ming a s an-
da d Damas-Milne ype in e ence [DM82] wi h ypes deco a ed wi h esh anno a ion a i-
ables and p oducing a se o linea inequali ies ha can hen be au oma ically sol ed by a
s anda d LP sol e . No guidance om he p og amme is necessa y.
1.1 Con ibu ions
This hesis makes he ollowing no el con ibu ions:
•we p esen he i s success ul a emp , o which we a e awa e, o p oduce an au o-
ma ic, e icien , ype-based, s a ic analysis wi h o mally gua an eed da a-dependen
esou ce bounds o lazy e alua ion;
•we in oduce a cos model o heap alloca ions o a lazy unc ional language based
on Launchbu y’s na u al seman ics o lazy e alua ion [Lau93], and use his as he
basis o de eloping a esou ce analysis;
•we p o e he soundness o ou analysis wi h espec o he cos -ins umen ed seman-
ics;
•we de elop an analysis o eage unc ional p og ams wi h he pu pose o be e
con as ing he analysis o laziness; and
∗Ped o Vasconcelos implemen ed in Haskell a publicly accessible web-p o o ype o ou analysis (a ailable
a h p://www.dcc. c.up.p /~pb /cgi/aalazy.cgi) — a much welcome elie om he bu den o manually
es ing p og am examples.
FCUP 3
1.1. Con ibu ions 999.
•we demons a e he e ec i eness o he analysis by de i ing cos s o some non- i ial
examples.
The esea ch on which his hesis is based was done in collabo a ion wi h o he s. In
pa icula , he au oma ic amo ised analysis o lazily-e alua ed unc ional p og ams has
p e iously been epo ed in a published pape [SVF+12] which was join ly au ho ed by
Ped o Vasconcelos, S e en Jos , my wo supe iso s M´
a io Flo ido and Ke in Hammond,
and mysel : Hugo Sim˜
oes, Ped o Vasconcelos, M´
a io Flo ido, S e en Jos , and Ke in Ham-
mond. Au oma ic Amo ised Analysis o Dynamic Memo y Alloca ion o Lazy Func ional
P og ams. In P oceedings o he ACM SIGPLAN In e na ional Con e ence on Func ional
P og amming (ICFP’12), pages 165–176, Copenhagen, Denma k, Sep embe 2012. The
echnical di e ences o he published pape a e ha his hesis:
• ixes a mino p oblem in he soundness p oo (caused by ule LET o ou ype sys em);
•changes he language o be compa ible wi h Launchbu y’s seman ics ( eplaces ma ch
wi h case exp essions, emo es pa en heses o cons uc o applica ions and me ges
le cons wi h le exp essions);
•simpli ies anno a ions by eplacing he double cos anno a ions wi h a single cos
anno a ion ( his is possible since we a e analysing a mono onic esou ce: o al heap
alloca ions);
• es ic s he in e sion lemmas o Sec ion 5.5.1 o ha e ze o on he u ns ile o he ype
judgemen s (o he wise hose lemmas would no hold);
•adds a side-condi ion o ule WEAK o ou ype sys em;
•con as s he lazy sys em wi h an eage sys em ha is speci ically ailo ed o empha-
sise he key elemen s o he no el analysis; and
•illus a es he e ec i eness o he analysis wi h de ailed de i a ions o some non- i ial
examples;
No e ha meanwhile he soundness p oo was double checked in de ail, since he i s i e
i ems abo e o ced almos all o he p e ious echnical wo k (including p oo s) o be ew i en
in his hesis.
4FCUP
999. 1. In oduc ion
Also in he cou se o his PhD plan, du ing he in oduc o y s udies on he ield o s a ic
esou ce analysis, he au ho con ibu ed o ano he pape [SHFV07]: Hugo R. Sim˜
oes,
Ke in Hammond, M´
a io Flo ido, and Ped o Vasconcelos. Using In e sec ion Types o
Cos -Analysis o Highe -O de Polymo phic Func ional P og ams. In Tho s en Al enki ch
and Cono McB ide, edi o s, Re ised Selec ed Pape s o he In e na ional Wo kshop on
Types o P oo s and P og ams (TYPES’06), No ingham, UK, Ap il, 2006, olume 4502 o
Lec u e No es in Compu e Science, pages 221–236. Sp inge , 2007. This pape imp o es
he quali y o a p e ious analysis o eage ly e alua ed p og ams by showing how disc e e
polymo phism helps educe he p oblem o size aliasing. Howe e , since i is no a di ec
con ibu ion o he ield o analysis o lazy e alua ion ( he co e opic o his hesis), he esul
is simply e e enced he e.
1.2 O e iew
In he emainde o his hesis we s a by e iewing some ela ed wo k in Chap e 2. Nex ,
in Chap e 3, we e iew some backg ound on amo isa ion, co e ing he desc ip ion o he
gene al echnique and i s applica ion o ype-based analyses.
Then, in Chap e 4, we de ine a simple unc ional language and p esen a cos model o
measu ing he o al heap alloca ions unde a call-by-need seman ics o p og ams w i en in
his language.
In Chap e 5 we de elop a ype-based amo ised analysis o lazy e alua ion and p o ide a
soundness p oo as he main con ibu ion o his hesis, gua an eeing ha he cos bound
o he analysis is obse ed wi h espec o he cos model.
An expe imen al assessmen o he analysis is gi en in Chap e 6 h ough a ange o
illus a i e examples.
Finally, Chap e 7 concludes.
2. Rela ed Wo k
2.1 Seman ics o Lazy E alua ion
We build hea ily on Launchbu y’s na u al seman ics o lazy e alua ion [Lau93], as subse-
quen ly adap ed by Ses o [Ses97], and exploi ideas ha we e de eloped by Encina and
Pe˜
na [EP02, EP03a]. The e is a signi ican body o o he wo k on he seman ics o call-
by-need e alua ion. P e-da ing Launchbu y’s wo k, Josephs [Jos89] ga e a deno a ional
seman ics o lazy e alua ion, using a con inua ion-based seman ics o model sha ing, and
including an explici s o e. Howe e , his app oach does no i well wi h s anda d p oo
echniques. Ma ais e al. [MOW98] subsequen ly de ined bo h na u al and educ ion se-
man ics o he call-by-need lambda calculus, so enabling equa ional easoning, and a
simila app oach was independen ly desc ibed by A iola and Felleisen [AF97].
Like Encina and Pe˜
na [EP03a, EP09], Moun joy [Mou98] de i ed an ope a ional seman ics
o he Spineless Tagless G-Machine om he na u al seman ics o Launchbu y and Ses o ,
including poly-applica i e λ-exp essions. The main di e ences be ween hese app oaches
a e ha Encina and Pe˜
na co ec some mis akes in Moun joy’s p esen a ion; ha hey
p o ide co ec ness p oo s; ha hei seman ics co ec ly deals wi h pa ial applica ions
in he Spineless Tagless G-Machine; ha hey deal wi h pa ial applica ions as no mal
o ms; and ha hey conside wo dis inc implemen a ion a ian s, based on push/en e
e sus apply/e al. Mo e ecen ly, Pi og and Bie nacki [PB10] ha e es ablished he equi -
alence be ween he Spineless Tagless G-Machine and an ex ended e sion o he na u al
seman ics o Launchbu y and Ses o as e idenced by Dan y e al.’s [ADM04] unc ional
co espondence be ween abs ac machines and e alua o s.
Bakewell and Runciman [BR01] ha e p e iously de ined an ope a ional seman ics o Co e
Haskell ha gi es ime and space execu ion cos s in e ms o Ses o ’s seman ics o his
5
6FCUP
999. 2. Rela ed Wo k
Ma k 1 abs ac machine. The wo k has subsequen ly been ex ended o gi e a model
ha can be used o de e mine space leaks by compa ing he space usage o wo e alua-
o s using a bisimula ion app oach [BR00]. Gus a sson and Sands [GS99] ha e simila ly
de ined a space-imp o emen ela ion ha gua an ees ha some op imisa ion can ne e
lead o asymp o ically wo se space beha iou o call-by-need p og ams and Mo an and
Sands [MS99] ha e de ined an imp o emen ela ion o call-by-need p og ams ha can
be used o de e mine whe he one e mina ing p og am imp o es ano he in all possible
con ex s.
Finally, gi en ha compile s o lazy e alua ion e en ually gene a e op imised code based
on in o ma ion om s ic ness analysis [Myc81, BHA86, MN92, WH87] o cheapness anal-
ysis [Myc80, Fax00] and hus implemen in ac a non-s ic seman ics a he han call-by-
need, i is wo h no ing an al e na i e non-s ic educ ion s a egy by Ennals e al. [EP03b,
Enn03], called op imis ic e alua ion, ha , in an a emp o imp o e he a e age ime pe o -
mance agains call-by-need, is based on specula i ely e alua ing exp essions ha a e con-
side ed o be usually used and usually cheap o e alua e and abo ing i an embedded p o-
ile de e mines ha i is no he case. Al hough he app oach p omised o achie e consid-
e able pe o mance imp o emen s, i s de elopmen is cu en ly suspended om indus y-
s engh compile s gi en he di icul ies in main aining he suppo ing amewo k (i.e. spec-
ula ion, p o iling and abo ion) while implemen ing o he ea u es.
Ou own wo k di e s om his body o ea lie wo k in ha we p o ide a cos seman ics om
which we de i e a s a ic analysis o au oma ically de e mine uppe bounds on he memo y
equi emen s o lazily e alua ed p og ams.
2.2 Resou ce Analyses o Lazy E alua ion
Resou ce analysis based on p o iling and manual code inspec ion has long o med he
s a e-o - he-a and s ill is cu en p ac ice in many cases. Indeed, o non-s ic unc ional
languages, such as Haskell, ad-hoc echniques, manual analysis o symbolic p o iling a e
he only cu en ly iable app oaches: he dynamic demand-d i en na u e o lazy unc-
ional p og amming c ea es pa icula p oblems o esou ce analysis, whe he manual o
au oma ic. The e has he e o e been e y li le wo k on s a ic esou ce analysis o lazy
unc ional p og ams, and, o ou knowledge, no p e ious au oma ic s a ic analysis has e e
been p oduced. The mos signi ican p e ious wo k in he a ea is ha by Sands [San90a,
FCUP 7
2.2. Resou ce Analyses o Lazy E alua ion 999.
San90b], whose PhD hesis p oposed a cos calculus o easoning abou su icien and nec-
essa y execu ion ime o lazily e alua ed highe -o de p og ams, using an app oach based
on e alua ion con ex s [Wad88, San98] o cap u e in o ma ion abou e alua ion deg ee
and app op ia e p ojec ions [WH87] o p ojec his in o ma ion o he equi ed app oach.
Wadle [Wad88] had ea lie p oposed a simila app oach o ha aken by Sands, bu lim-
i ed o i s -o de unc ions and using only s ic ness analysis combined wi h app op ia e
p ojec ions, a he han he neededness analysis ha Sands also uses. A ound he same
ime, Bje ne and Holms ¨
om [BH89] de eloped an app oach using demand analysis which
equi es, a-p io i, a domain s uc u e desc ibing an app oxima ion o he ou pu o he
analysed p og am. A p ima y disad an age o such app oaches lies in he complexi y o he
domain s uc u e and associa ed p ojec ions ha mus be used when analysing e en simple
da a s uc u es such as lis s. In con as , ou app oach easily ex ends o algeb aic da a
s uc u es. A seconda y disad an age is ha a demand analysis app oach equi es knowing
in ad ance much in o ma ion abou he ou pu alue and, unlike he sel -con ained analysis
we ha e desc ibed, p ojec ion-based app oaches ely on he exis ence o a complex and
powe ul ex e nal neededness analysis o de e mine e alua ion con ex s o exp essions.
These a e se ious p ac ical disad an ages: in ac , o da e, we a e no awa e o any ully
au oma ic s a ic analysis ha has been p oduced using hese echniques.
T ans o ming lazy p og ams in o eage ones would be a possible app oach o p oducing an
analysis o lazily e alua ed p og ams. The esul ing p og ams would hen be analysed us-
ing (simple ) echniques o eage ly e alua ed p og ams. Unlike ou wo k, hese app oaches
would su e om he p oblems ha hey would p oduce e y poo quali y bounds (many
p og ams equi ing a small ini e amoun o esou ces unde lazy e alua ion, would equi e
an in ini e amoun i e alua ed eage ly), ha hey would be, in gene al, no cos -p ese ing,
ha hey would lead o po en ially exponen ial code explosion, and ha , because hey
would al e he p og am, hey would no be sui able o use wi h s anda d compile s o
lazy unc ional languages. Pe haps because o such d awbacks, no one appea s o ha e
ac ually done his.
Se e al au ho s ha e p oposed app oaches whe e p og ams a e anno a ed wi h addi ional
cos pa ame e s. Fo example, Albe e al. [ASV03] desc ibes how o au oma ically con-
s uc ecu ence ela ions by adding ex a cos pa ame e s o each unc ion unde a call-by-
name seman ics and sugges s ex ending he app oach o call-by-need h ough an addi ional
linea isa ion phase oge he wi h gua ded cons ain s ( o handle sha ing and so a oid cos
14 FCUP
999. 3. Amo isa ion
analysed, made he app oach in e es ing.
Since hen, keeping he undamen al idea, hei echnique has been success ully applied in
he analyses o s ack usage [Cam09], gene ic esou ce me ics [JLH+09], highe -o de and
polymo phic unc ions [JLHH10] and in e icien ly inding mul i a ia e polynomial
bounds [HAH11] h ough using non-linea po en ial unc ions.
3.2.1 In o mal Desc ip ion
In he classical amo isa ion echnique, he i s s ep in de eloping an amo ised analysis is
o de ine he po en ial unc ion — he mapping om con igu a ions o numbe s. In Ho mann
and Jos ’s app oach, his co esponds o de ining he anno a ed ypes he ype sys em will
handle. The anno a ed da a ypes, in pa icula , ca y he con ibu ions o a node in a
pa icula da a s uc u e o he o e all po en ial o he memo y con igu a ion. Fo example,
a ed-black bina y ee [Bay72] is a bina y ee da a s uc u e ha is easie o main ain
balanced han i s egula coun e pa . I consis s o h ee possible cons uc o s: a Red and
aBlack bina y cons uc o s ha ing a le and a igh ed-black bina y ee as a gumen s,
and a ze o-a i y Lea cons uc o . Conside he ollowing anno a ed da a ype o ed-black
bina y ees o In s:
RBT ee(q , qb, ql,In )
In a ee wi h his ype, whe e q ,qband qla e non-nega i e a ional numbe s, each Red and
Black node con ibu es wi h q and qb, espec i ely, and each Lea node con ibu es wi h
ql o he po en ial o he ee. Gi en a ee wi h n ed nodes, nbblack nodes and nllea
nodes, he po en ial o such ee is n ×q +nb×qb+nl×ql. No e ha he po en ial o he
ee is linea wi h espec o i s numbe o nodes. Res ic ing o linea po en ial wi h espec
o he numbe o cons uc o s in a da a s uc u e is common in ype sys ems ollowing he
app oach o Ho mann and Jos , wi h a no able excep ion [HH10, HAH11]. Since ou main
conce n he e is o ex end he app oach o a lazy se ing, we keep he linea es ic ion,
lea ing as u he wo k he adop ion o supe -linea bounds in ou analysis.
Also, ecall om Sec ion 3.1 ha he goal o any amo ised analysis is o ind a cons an
ha bounds he luc ua ions o he successi e ac ual ope a ion cos s (in o de o simpli y he
o e all bounding exp ession). Tha is he pu pose o he anno a ed ype sys ems ollowing
Ho mann and Jos ’s app oach: o ensu e he amo ised cos s a e ze o, so ha he po en ial
FCUP 15
3.2. Au oma ic Amo ised Analysis 999.
o he ini ial con igu a ion is an uppe bound o he o e all ac ual cos .
Once he ype sys em is de ined, hese ype-based amo ised analyses ob ain hei esul
au oma ically by pe o ming he ollowing 4 s eps:
1) pe o m a Damas-Milne ype in e ence [DM82] o ob ain a ype de i a ion (wi hou
anno a ion a iables);
2) deco a e he Hindley-Milne ypes [Mil78] wi h esh anno a ion a iables;
3) a e se he ype de i a ion, ga he ing linea cons ain s among anno a ion a iables
acco ding o he ules o he ype sys em;
4) eed he linea cons ain s o a s anda d linea p og amming sol e wi h he objec i e
o minimising he o e all exp ession cos .
No e ha only he i s o he las s ep may ail, i.e. ei he he p og am being analysed is no
well- yped o he ga he ed linea cons ain s canno be sol ed.
Each solu ion o he gene a ed linea p og am co esponds o a pa icula bound on he ex-
ecu ion cos . Howe e , hese bounds a e hen only use ul p o ided a co ec ness gua an ee
exis s. As such, a soundness p oo is he key esul o hese sys ems, since i es ablishes
he link be ween cos model and ype sys em. This ensu es he un- ime ac ual cos s ne e
exceed he compile- ime p edic ed bounds.
I is impo an o no e ha he analysis p oduces da a-dependen bounds. Fo example,
using an au oma ic amo ised analysis, Loidl and Jos [LJ09] lea ned ha inse ion, in hei
cos model, is gene ally mo e expensi e o a ed-black ee ha ing many black nodes, since
coe icien qbwas abou 3 imes highe han q .
In his hesis we p esen a ype-based amo ised analysis o lazy unc ional p og ams
ollowing Ho mann and Jos ’s app oach and show i s comple e de elopmen in Chap e 5
— om he chosen anno a ed ypes, o he in a ian s equi ed o he soundness p oo .
16 FCUP
999. 3. Amo isa ion
4. Cos Model
In his chap e we p esen a cos model ha allows us o measu e o al heap alloca ions. I is
gi en as an ope a ional seman ics ha o malises he cos o e alua ing an exp ession. We
de ine a cos model o wo easons: o p o e he soundness o ou analysis (Chap e 5),
i.e. o p o e ha e alua ing an exp ession ne e cos s mo e han he analysis p edic ed,
and o measu e he quali y o ou analysis agains a ange o examples (Chap e 6), i.e. o
compa e he cos s o e alua ing an exp ession wi h he cos s p edic ed by he analysis o
he same exp ession.
The cos model we p esen is buil on Encina and Pe˜
na’s co ec ed e sion [EP02] o
Ses o ’s e ision [Ses97] o Launchbu y’s na u al seman ics o lazy e alua ion [Lau93].
Launchbu y’s seman ics o ms one o he ea lies and mos widely-used ope a ional ac-
coun s o lazy e alua ion o he λ-calculus. Encina and Pe˜
na [EP02] [EP03a] subse-
quen ly p o ed ha he Spineless Tagless G-Machine [Jon92] is sound and comple e wi h
espec o one o Ses o ’s abs ac machines. Mo e ecen ly, Pi og and Bie nacki [PB10]
ha e es ablished he equi alence be ween he Spineless Tagless G-Machine and hei
ex ended e sion o he na u al seman ics o Launchbu y and Ses o . This equi alence is
e idenced by Dan y e al.’s [ADM04] unc ional co espondence be ween abs ac machines
and e alua o s. We he e o e ha e a high deg ee o con idence ha he cos model o lazy
e alua ion de eloped in his hesis is no jus heo e ically sound, bu also ha i could, in
p inciple, be ex ended o model eal implemen a ions o lazy e alua ion, such as he GHC
implemen a ion o Haskell.
Be o e looking a he cos model in Sec ion 4.3, we will see in de ail he ope a ional seman-
ics on which i is based. Howe e , we i s need o de ine he language o be used on bo h
he cos model and he analysis.
17
18 FCUP
999. 4. Cos Model
4.1 Language Syn ax
The Fun language (Figu e 4.1) is simila o he one ound in Ses o ’s e ision [Ses97] o
Launchbu y’s na u al seman ics o lazy e alua ion [Lau93]. The eade un amilia wi h he
men ioned e e ences should no e ha a gumen s o bo h applica ions and cons uc o ap-
plica ions a e es ic ed o a iables and ha his can be achie ed h ough a p ocess called
no malisa ion [Lau93], which consis s o naming he a gumen s using le exp essions.
We ha e hus a no malised λ-calculus ex ended wi h (possibly ecu si e) local bindings,
(sa u a ed) cons uc o applica ions and case exp essions.
In con as o Launchbu y and Ses o ’s language, we conside only ( o simplici y) single-
a iable le -bindings (mul iple le -bindings can be encoded, i needed, using pai s and
p ojec ions). Also, cons uc o applica ions appea only in le -bindings as in Encina and
Pe˜
na’s seman ics o lazy e alua ion [EP09]. Howe e , Encina and Pe˜
na’s mo i a ion o
such es ic ion was di e en om ou s: hey wan ed o be as close as possible o he STG
language, while we simply need o dis inguish be ween alloca ing a cons uc o and me ely
e e encing an exis ing one, since hese a e handled di e en ly by ou analysis.
As in Ses o ’s language, we do no equi e bound a iables (ei he lambda-, le - o case-
bound) o be dis inc , excep ha , o each case exp ession, each elemen in mul ise {−→
xi}
mus be dis inc , o i= 1, . . . , n. Fo example,
case eo c1x y -> x, c2y-> y
would be a alid p og am, whe eas he ollowing would no
case eo c1x x -> x, c2y-> y
4.2 Ope a ional Seman ics
Ou big-s ep ope a ional seman ics is based on Launchbu y’s na u al seman ics o lazy
e alua ion [Lau93], as subsequen ly adap ed by Ses o [Ses97], as co ec ed o case
exp essions by Encina and Pe˜
na [EP02]. Figu e 4.2 shows he se o ules ha de ine
ou ope a ional seman ics.
FCUP 19
4.2. Ope a ional Seman ics 999.
– Va iables
::= x|y– bound a iable
|l– ee a iable (loca ion)
– Exp essions
e::= – a iable
|λx. e – lambda abs ac ion
|e – applica ion
|le x=bein e– (possibly ecu si e) le -binding
|case eo {ci−→
xi-> ei}n
i=1 – case exp ession
– Augmen ed exp essions
be::= c ~ – (sa u a ed) cons uc o applica ion
|e– exp ession
– Weak head no mal o ms
w::= λx. e – lambda abs ac ion
|c~
l– cons uc o applica ion
Figu e 4.1: Language Fun
Judgemen s o he o m H,S,Lbe⇓w, H′should be ead as “in he heap H, (aug-
men ed) exp ession bee alua es o whn (weak head no mal o m) w, p oducing he new
heap H′”, whe e a heap is a pa ial unc ion mapping dis inc a iable names o hunks and
a hunk is an augmen ed exp ession (bound in he heap) ha may be u he e alua ed o
whn . No e ha , as usual (and seen in Figu e 4.1), weak head no mal o ms a e exp essions
whose ou e mos s uc u e is a lambda o a cons uc o . The auxilia y se Lo loca ions
unde e alua ion was one o he changes in oduced by Ses o ∗ o imp o e he enaming
mechanism o Launchbu y’s seman ics. The auxilia y se Swas in oduced by Encina and
Pe˜
na†in o de o ix a eshness p ope y o Ses o ’s ules, and, al hough in hei pape i
con ains he al e na i es o case exp essions {ci−→
xi-> ei}n
i=1, we simply keep he bound
a iables o such al e na i es, since hese a e su icien o ix he p oblem.
We nex de ine he se o bound a iables con ained in a Fun exp ession in o de o la e
o malise he no ion o eshness o a iables.
De ini ion 4.1 (Bound Va iables o Fun Exp essions).The bound a iables o a Fun ex-
p ession be, deno ed by BV(be), a e de ined in he usual way as shown in Figu e 4.3.
∗In [Ses97] his se is called A.
†In [EP02] his se is called C.
20 FCUP
999. 4. Cos Model
wis in whn
H,S,Lw⇓w, H(WHNF⇓)
ℓ6∈ L H,S,L∪ {ℓ}H(ℓ)⇓w, H′
H,S,Lℓ⇓w, H′[ℓ7→ w](VAR⇓)
H,S,Le⇓λx. e′,H′H′,S,Le′[ℓ/x]⇓w, H′′
H,S,Le ℓ ⇓w, H′′ (APP⇓)
ℓis esh H[ℓ7→ be[ℓ/x]],S,Le[ℓ/x]⇓w, H′
H,S,Lle x=bein e⇓w, H′(LET⇓)
H,S∪Sn
i=1 ({−→
xi} ∪ BV(ei)) ,Le⇓ck~
ℓ, H′
H′,S,Lek[~
ℓ/−→
xk]⇓w, H′′
H,S,Lcase eo {ci−→
xi-> ei}n
i=1 ⇓w, H′′ (CASE⇓)
Figu e 4.2: Lazy ope a ional seman ics
BV( ) = ∅
BV(λx. e) = {x} ∪ BV(e)
BV(e ) = BV(e)
BV(le x=bein e) = {x} ∪ BV(be)∪BV(e)
BV(case eo {ci−→
xi-> ei}n
i=1) = BV(e)Sn
i=1({−→
xi} ∪ BV(ei))
BV(c ~ ) = ∅
Figu e 4.3: Bound a iables o Fun exp essions
The ollowing auxilia y de ini ion o eshness o a iables is due o Encina and Pe˜
na [EP02]:
De ini ion 4.2 (F eshness).In a judgemen H,S,Lbe⇓w, H′a a iable is esh i i is
no in dom(H)no Sno Land i is no bound in ei he an(H)o be.
Exp essions in whn (lambda abs ac ions and cons uc o applica ions) a e al eady alues
and should he e o e e alua e o hemsel es, keeping he heap unchanged. This is e lec ed
in ule WHNF⇓.
Rule VAR⇓s a es ha in o de o e alua e a loca ion ℓ, p esen in a heap H, we e alua e
H(ℓ)wi h ℓincluded in he se o loca ions unde e alua ion. I , as a esul , we ob ain
awhn wand a heap H′, hen e alua ing ℓin He alua es o he same wand he new
heap p oduced is H′wi h a mapping upda ing ℓ o w. No e ha once ℓis upda ed i s
FCUP 21
4.2. Ope a ional Seman ics 999.
subsequen accesses ob ain he co esponding whn immedia ely, e ec i ely implemen ing
sha ing o named exp essions. Also no e ha i ℓdepends di ec ly on i sel be o e e alua ing
o whn , when a emp ing o e alua e ℓ o he second ime, no ule will apply, since ℓwill
be ma ked as being unde e alua ion in ule VAR⇓. This si ua ion is known as a “black-
hole”: a de ec ably sel -dependen in ini e loop. In Launchbu y’s seman ics, a black-hole
is de ec ed by emo ing ℓ om he heap be o e e alua ing i s con en s. Since Ses o ’s
e ision o he seman ics, black-holes can equi alen ly be de ec ed using he se o loca ions
ma ked as being unde e alua ion. In his hesis we need o keep ℓin he heap since he
mappings de ined o he in a ian s o ou soundness p oo in Chap e 5 mus apply o all
heap loca ions ( ega dless o being unde e alua ion). Thus, we use se L o de ec black-
holes (in addi ion o he bene i s ha mo i a ed i s in oduc ion).
The APP⇓ ule deals wi h unc ion applica ions and, assuming he e m is well- yped, e alu-
a ion is done in wo s eps: i s , i s exp ession eis e alua ed in he o iginal heap, p oducing
a lambda abs ac ion and an in e media e heap. Then, subs i u ing he lambda a iable by
he a gumen o he applica ion, he body o he unc ion is e alua ed in he in e media e
heap o a inal whn , p oducing a inal heap as well.
The LET⇓ ule s a s by c ea ing a esh loca ion. Then, he le -bound a iable is enamed
o his esh loca ion in all sub-exp essions. The loca ion is hen alloca ed o he heap,
mapping o he espec i e augmen ed exp ession, and he body o he le is e alua ed in
his la ge heap, wi h he esul s being ca ied o e .
Finally, ule CASE⇓ i s e alua es he case disc iminan , adding o S he bound a iables
o he case al e na i es in o de o a oid such a iables om being used as loca ions. As-
suming his e alua es o a cons uc o applica ion in an in e media e heap, hen, depending
on he cons uc o ha esul s om he e alua ion, he selec ed al e na i e is e alua ed in
he in e media e heap, subs i u ing he o mal cons uc o a gumen s by he conc e e ones.
The esul s o e alua ing he al e na i e a e hen ca ied o e as he esul s o e alua ing
he whole case exp ession. No e ha he se Swas in oduced by Encina and Pe˜
na [EP02]
o keep eshness locally checkable, a p ope y ha mo i a ed Ses o ’s e ision [Ses97] o
Launchbu y’s seman ics [Lau93].
22 FCUP
999. 4. Cos Model
To illus a e he pu pose o se S, conside he ollowing a i icial example (in lack o a
meaning ul sho one):
case (le s=Succ s in s)o Succ x -> λy. x
No e ha sis de ined as a cyclic successo o i sel and ha he expec ed esul o e alua ing
he whole exp ession is a unc ion ha disca ds i s single a gumen and e u ns he cyclic
successo . Howe e , when e alua ing le s=Succ s in s, had he lambda-bound a iable
yno been added o se S, we could ha e chosen yas a esh loca ion and, al hough no
iola ing he eshness condi ion, we would ha e ended up wi h he iden i y unc ion ins ead
as he esul , since (wi h nai e subs i u ion) he e m λy. x[y/x]is equi alen o λy. y. The
se Sa oids such a iable cap u es.
We now p esen a lemma ha s a es ha he con en s o heap loca ions ha a e unde
e alua ion a e p ese ed du ing in e media e e alua ions.
Lemma 4.3 (In a ian Loca ions Unde E alua ion).I H,S,L⊢be⇓w, H′ hen o all ℓ∈L
we ha e ℓ∈Hi ℓ∈H′and i ℓ∈H hen H′(ℓ) = H(ℓ).
P oo . By inspec ion o he ope a ional seman ics (Figu e 4.2) we obse e ha VAR⇓is
he only ule ha modi ies an exis ing loca ion ℓand ha his ule does no apply when
ℓ∈L.
4.3 Cos -ins umen ed Ope a ional Seman ics
In o de o measu e he o al numbe o heap alloca ions o a gi en p og am, we ha e
de ined a cos model by ins umen ing he ules o Figu e 4.2 wi h a non-nega i e coun e
as shown in Figu e 4.4.
In he new ules, judgemen s o he o m H,S,Lmbe⇓w, H′should be ead as “in he
heap H, exp ession bee alua es o whn w, p oducing he new heap H′, and mnew heap
cells ha e been alloca ed”.
Fo simplici y, bu wi hou loss o gene ali y, we choose a uni o m cos -model whe e e al-
ua ion cos s one (heap) uni o each esh heap loca ion ( ega dless o i s con en ) ha
is needed du ing e alua ion — essen ially coun ing he numbe o new loca ions in he
FCUP 23
4.3. Cos -ins umen ed Ope a ional Seman ics 999.
wis in whn
H,S,L0w⇓w, H(WHNF⇓C)
ℓ6∈ L H,S,L∪ {ℓ}mH(ℓ)⇓w, H′
H,S,Lmℓ⇓w, H′[ℓ7→ w](VAR⇓C)
H,S,Lme⇓λx. e′,H′H′,S,Lm′e′[ℓ/x]⇓w, H′′
H,S,Lm+m′e ℓ ⇓w, H′′ (APP⇓C)
ℓis esh H[ℓ7→ be[ℓ/x]],S,Lme[ℓ/x]⇓w, H′
H,S,L1 + mle x=bein e⇓w, H′(LET⇓C)
H,S∪Sn
i=1 ({−→
xi} ∪ BV(ei)) ,Lme⇓ck~
ℓ, H′
H′,S,Lm′ek[~
ℓ/−→
xk]⇓w, H′′
H,S,Lm+m′case eo {ci−→
xi-> ei}n
i=1 ⇓w, H′′ (CASE⇓C)
Figu e 4.4: Cos -ins umen ed lazy ope a ional seman ics
heap (i.e. he numbe o newly alloca ed loca ions). We could ha e chosen o he me -
ics [JLH+09], modelling he usage o o he coun able esou ces such as execu ion ime o
s ack space, bu we belie e his simplici y has allowed us o ocus on he p inciples needed
o de elop a esou ce analysis o call-by-need. Cos -me ic e inemen s a e le o u he
wo k.
The only change in oduced in Figu e 4.4 wi h espec o Figu e 4.2 is he in oduc ion o
he non-nega i e alue abo e he u ns ile. This alue co esponds o he cos o e alua ion
in e ms o quan i y o heap cells equi ed. We will now desc ibe how he ules in Figu e 4.4
a ec his o al heap alloca ion coun e .
As we ha e seen, ule WHNF⇓lea es he heap unchanged. Thus, no heap cells a e
alloca ed in ule WHNF⇓C, co esponding o a cos o ze o.
In ules APP⇓Cand CASE⇓C he cos o e alua ion is he sum o he cos s o each o he wo
e alua ion s eps.
Rule VAR⇓Cs a es ha he cos o e alua ing a loca ion ℓis he cos o e alua ing he
co esponding heap exp ession H(ℓ). No e ha al hough he esul ing heap is upda ed, ℓ
was al eady in he domain o H′(by Lemma 4.3) and hus no new heap cell was added a
ha poin which jus i ies he p ese a ion o cos m.
Rule LET⇓Cis he only ule ha e ec i ely alloca es heap cells, cos ing one heap cell o he
30 FCUP
999. 5. Amo ised Analysis
.(A| ∅)(SHAREEMPTY)
.(X|X,...,X)(SHAREVAR)
Bi=µX.c1: (p′
i1,~
Bi1)|···|cm: (p′
im,~
Bim)
.~
Aj~
B1j, . . . , ~
Bnj pj≥Pn
i=1 p′
ij (1 ≤i≤n, 1≤j≤m)
.µX.c1: (p1,~
A1)|···|cm: (pm,~
Am)|B1, . . . , Bn(SHAREDAT)
.(Ai|A).(B|Bi)qi≥q(1 ≤i≤n)
.A−→
qBA1−→
q1B1, . . . , An−→
qnBn(SHAREFUN)
.(Aj|B1j, . . . , Bnj )m=~
A=~
Bi(1 ≤i≤n, 1≤j≤m)
.~
A~
B1, . . . , ~
Bn(SHAREVEC)
.(A|A1,...,An)qi≥q(1 ≤i≤n)
.(Tq(A)|Tq1(A1),...,Tqn
(An)) (SHARETHUNK)
Figu e 5.2: Sha ing ela ion
.(Γ | ∅)(SHAREEMPTYCTX)
.(A|B1,...,Bn).(Γ |∆)
.(x:A, Γ|x:B1,...,x:Bn,∆) (SHARECTX)
Figu e 5.3: Sha ing ela ion ex ended o con ex s
do no . The las h ee sha ing examples ail since in he i s o hese a yping o yappea s
only a he igh -hand side o he sha ing ela ion; in he second, he po en ial on he le -
hand side is no linea ly dis ibu ed wi h espec o he igh -hand side (56≤ 3 + 3); and
he las example ails since sha ing is con a a ian in he le a gumen o unc ions and
hus, while he cos o he ou e mos hunk ype on he igh -hand side can exceed he
co esponding cos on he le -hand side, he cos o he inne hunk ype canno .
5.2.1 Sub yping Rela ion
Sha ing also allows he elaxa ion o anno a ions o subsume sub yping. The special case
o sha ing one ype o a single o he co esponds o a sub yping ela ion; we de ine he
sho hand no a ion A <:B o mean .(A|B). Inequali ies o e ype anno a ions in ules
SHAREDAT, SHAREFUN and SHARETHUNK allow po en ial anno a ions o dec ease and
cos anno a ions o inc ease. In o mally, A <:Bimplies no only ha Aand Bha e iden ical
FCUP 31
5.2. Sha ing Rela ion 999.
unde lying ypes, bu also ha Bhas lowe o equal po en ial and g ea e o equal cos han
ha o A. As usual in s uc u al sub yping, his ela ion is con a a ian in he le a gumen
o unc ions (SHAREFUN).
5.2.2 Idempo en Types
We now de ine he no ion ha some ypes can be eely sha ed. Namely, i hey obse e
he ollowing de ini ion:
De ini ion 5.1 (Idempo en Types and Idempo en Con ex s).We say ype A( espec i ely
con ex Γ) is idempo en i .(A|A, A)( espec i ely .(Γ |Γ,Γ)) holds.
This special case occu s when sha ing a ype o con ex o i sel : because o non-nega i i y,
.(A|A, A)( espec i ely .(Γ |Γ,Γ)) equi es he po en ial anno a ions in A( espec i ely Γ)
o be ze o o all da a ypes ou side o unc ion ypes.
No e hough ha unc ion ypes a e una ec ed by his special case o sha ing. Howe e ,
since unc ion ypes do no ca y po en ial pe se ( he po en ial equi ed o execu e he body
o a unc ion mus come om i s a gumen s), all ypes subjec o such cons ain ca y no
po en ial.
Fo example, ypes
T1(µX.{Uni :(0,())})
T1(T1(µX.{Uni :(1,())})−→
1B)
T1(µX.{Cons:(0,(T1(µX.{Uni :(0,())}),T1(X))) | Nil:(0,())})
a e idempo en , whe eas ypes
T1(µX.{Uni :(1,())})
T1(µX.{Cons:(1,(T1(µX.{Uni :(0,())}),T1(X))) | Nil:(0,())})
T1(µX.{Cons:(0,(T1(µX.{Uni :(0,())}),T1(X))) | Nil:(1,())})
a e no .
We use his p ope y o impose a cons ain ha ypes o con ex s ca y no po en ial. A
a ian o his is .(A|A, A′), which implies ha A′is a sub ype o A ha holds no po en ial.
32 FCUP
999. 5. Amo ised Analysis
5.3 Typing Judgemen s
Ou analysis o lazy e alua ion is p esen ed in Figu es 5.4 and 5.5 as a p oo sys em
ha de i es judgemen s o he o m Γqbe:A, whe e Γis a yping con ex , beis an
augmen ed exp ession, Ais an anno a ed ype and q(abo e he u ns ile) is a non-nega i e
a ional numbe app oxima ing he cos o e alua ing be. Fo simplici y, we will omi u ns ile
anno a ions whene e hey a e no explici ly men ioned.
In he LET ule, he cos q′o e alua ing beis de e ed by mo ing i o he hunk ype o xin he
ype judgemen o e. I xdoes no occu in e hen i s cos can be disca ded, in acco dance
wi h lazy e alua ion. Also, ype A′is es ic ed o being idempo en in o de o p e en he
po en ial o x om being eused in he de i a ion o be, keeping po en ial om being ob ained
o ee in he ecu si e de ini ion. Finally, he o e all cos o he le exp ession is 1 o he
newly alloca ed heap cell (acco ding o he cos model) plus he cos qo e alua ing he
body eand, i beis a cons uc o , i s po en ial p′is also added o he o e all cos . No e ha
he hunk cos o xin he ype judgemen o beis q′, ins ead o always ze o as in a p e ious
p esen a ion [SVF+12]. This change allowed us o ix a mino p oblem in he soundness
p oo o he main heo em.
VAR mo es he cos om he hunk ype o he u ns ile, ensu ing ha any cos in he hunk
ype is paid o a his poin o access in a ype de i a ion.
In he ABS ule, he cos o e en ually applying he λ-abs ac ion is q, bu he cos o
e alua ing he λ-abs ac ion i sel is ze o, since i is al eady a whn . In o de o a oid
duplica ing po en ial whe e a λ-abs ac ion is applied mo e han once, ABS ensu es ha Γ
is idempo en , by o cing i o sha e wi h i sel . While on he one hand his means unc ions
can be eused a bi a ily wi hou isking unsound duplica ion o po en ial, on he o he hand
unc ions mus ob ain all hei equi ed po en ial, o he han a cons an amoun , om hei
inpu a gumen xalone and no om o he a iables in dom(Γ).
APP ensu es ha he a gumen and unc ion ypes ma ch and includes he cos o he
unc ion in he inal esul .
The CONS ule simply ensu es consis ency be ween he a gumen s and he esul ype.
Since cons uc o s canno appea in sou ce o ms, he ule is used only when we need o
assign ypes ei he o heap exp essions o o e alua ion esul s. No e ha while ule LET
FCUP 33
5.3. Typing Judgemen s 999.
Γ, x:Tq′(A′)q′be:A∆, x:Tq′(A)qe:C
x6∈ dom(Γ,∆) .(A|A, A′)q′= 0 i beis a whn
p=p′,i be≡c ~y and A=µX.{· · · |c: (p′,~
B)|· · · }
0,o he wise
Γ,∆1 + q+ple x=bein e:C(LET)
x:Tq(A)qx:A(VAR)
Γ, x:Aqe:C x 6∈ dom(Γ) .(Γ |Γ,Γ)
Γ0λx.e :A−→
qC(ABS)
Γqe:A−→
q′
C
Γ, y:Aq+q′e y :C(APP)
B=µX.{· · · |c: (p, ~
A)|· · · }
y1:A1[B/X],...,yk:Ak[B/X]0c ~y :B(CONS)
Γqe:B B =µX.{c1: (p1,−→
A1)|···|cn: (pn,−→
An)}
(Sn
i=1{−→
xi})∩dom(∆) = ∅
i= 1, . . . , n (|−→
Ai|=|−→
xi|=ki
∆, xi1:Ai1[B/X],...,xiki:Aiki[B/X]q′+piei:C
Γ,∆q+q′case eo {ci−→
xi-> ei}n
i=1 :C(CASE)
Figu e 5.4: Syn ax di ec ed ype ules
mus ensu e ha su icien po en ial (p′) is a ailable o he cons uc o , he CONS ule does
no — he o me co esponds o alloca ing a cons uc o , he la e o me ely e e encing
one.
The CASE ule deals wi h pa e n-ma ching o e an exp ession o a (possibly ecu si e) da a
ype. The ule equi es ha all b anches o he al e na i es admi an iden ical esul ype
and ha pa o he es ima ed cos o each al e na i e b anch is he same; ul illing such
a condi ion may equi e he elaxa ion o ype and/o cos in o ma ion using he s uc u al
ules desc ibed below. The ma ching b anch uses ex a esou ces co esponding o he
po en ial anno a ion on he ma ched cons uc o , p e iously se aside a he in oduc ion o
he cons uc o (LET).
The s uc u al ules o Figu e 5.5 allow he analysis o be elaxed in a ious ways. Rule
WEAK allows he in oduc ion o an ex a hypo hesis in he yping con ex and he side
condi ion ensu es ype Amus be s uc u ally equi alen o any o Γ↾x, i Γ↾xis no emp y,
p e en ing ill- o med con ex s, such as {x:Bool, x:Lis }. RELAX allows a gumen cos s o
be elaxed. SUPERTYPE and SUBTYPE allow supe yping in a hypo hesis and sub yping
34 FCUP
999. 5. Amo ised Analysis
Γqe:C.(A′|(Γ, x:A)↾x)
Γ, x:Aqe:C(WEAK)
Γq′e:A q ≥q′
Γqe:A(RELAX)
Γ, x:Bqe:C A <:B
Γ, x:Aqe:C(SUPERTYPE)
Γqe:B B <:C
Γqe:C(SUBTYPE)
Γ, x:A1, x:A2qe:C.(A|A1, A2)
Γ, x:Aqe:C(SHARE)
Γ, x:Tq′
0(A)qe:C
Γ, x:Tq′
0+q′(A)q+q′e:C(PREPAY)
Figu e 5.5: S uc u al ype ules
in he conclusion, espec i ely. SHARE allows he use o sha ing o spli po en ial in a
hypo hesis. Finally, PREPAY allows (pa o all o ) he cos o a hunk o be paid o , so
educing he cos o u he uses.
I is impo an o no e ha a dec ease o cos anno a ions o hunks (possibly down o ze o)
can only be achie ed h ough he PREPAY s uc u al ule and no h ough he sha ing ules
o Figu e 5.2. Wi hou PREPAY he sys em would model call-by-name, since each access
o a a iable would pay o he en i e cos . Also, i we would o ce he use o PREPAY o
he en i e cos a e each LET, we would be modelling call-by- alue: pay in ull once a
in oduc ion (LET) and pay ze o a e e y access (VAR). I is he abili y o selec i ely choose
when o use PREPAY ha enables he sys em o model call-by-need. Thus, “p epaying”
is key o co ec ly modelling he educed cos s o lazy e alua ion by allowing cos s o be
accoun ed only once o a hunk, i a all.
5.4 Example: Analysing Call-By-Need
We now p esen ype de i a ions o he examples om Sec ion 4.4 in o de o illus a e how
he ype ules o Figu es 5.4 and 5.5 e lec he cos s o ou ope a ional seman ics.
FCUP 35
5.4. Example: Analysing Call-By-Need 999.
5.4.1 Non-S ic E alua ion
Recall example (4.1) which demons a es ha unneeded edexes a e no educed (i.e. ha
he seman ics is non-s ic ):
le z=zin (λx. λy.y)z
E alua ion o his e m in ou ope a ional seman ics succeeds, equi es one heap cell ( o
alloca ing he hunk named by z) and he esul is he iden i y unc ion λy.y:
H,S,L1le z=zin (λx. λy.y)z⇓λy.y,H′
An analysis o his e m is gi en in Figu e 5.6 as an anno a ed ype de i a ion.∗
The inal judgemen is:
∅1le z=zin (λx.λy.y)z:Tq(B)−→
qB
The anno a ion in he u ns ile o his judgemen gi es a cos es ima e o one heap cell,
ma ching he exac cos o he ope a ional seman ics. The ype anno a ion q ep esen s he
cos o he hunk bound o he conc e e a gumen o he iden i y unc ion λy.y. The alue o
qcan be a bi a y. So can ype B. No e ha ype A′is simila ly a bi a y, subjec only o he
side condi ion .(A′|A′, A′), o bidding ci cula da a o ha ing po en ial.
5.4.2 Lazy E alua ion
The second example (4.2) illus a es he sha ing o no mal o ms, i.e. lazy e alua ion:
le =le z=zin (λx. λy.y)z
in le i=λx.xin le = i in
E alua ing o ces he hunk named by ; ollowing e alua ion, he loca ion associa ed
wi h is upda ed wi h a whn . Subsequen e alua ions o e-use his esul . E alua ion o
∗Fo he comple e de i a ion see Figu e B.1 in Appendix B.
36 FCUP
999. 5. Amo ised Analysis
VAR
z:Tq′′A′q′′
z:A′
...
z:Tq′′A′0(λx.λy.y)z:Tq(B)−→
qBLET
∅1le z=zin (λx.λy.y)z:Tq(B)−→
qB
whe e .(A′|A′, A′)
Figu e 5.6: Type de i a ion o a non-s ic e alua ion example
he o e all exp ession he e o e cos s 4 heap cells (as seen in Figu e 4.5, Chap e 4):
∅,∅,∅4(4.2) ⇓λx.x,[ℓ07→ λy.y, ℓ17→ λx.x, ℓ27→ λx.x, ℓ37→ ℓ3]
The ype de i a ion in Figu e 5.7 shows he analysis o his example.†
The inal ype judgemen eplica es he exac ope a ional cos o 4 heap cells:
∅4(4.2) :B, whe e B=Tq′(C)−→
q′
C
No e ha we employ he s uc u al ype ule SHARE o allow he unc ion o be used wice.
The duplica ion is jus i ied since he ype o is idempo en (i.e. i sha es o i sel ).
The c ucial poin in his ype de i a ion ha allows us o ma ch he exac ope a ional cos is
he use o he s uc u al ule PREPAY (below SHARE) o pay, p ecisely once, he cos o he
hunk bound o .
Also no e ha al hough he ype de i a ion cons ains B=Tq′(C)−→
q′
C o be idempo en ,
i.e. .(B|B, B ), i lea es ype Cuncons ained.
5.5 Soundness
This sec ion es ablishes he soundness o ou analysis o lazy e alua ion wi h espec o
he cos model o Sec ion 4.3.
We begin by s a ing some auxilia y p oo lemmas and p elimina y de ini ions, no ably o -
malising he no ion o po en ial. We hen de ine he p incipal in a ian s o ou sys em,
namely, ype consis ency and ype compa ibili y ela ions be ween a heap con igu a ion o
†Fo he comple e de i a ion see Figu e B.2 in Appendix B.
FCUP 37
5.5. Soundness 999.
(Figu e 5.6,whe e q= 0) WEAK
:T1(T0
(B)−→
0B)1le z=zin (λx.λy.y)z:T0
(B)−→
0B
...
i:T0(B)0λx.x:B
...
:T0(T0
(B)−→
0B),
:T0(T0
(B)−→
0B),i:T0(B)1le = i in :BSHARE
:T0(T0
(B)−→
0B),i:T0(B)1le = i in :BPREPAY
:T1(T0
(B)−→
0B),i:T0(B)2le = i in :BLET
:T1(T0
(B)−→
0B)3le i=λx.xin ...:BLET
∅4le = (le z=zin (λx.λy.y)z)in le i=λx.xin le = i in :B
whe e B = Tq′(C)−→
q′
C
Figu e 5.7: Type de i a ion o a lazy-e alua ion example
he ope a ional seman ics and global ypes, con ex s and balance. We conclude wi h he
soundness esul p ope (Theo em 5.13).
5.5.1 Auxilia y Lemmas
The i s auxilia y lemma allows us o eplace a iables in ype de i a ions. No e ha
because o he lazy e alua ion seman ics (and unlike he usual subs i u ion lemma o he
λ-calculus), we subs i u e only wi h a iables bu no wi h a bi a y exp essions. Also, since
ou yping con ex s a e mul ise s, we need o ensu e he simul aneous subs i u ion o all
ypings o he a iable in he con ex .
Lemma 5.2 (Subs i u ion).I Γ, x:A1,...,x:An
qbe:Cand x6∈ dom(Γ) and y /∈dom(Γ) ∪
FV(be) hen also Γ, y:A1,...,y:An
qbe[y/x] : C.
P oo . By induc ion on he heigh o de i a ion o Γ, x:A1,...,x:An
qbe:C, simply eplac-
ing any occu ences o x o y.
The nex wo lemmas es ablish in e sion p ope ies o cons uc o s and λ-abs ac ions.
Lemma 5.3 (CONS In e sion).I Γ0c ~y :B hen B=µX.{· · · | c: (p, ~
A)| · · · } and
.(Γ |y1:A1[B/X], . . . , yk:Ak[B/X]).
38 FCUP
999. 5. Amo ised Analysis
Lemma 5.4 (ABS In e sion).I Γ0λx.e :A−→
qC hen he e exis s Γ′such ha .(Γ |Γ′),
.(Γ′|Γ′,Γ′),x /∈dom(Γ′)and Γ′, x:Aqe:C.
P oo Ske ch ( o bo h lemmas). A yping wi h conclusion Γ0c ~y :Bmus esul om ax-
iom CONS ollowed by (possibly ze o) uses o s uc u al ules. Simila ly, a yping Γ0λx.e :
A−→
qCmus esul om an applica ion o he ule ABS ollowed by (possibly ze o) uses o
s uc u al ules. The p oo ollows by induc ion on he s uc u al ules, conside ing each ule
sepa a ely. Fo ules RELAX and PREPAY induc ion is i ial since bo h ype judgemen s
ha e ze o on he u ns ile. Fo he emaining s uc u al ules he p oo ollows by ansi i i y
o he sha ing ela ion. See Sec ion 5.5.6.2 and 5.5.6.3, espec i ely, o he de ailed
p oo s.
No e ha , o a yping judgemen wi h any numbe g ea e han ze o on he u ns ile,
in e sion in ou ype sys em would no hold in gene al. The eason is ha wo (mu-
ually exclusi e) ules migh apply. Fo example x:T1(A)1e:Cmigh ha e p emise
x:T1(A)0e:C h ough ule RELAX, o i migh ha e p emise x:T0(A)0e:C h ough
ule PREPAY. This is no a p oblem since he p oo s we p esen in ou sys em do no equi e
in e sion lemmas wi h a numbe o he han ze o on he u ns ile o he yping judgemen s.
The inal auxilia y lemma allows spli ing con ex s used o yping exp essions in whn
acco ding o a spli o he esul ype.
Lemma 5.5 (Con ex Spli ing).I Γ0w:A, whe e wis an exp ession in whn and
.(A|A1, A2); hen he e exis Γ1,Γ2such ha .(Γ |Γ1,Γ2),Γ10w:A1and Γ20w:A2.
P oo Ske ch. The p oo ollows om an applica ion o Lemma 5.3 (i wis a cons uc o )
o Lemma 5.4 (i wis an abs ac ion) oge he wi h he de ini ion o sha ing. See Sec-
ion 5.5.6.4 o he de ailed p oo .
5.5.2 Global Types, Con ex s and Balance
We now de ine some auxilia y mappings ha will be necessa y o o mula ing he sound-
ness o ou ype sys em.
The mapping M om loca ions o ypes, w i en {ℓ17→ A1,...,ℓn7→ An}, eco ds he global
ype o a loca ion, which accoun s o all po en ial in all e e ences o ha loca ion.
FCUP 39
5.5. Soundness 999.
We ex end sub yping o global ypes in he na u al way, namely M<:M′i and only i
dom(M)⊆dom(M′)and o all ℓ∈dom(M)we ha e M(ℓ)<:M′(ℓ). This ela ion will be
used o asse ha he po en ial assigned o global ypes is always non-inc easing du ing
execu ion.
The mapping C om loca ions o yping con ex s, w i en {ℓ17→ Γ1,...,ℓn7→ Γn}, associa es
each loca ion wi h i s global con ex ha jus i ies i s global ype.
We also ex end he p ojec ion ope a ion om (local) con ex s o global con ex s in he na u al
way:
C↾ℓ={ℓ17→ Γ1,...,ℓn7→ Γn}↾ℓ
de
= (Γ1,...,Γn)↾ℓ
Fu he mo e, we in oduce an auxilia y balance (o lazy po en ial) mapping B om loca ions
o non-nega i e a ional numbe s.
The balance mapping will be used o keep ack o he pa ial cos s o hunks ha ha e been
paid in ad ance by applica ions o he PREPAY ule.
No e ha hese auxilia y mappings a e needed only in he soundness p oo o he analysis
o bookkeeping pu poses, bu a e no pa o he ope a ional seman ics — in pa icula ,
hey do no incu un- ime cos s.
5.5.3 Po en ial
We now de ine he po en ial o an augmen ed exp ession wi h espec o a heap and an
anno a ed ype.
De ini ion 5.6 (Po en ial).The po en ial assigned o an augmen ed exp ession beo ype A
unde heap H, w i en φH(be:A), is de ined in (5.1) wi hin Figu e 5.8.
The po en ial o da a cons uc o s is ob ained by summing he ype anno a ion wi h he
(possibly ecu si e) po en ial con ibu ed by each o he a gumen s. No e how he po en ial
o da a cons uc o s is unw apped om hunk ypes. The po en ial o exp essions o he han
da a cons uc o s is always ze o.
Equa ion (5.2) ex ends he de ini ion o yping con ex s in he na u al way. Equa ion (5.3)
de ines po en ial o global con ex s, bu conside s only hunks ha a e no unde e alua ion.
46 FCUP
999. 5. Amo ised Analysis
5.5.6.2 In e sion Lemma o Cons uc o s
Lemma 5.3 (CONS In e sion).I Γ0c ~y :B hen B=µX.{· · · | c: (p, ~
A)| · · · } and
.(Γ |y1:A1[B/X],...,yk:Ak[B/X]).
P oo . A yping wi h conclusion Γ0c ~y :Bmus esul om axiom CONS ollowed by
(possibly ze o) uses o s uc u al ules. The p oo ollows by induc ion on he s uc u al
ules, conside ing each ule sepa a ely. Fo ules RELAX and PREPAY induc ion is i ial
since bo h ype judgemen s ha e ze o on he u ns ile. Fo he emaining s uc u al ules he
p oo ollows by ansi i i y o he sha ing ela ion. We now conside each o he emaining
s uc u al ules.
Case WEAK:We ha e Γ, xn+1:Cn+1 0c ~y :B. Applying induc ion o he p emise o ule
WEAK Γ0c ~y :Bwe ob ain
B=µX.{· · · |c: (p, ~
A)|· · · }
as equi ed o he conclusion, and
.(Γ |y1:A1[B/X],...,yk:Ak[B/X])
Le Γ = {x1:C1,...,xn:Cn}. By he de ini ion o sha ing (Figu e 5.3) we know ha
.(x1:C1,...,xn:Cn|y1:A1[B/X],...,yk:Ak[B/X])
i he e is a pa i ion ∆1,...,∆no {y1:A1[B/X],...,yk:Ak[B/X]}such ha .(xi:Ci|∆i)
holds and dom(∆i)⊆ {xi}, o (1 ≤i≤n).
Le ∆n+1 =∅. Since .(xn+1:Cn+1 |∆n+1 )holds (by SHAREEMPTYCTX) and dom(∆n+1)⊆
{xn+1}, again by de ini ion o sha ing we ha e
.(Γ, xn+1:Cn+1 |y1:A1[B/X],...,yk:Ak[B/X])
as equi ed.
FCUP 47
5.5. Soundness 999.
Case SUPERTYPE:We ha e Γ, xn+1:C′
n+1 0c ~y :B. The p emises o ule SUPERTYPE
a e Γ, xn+1:Cn+1 0c ~y :Band .C′
n+1 |Cn+1 . Applying induc ion o Γ, xn+1:Cn+1 0c ~y :
Bwe ob ain
B=µX.{· · · |c: (p, ~
A)|· · · }
as equi ed o he conclusion, and
.(Γ, xn+1:Cn+1 |y1:A1[B/X],...,yk:Ak[B/X])
Le Γ = {x1:C1,...,xn:Cn}. By he de ini ion o sha ing (Figu e 5.3) we know ha
.(x1:C1,...,xn:Cn, xn+1:Cn+1 |y1:A1[B/X],...,yk:Ak[B/X])
i he e is a pa i ion ∆1,...,∆n,∆n+1 o {y1:A1[B/X],...,yk:Ak[B/X]}such ha
.(xi:Ci|∆i)holds and dom(∆i)⊆ {xi}, o (1 ≤i≤n+ 1).
F om .C′
n+1 |Cn+1 and .(xn+1:Cn+1 |∆n+1 )by he ansi i i y o sha ing we ha e
.xn+1:C′
n+1 |∆n+1
Thus by de ini ion o sha ing we ha e
.Γ, xn+1:C′
n+1 |y1:A1[B/X],...,yk:Ak[B/X]
as equi ed.
Case SUBTYPE:We ha e Γ0c ~y :C. The p emises o ule SUBTYPE a e Γ0c ~y :B
and .(B|C). Applying induc ion o Γ0c ~y :Bwe ob ain
B=µX.{· · · |c: (p, ~
A)|· · · }
and
.(Γ |y1:A1[B/X],...,yk:Ak[B/X])
F om .(B|C)we know
C=µX.{· · · |c: (p′,~
A′)|· · · }
48 FCUP
999. 5. Amo ised Analysis
whe e p≤p′and .~
A~
A′. Also, .(yi:Ai[B/X]|yi:A′
i[C/X]) o (1 ≤i≤k). By he
ansi i i y o sha ing we ob ain
.(Γ |y1:A′
1[C/X],...,yk:A′
k[C/X])
as equi ed.
Case SHARE:We ha e Γ, x:C′0c ~y :B. Applying induc ion o he p emise o ule
SHARE Γ, x:C′
1, x:C′
20c ~y :Bwe ob ain
B=µX.{· · · |c: (p, ~
A)|· · · }
as equi ed o he conclusion, and
.(Γ, x:C′
1, x:C′
2|y1:A1[B/X],...,yk:Ak[B/X])
Le Γ = {x1:C1,...,xn:Cn}. By he de ini ion o sha ing (Figu e 5.3) we know ha
.(x1:C1,...,xn:Cn, x:C′
1, x:C′
2|y1:A1[B/X],...,yk:Ak[B/X])
i he e is a pa i ion ∆1,...,∆n,∆′
1,∆′
2o {y1:A1[B/X],...,yk:Ak[B/X]}such ha
.(xi:Ci|∆i)holds and dom(∆i)⊆ {xi}, o (1 ≤i≤n), and .(x:C′
1|∆′
1),.(x:C′
2|∆′
2)
hold and dom(∆′
1∪∆′
2)⊆ {x}.
F om .(x:C′
1|∆′
1)and .(x:C′
2|∆′
2)we ha e .(x:C′
1, x:C′
2|∆′
1,∆′
2). F om .(C′|C′
1, C′
2)
(also p emise o ule SHARE) and he ansi i i y o sha ing we ha e .(x:C′|∆′
1,∆′
2). By
de ini ion o sha ing we ha e
.(Γ, x:C′|y1:A1[B/X],...,yk:Ak[B/X])
as equi ed.
This concludes he p oo o he CONS In e sion.
FCUP 49
5.5. Soundness 999.
5.5.6.3 In e sion Lemma o λ-abs ac ions
Lemma 5.4 (ABS In e sion).I Γ0λx.e :A−→
qC hen he e exis s Γ′such ha .(Γ |Γ′),
.(Γ′|Γ′,Γ′),x /∈dom(Γ′)and Γ′, x:Aqe:C.
P oo . A yping Γ0λx.e :A−→
qCmus esul om an applica ion o he ule ABS ollowed
by (possibly ze o) uses o s uc u al ules. The p oo ollows by induc ion on he s uc u al
ules, conside ing each ule sepa a ely. Fo ules RELAX and PREPAY induc ion is i ial
since bo h ype judgemen s ha e ze o on he u ns ile. Fo he emaining s uc u al ules he
p oo ollows by ansi i i y o he sha ing ela ion. We now conside each o he emaining
s uc u al ules.
Case WEAK:We ha e Γ, yn+1:Bn+1 0λx.e :A−→
qCand, as a p emise o ule WEAK,
Γ0λx.e :A−→
qC
Applying induc ion o Γ0λx.e :A−→
qCwe ob ain Γ′such ha .(Γ |Γ′),.(Γ′|Γ′,Γ′),
x /∈dom(Γ′)and Γ′, x:Aqe:C.
Le Γ = {y1:B1,...,yn:Bn}. By he de ini ion o sha ing (Figu e 5.3) we know ha
.(y1:B1,...,yn:Bn|Γ′)
i he e is a pa i ion ∆1,...,∆no Γ′such ha .(yi:Bi|∆i)holds and dom(∆i)⊆ {yi}, o
(1 ≤i≤n).
Le ∆n+1 =∅. F om SHAREEMPTYCTX we ha e .(yn+1:Bn+1 |∆n+1 ). By he de ini ion o
sha ing we ha e
.(Γ, yn+1:Bn+1 |Γ′)
as equi ed.
Case SUPERTYPE:We ha e Γ, yn+1:B′
n+1 0λx.e :A−→
qCand, as a p emise o ule
SUPERTYPE,
Γ, yn+1:Bn+1 0λx.e :A−→
qC
50 FCUP
999. 5. Amo ised Analysis
whe e .B′
n+1 |Bn+1 . Applying induc ion o Γ, yn+1:Bn+1 0λx.e :A−→
qCwe ob ain Γ′
such ha .(Γ, yn+1:Bn+1 |Γ′),.(Γ′|Γ′,Γ′),x /∈dom(Γ′)and Γ′, x:Aqe:C.
Le Γ = {y1:B1,...,yn:Bn}. By he de ini ion o sha ing (Figu e 5.3) we know ha
.(y1:B1,...,yn:Bn, yn+1:Bn+1 |Γ′)
i he e is a pa i ion ∆1,...,∆n,∆n+1 o Γ′such ha .(yi:Bi|∆i)holds and dom(∆i)⊆
{yi}, o (1 ≤i≤n+ 1).
F om .B′
n+1 |Bn+1 and .(yn+1:Bn+1 |∆n+1 )by he ansi i i y o sha ing we ha e
.yn+1:B′
n+1 |∆n+1
Thus, by he de ini ion o sha ing we ob ain
.Γ, yn+1:B′
n+1 |Γ′
as equi ed.
Case SUBTYPE:We ha e Γ0λx.e :A′−→
q′
C′and, as a p emise o ule SUBTYPE,
Γ0λx.e :A−→
qC
whe e .A−→
qCA′−→
q′
C′. Applying induc ion o Γ0λx.e :A−→
qCwe ob ain Γ′such
ha .(Γ |Γ′),.(Γ′|Γ′,Γ′),x /∈dom(Γ′)and Γ′, x:Aqe:C.
F om .A−→
qCA′−→
q′
C′we know q≤q′,.(A′|A)and .(C|C′).
F om Γ′, x:Aqe:Capplying ules SUPERTYPE (wi h .(A′|A)), RELAX (wi h q≤q′) and
SUBTYPE (wi h .(C|C′)) we ob ain
Γ′, x:A′q′e:C′
as equi ed.
FCUP 51
5.5. Soundness 999.
Case SHARE:We ha e Γ, y:B′0λx.e :A−→
qCand, as a p emise o ule SHARE,
Γ, y:B′
1, y:B′
20λx.e :A−→
qC
whe e .(B′|B′
1, B′
2). Applying induc ion o Γ, y:B′
1, y:B′
20λx.e :A−→
qCwe ob ain Γ′
such ha .(Γ, y:B′
1, y:B′
2|Γ′),.(Γ′|Γ′,Γ′),x /∈dom(Γ′)and Γ′, x:Aqe:C.
Le Γ = {y1:B1,...,yn:Bn}. By he de ini ion o sha ing (Figu e 5.3) we know ha
.(y1:B1,...,yn:Bn, y:B′
1, y:B′
2|Γ′)
i he e is a pa i ion ∆1,...,∆n,∆′
1,∆′
2o Γ′such ha .(yi:Bi|∆i)holds and dom(∆i)⊆
{yi}, o (1 ≤i≤n), and .(y:B′
1|∆′
1)and .(y:B′
2|∆′
2)hold, and dom(∆′
1∪∆′
2)⊆ {y}.
F om .(y:B′
1|∆′
1)and .(y:B′
2|∆′
2)we ha e .(y:B′
1, y:B′
2|∆′
1,∆′
2). F om .(B′|B′
1, B′
2)and
he ansi i i y o sha ing we ha e .(y:B′|∆′
1,∆′
2). By de ini ion o sha ing we ha e
.(Γ, y:B′|Γ′)
as equi ed.
This concludes he p oo o he ABS In e sion.
We now p esen he p oo o Lemma 5.5 (Con ex Spli ing), ollowed by he p oo o
Lemma 5.7 (Po en ial Spli ing).
5.5.6.4 Con ex Spli ing Lemma
Lemma 5.5 (Con ex Spli ing).I Γ0w:A, whe e wis an exp ession in whn and
.(A|A1, A2); hen he e exis Γ1,Γ2such ha .(Γ |Γ1,Γ2),Γ10w:A1and Γ20w:
A2.
P oo . Exp ession wis ei he a cons uc o applica ion o a λ-abs ac ion. The p oo ollows
by conside ing he wo cases sepa a ely.
Z/A A/B B/Z
52 FCUP
999. 5. Amo ised Analysis
Case w=c ~y:We ha e Γ0c ~y :Aand .(A|A1, A2). By applying Lemma 5.3 we ob ain
A=µX.{· · · |c: (p, ~
B)|· · · } and .(Γ |y1:B1[A/X],...,yk:Bk[A/X]). F om .(A|A1, A2)
we also ob ain
A1=µX.{· · · |c: (p′,~
B′)|· · · }
A2=µX.{· · · |c: (p′′,~
B′′)|· · · }
Applying ule CONS we ob ain
y1:B′
1[A1/X],...,yk:B′
k[A1/X]0c ~y :A1
y1:B′′
1[A2/X],...,yk:B′′
k[A2/X]0c ~y :A2
as equi ed, by conside ing
Γ1=y1:B′
1[A1/X],...,yk:B′
k[A1/X]
Γ2=y1:B′′
1[A2/X],...,yk:B′′
k[A2/X]
We a e le o p o e .(Γ |Γ1,Γ2). No e ha by de ini ion o sha ing and .(A|A1, A2)
.(yi:Bi[A/X]|yi:B′
i[A1/X], yi:B′′
i[A2/X])
o (1 ≤i≤k). Thus, we ha e .(y1:B1[A/X],...,yk:Bk[A/X]|Γ1,Γ2). By ansi i i y o
sha ing we ob ain .(Γ |Γ1,Γ2)as equi ed.
Case w=λx.e:We ha e Γ0λx.e :A−→
qCand .A−→
qCA1−→
q1C1, A2−→
q2C2. By
applying Lemma 5.4 we ob ain Γ′such ha .(Γ |Γ′),.(Γ′|Γ′,Γ′),x /∈dom(Γ′)and
Γ′, x:Aqe:C.
F om .A−→
qCA1−→
q1C1, A2−→
q2C2we also ob ain .(A1|A),q≤q1,.(C|C1),.(A2|A),
q≤q2and .(C|C2).
Le Γ1= Γ2= Γ′. F om Γ1, x:Aqe:Capplying ules SUPERTYPE (wi h .(A1|A)), RELAX
(wi h q≤q1), SUBTYPE (wi h .(C|C1)) and ABS (wi h .(Γ1|Γ1,Γ1)and x /∈dom(Γ1))
we ob ain Γ10λx.e :A1−→
q1C1as equi ed. Also om Γ2, x:Aqe:Capplying ules
SUPERTYPE (wi h .(A2|A)), RELAX (wi h q≤q2), SUBTYPE (wi h .(C|C2)) and ABS (wi h
.(Γ2|Γ2,Γ2)and x /∈dom(Γ2)) we ob ain Γ20λx.e :A2−→
q2C2as equi ed.
We a e le o p o e .(Γ |Γ1,Γ2). This is equi alen o .(Γ |Γ′,Γ′)and ollows om .(Γ |Γ′)
FCUP 53
5.5. Soundness 999.
and .(Γ′|Γ′,Γ′)by he ansi i i y o sha ing.
We hus conclude he p oo o Con ex Spli ing.
5.5.6.5 Po en ial Spli ing Lemma
Lemma 5.7 (Po en ial Spli ing).I .(A|A1,...,An) hen o all besuch ha he po en ials
a e de ined, we ha e φH(be:A)≥PiφH(be:Ai).
P oo . Fi s no e ha he esul s ollow immedia ely i beis no in whn o is a λ-abs ac ion
(because po en ials a e ze o in hose cases). The po en ial is also ze o i beis a cons uc o
ha is pa o a cycle (since o he wise i would be unde ined). The emaining case is o a
cons uc o wi h no cycles, i.e. a di ec ed acyclic g aph (DAG). The p oo is hen by induc ion
on he leng h o he longes pa h. We ha e .(A|A1,...,An)and be≡c ~y. Also φH(c ~y:A)is
de ined.
I A=Tq(B) hen Ai=Tqi(Bi) o (1 ≤i≤n)and we would p oceed o p o ing
φH(c ~y:B)≥PiφH(c ~y:Bi).
O he wise, A=µX.{· · · |c:(p, ~
B)|· · · } and Ai=µX.{· · · |c:(pi,~
B′
i)|· · · } o (1 ≤i≤n).
We ha e o p o e φH(c ~y:A)≥PiφH(c ~y:Ai)o in his case he equi alen inequali y
p+X
j
φH(H(ℓj):Bj[A/X]) ≥X
i
(pi+X
j
φHH(ℓj):B′
ij[Ai/X])
By induc ion on he sho e pa hs H(ℓj), we know
X
j
φH(H(ℓj):Bj[A/X]) ≥X
iX
j
φHH(ℓj):B′
ij[Ai/X]
F om he non-nega i i y o po en ial anno a ions, all ha emains o p o e is
p≥X
i
pi
and ha ollows om .(A|A1,...,An)by he de ini ion o sha ing.
This concludes he p oo o Po en ial Spli ing.
54 FCUP
999. 5. Amo ised Analysis
5.5.6.6 Idempo en Cycles
De ini ion 5.16 (Reachabili y).The one-s ep eachabili y ela ion ℓ❀Hℓ′be ween wo loca-
ions ℓ, ℓ′in a heap Hholds i and only i H(ℓ) = c~
ℓ′′ and ℓ′∈~
ℓ′′. The many-s ep eachabili y
ela ion ❀+
His de ined as he ansi i e closu e o he one-s ep eachabili y ela ion.
No e ha eachabili y only a e ses cons uc o s, bu no une alua ed loca ions no
λ-abs ac ions. This mimics he de ini ion o po en ial (De ini ion 5.6).
The ollowing lemma shows ha , in a consis en con igu a ion, loca ions wi hin cycles can be
assigned global ypes wi h ze o po en ial. Because o he way he in a ian s we e de ined,
any cycles ha ing posi i e po en ial mus keep his po en ial wi hin he cycle in o de o
jus i y he yping o each subsequen loca ion. The e o e, since his po en ial canno a ec
he ypes o loca ions ou side he cycle, we can always se he po en ial wi hin a cycle o
ze o.
Lemma 5.17 (Idempo en Cycles).Le (H,L)be a heap con igu a ion consis en wi h global
ypes, con ex s and balance M,C,B, ha is, such ha C,B⊢MEM (H,L) : Mand .(M|Γ,C).
Then he e exis C′,M′such ha M<:M′wi h C′,B⊢MEM (H,L) : M′and .(M′|Γ,C′)such
ha o all ℓwi h ℓ❀+
Hℓwe ha e .(M′(ℓ)|M′(ℓ),M′(ℓ)) as well.
P oo . Conside a cycle consis ing o he loca ions ℓ0,...,ℓn+1 wi h ℓi❀Hℓi+1 and ℓn+1 =
ℓ0. By De ini ion 5.16 (Reachabili y) each H(ℓi)mus be a cons uc o o he o m
ci(...,ℓi+1,...). The ype consis ency o loca ions (De ini ion 5.10) o each ℓimus hold
by case LOC1, because cons uc o s a e whn s. Since hunk anno a ions a e i ele an o
LOC1, we omi hem in he ollowing o eadabili y.
Le M(ℓi) = T(Ai), hence C(ℓi)0ci(...,ℓi+1,...) : Aiby LOC1. By ou assump ion ha
ecu si e ypes a e non-in e lea ing, he ype o he posi ion o ℓi+1 wi hin he cons uc o ci
mus be he µ-bound ype a iable, i.e. Ai=µX.{ · · · |ci: (pi,...T(X)...)|· · · }. Applying
Lemma 5.3 (CONS In e sion) we ob ain
.(C(ℓi)|ℓi+1:T(Ai),...)(5.17)
FCUP 55
5.5. Soundness 999.
F om (5.17) by he de ini ion o con ex sha ing and sub yping we conclude ha he e
exis s A′
isuch ha T(A′
i)∈C↾ℓi+1 and A′
i<:Ai. By he de ini ion o global compa ibili y
(De ini ion 5.12), we ha e .M(ℓi+1)Γ↾ℓi+1 ,C↾ℓi+1 ; again by de ini ion o sub yping his
implies Ai+1 <:A′
i; combining wi h A′
i<:Aies ablished ea lie , we ob ain
Ai+1 <:A′
i<:Ai o 0≤i≤n(5.18)
Because <:is a pa ial o de (Lemma 5.14) and An+1 =A0by de ini ion, i ollows om (5.18)
ha he Ai, A′
imus all be equal. Le Abe his common ype o he cycle loca ions, i.e.
M(ℓi) = T(A) o all 0≤i≤n. The compa ibili y hypo hesis o loca ion ℓinow ins an ia es
as ollows:
.T(A)Γ↾ℓi,T(A),...(5.19)
Because each loca ion occu s a leas once in he cycle wi h exac ly he global ype T(A)
we know ha any o he e e ences in Γo Cmus occu wi h an idempo en sub ype o A,
i.e. A′such ha A <:A′and .(A′|A′, A′). We can hus se he global ype o all loca ions
in he cycle o his sel -sha ing ype A′wi hou dis up ing ype consis ency.
5.5.6.7 P oo o he Soundness Theo em
The p oo o Theo em 5.13 ollows by induc ion on he leng hs o he de i a ions o (5.6) and
(5.5) o de ed lexicog aphically, wi h he de i a ion o he e alua ion aking p io i y o e he
yping de i a ion. This is equi ed since an induc ion on he leng h o he yping de i a ion
alone would ail o he case o une alua ed loca ions, which p olongs he leng h o he
yping de i a ion by a yping judgemen o he hunk, g an ed h ough he ype consis ency
hypo hesis. On he o he hand, he leng h o he de i a ion o he e m e alua ion ne e
inc eases, bu may emain unchanged whe e he las s ep o he yping de i a ion was
ob ained by a s uc u al ule. In hese cases, he leng h o he yping de i a ion does de-
c ease, allowing an induc ion o e he lexicog aphically o de ed leng hs o bo h de i a ions.
We p oceed by case analysis o he yping ule used in p emise (5.5).
Case VAR:We ha e ℓ:Tq(A)qℓ:A om he yping hypo hesis (5.5). F om he compa i-
bili y hypo hesis (5.8) we hen ob ain .M(ℓ)Tq(A),Θ↾ℓ,C↾ℓwhich implies M(ℓ) = Tq′(b
A)
and .b
AA, ¯
A o some ypes b
A, ¯
Aand anno a ion q′wi h q≥q′.
62 FCUP
999. 5. Amo ised Analysis
and H,S,L⊢e ℓ ⇓w, H′′, espec i ely. By in e sion o ules APP and APP⇓we ob ain
Γqe:A−→
q′
C(5.41)
H,S,L⊢e⇓λx.e′,H′(5.42)
H′,S,L⊢e′[ℓ/x]⇓w, H′′ (5.43)
By p emise (5.9) we assume
m≥ +q+q′+φH(Γ, ℓ:A) + φH(Θ) + ΦL
H(C) + ΦL
H(B)
= ( +q′) + q+φH(Γ) + φH(ℓ:A, Θ) + ΦL
H(C) + ΦL
H(B)(5.44)
Inequa ion (5.44) shows ha he bound o msa is ies he equi emen s o applying induc-
ion o exp ession eusing judgemen s (5.41) and (5.42); we ob ain m′,Γ′,C′,B′,M′and m′′
1
such ha :
Γ′0λx.e′:A−→
q′
C(5.45)
H,S,Lm′′
1e⇓λx.e′,H′(5.46)
M<:M′(5.47)
C′,B′⊢MEM (H′,L) : M′(5.48)
.(M′|(Γ′, ℓ:A, Θ,C′)(5.49)
m′≥ +q′+φH′λx.e′:A−→
q′
C+φH′(ℓ:A, Θ) + ΦL
H′C′+ ΦL
H′B′(5.50)
m−m′≥m′′
1(5.51)
By Lemma 5.4 (ABS in e sion) applied o judgemen (5.45) we can assume wi hou loss
o gene ali y ha .(Γ′|Γ′,Γ′)and Γ′, x:Aq′e′:C; applying Lemma 5.2 (Subs i u ion) we
ob ain
Γ′, ℓ:Aq′e′[ℓ/x] : C(5.52)
In o de o apply he induc ion hypo hesis o e′[ℓ/x]i emains o show ha he bound (5.50)
o m′sa is ies he p emise (5.9). By .(Γ′|Γ′,Γ′)es ablished ea lie and Lemma 5.7
(Po en ial Spli ing) we know φH′(Γ′) = 0 and he e o e φH′(Γ′, ℓ:A) = φH′(ℓ:A).
FCUP 63
5.5. Soundness 999.
By De . 5.6 (Po en ial) we know φH′λx.e′:A−→
q′
C= 0; subs i u ing in (5.50) gi es us:
m′≥ +q′+φH′λx.e′:A−→
q′
C+φH′(ℓ:A, Θ) + ΦL
H′C′+ ΦL
H′B′
= +q′+φH′(ℓ:A, Θ) + ΦL
H′C′+ ΦL
H′B′
= +q′+φH′Γ′, ℓ:A+φH′(Θ) + ΦL
H′C′+ ΦL
H′B′
Hence we a e able o apply induc ion on e′[ℓ/x]and ob ain:
Γ′′ 0w:C(5.53)
H′,S,Lm′′
2e′[ℓ/x]⇓w, H′′ (5.54)
M′<:M′′ (5.55)
C′′,B′′ ⊢MEM (H′′,L) : M′′ (5.56)
.(M′′ |(Γ′′,Θ),C′′ )(5.57)
m′′ ≥ +φH′′ (w:C) + φH′′ (Θ) + ΦL
H′′ C′′+ ΦL
H′′ B′′(5.58)
m′−m′′ ≥m′′
2(5.59)
F om (5.47) and (5.55) and he ansi i i y o sub yping we conclude M<:M′′. F om (5.46)
and (5.54) and ule APP⇓Cwe ob ain H,S,Lm′′
1+m′′
2e ℓ ⇓w, H′′. F om (5.51) and (5.59)
we es ablish p oo obliga ion (5.16), i.e. m−m′′ =m+(−m′+m′)−m′′ = (m−m′)+ (m′−
m′′)≥m′′
1+m′′
2. Equa ions (5.53), (5.56), (5.57) and (5.58) es ablish he emaining p oo
obliga ions. This concludes he p oo o he APP case.
Case CONS:This case canno occu because he heo em applies only o ini ial exp es-
sions (no augmen ed exp essions).
Case CASE:The yping and e alua ion p emises a e
Γ,∆q+q′case eo {ci−→
xi-> ei}n
i=1 :C(5.60)
H,S,L⊢case eo {ci−→
xi-> ei}n
i=1 ⇓w, H′′ (5.61)
64 FCUP
999. 5. Amo ised Analysis
F om (5.61) by in e sion o ule CASE⇓we ob ain:
H,S∪
n
[
i=1
({−→
xi} ∪ BV(ei)) ,L⊢e⇓ck~
ℓ, H′(5.62)
H′,S,L⊢ek[~
ℓ/−→
xk]⇓w, H′′ (5.63)
F om (5.60) by in e sion o he yping ule CASE we ob ain:
Γqe:B(5.64)
B=µX.{c1: (p1,−→
A1)|···|cn: (pn,−→
An)}(5.65)
(
n
[
i=1
{−→
xi})∩dom(∆) = ∅(5.66)
|−→
Ak|=|−→
xk|=j(5.67)
∆, xk1:Ak1[B/X],...,xkj:Akj[B/X]q′+pkek:C(5.68)
F om (5.68), (5.66) and (5.67) oge he wi h Lemma 5.2 (subs i u ion) we ob ain
∆, ℓ1:Ak1[B/X],...,ℓj:Akj[B/X]q′+pkek[~
ℓ/−→
xk] : C(5.69)
Le mbe such ha
m≥ +q+q′+φH(Γ,∆) + φH(Θ) + ΦL
H(C) + ΦL
H(B)
= ( +q′) + q+φH(Γ) + φH(∆,Θ) + ΦL
H(C) + ΦL
H(B)(5.70)
We a e now able o apply he induc ion hypo hesis o exp ession eusing (5.64) and (5.62)
and ob ain:
Γ′0ck~
ℓ:B(5.71)
H,S∪
n
[
i=1
({−→
xi} ∪ BV(ei)) ,Lm′′
1e⇓ck~
ℓ, H′(5.72)
M<:M′(5.73)
C′,B′⊢MEM (H′,L) : M′(5.74)
.(M′|(Γ′,∆,Θ),C′)(5.75)
m′≥( +q′) + φH′(ck~
ℓ:B) + φH′(∆,Θ) + ΦL
H′C′+ ΦL
H′B′(5.76)
m−m′≥m′′
1(5.77)
FCUP 65
5.5. Soundness 999.
F om (5.71), by Lemma 5.3 (in e sion), we ha e
.(Γ′|l1:Ak1[B/X],...,lj:Akj[B/X]) (5.78)
F om (5.75) and (5.78), global compa ibili y can be elaxed o
.(M′|(l1:Ak1[B/X],...,lj:Akj[B/X],∆,Θ),C′)(5.79)
We now apply induc ion again, his ime o exp ession ek[~
ℓ/−→
xk]using (5.69), (5.63), (5.74)
and (5.79). I emains o show ha he bound (5.76) sa is ies p emise (5.9). By De . 5.6
(po en ial) and (5.65) we know φH′(ck~
ℓ:B) = pk+Pj
i=1 φH′(ℓi:Aki[B/X]); subs i u ing
in (5.76) yields:
m′≥ +q′+pk+Pj
i=1 φH′(ℓi:Aki[B/X]) + φH′(∆,Θ) + ΦL
H′(C′) + ΦL
H′(B′)
= +q′+pk+φH′∆, ℓ1:Ak1[B/X],...,ℓj:Akj[B/X]+φH′(Θ) + ΦL
H′C′+ ΦL
H′B′
Hence we can apply induc ion and ob ain:
Γ′′ 0w:C(5.80)
H′,S,Lm′′
2ek[~
ℓ/−→
xk]⇓w, H′′ (5.81)
M′<:M′′ (5.82)
C′′,B′′ ⊢MEM (H′′,L) : M′′ (5.83)
.(M′′ |(Γ′′,Θ),C′′ )(5.84)
m′′ ≥ +φH′′ (w:C) + φH′′ (Θ) + ΦL
H′′ C′′+ ΦL
H′′ B′′(5.85)
m′−m′′ ≥m′′
2(5.86)
F om (5.73) and (5.82) and he ansi i i y o sub yping we conclude M<:M′′. F om (5.72)
and (5.81) and ule CASE⇓Cwe ob ain
H,S,Lm′′
1+m′′
2case eo {ci−→
xi-> ei}n
i=1 ⇓w, H′′
F om (5.77) and (5.86) we es ablish p oo obliga ion (5.16), i.e. m−m′′ =m+(−m′+m′)−
m′′ = (m−m′)+(m′−m′′)≥m′′
1+m′′
2. Equa ions (5.80), (5.83), (5.84) and (5.85) es ablish
he emaining p oo obliga ions. This concludes he p oo o he CASE case.
66 FCUP
999. 5. Amo ised Analysis
Case WEAK:The yping p emise (5.5) eads Γ, x:Aqe:C. By in e sion o ule WEAK
we ob ain Γqe:C. In o de o apply he induc ion hypo hesis o his judgemen , we no e
ha p emise (5.7) ( ype consis ency) holds unchanged; and because .(M|Γ, x:A, Θ,C)
implies .(M|Γ,Θ,C)so does (5.8) (global compa ibili y). The bound (5.9) o he induc ion
also holds because φH(Γ, x:A)≥φH(Γ). We can he e o e apply induc ion o ewi h he
yping Γqe:Cand ob ain all equi ed esul s o his case.
Case RELAX:By he second p emise o RELAX ollows q−q′≥0and hus we can choose
′= +q−q′. We apply he induc ion hypo hesis o Γq′e:A o his ′. Since RELAX is a
s uc u al ule, all s a emen s apa om (5.5) and (5.9) emain unchanged. The induc ion
hypo hesis hus yields all equi ed conclusions e ba im, excep o (5.15). Ins ead, he
induc ion yields m′≥ ′+φH′(w:A) + φH′(Θ) + ΦL
H′(C′) + ΦL
H′(B′). Un olding ou choice o
′yields m′≥( +q−q′) + φH′(w:A) + φH′(Θ) + ΦL
H′(C′) + ΦL
H′(B′). By he second p emise
o RELAX ollows q−q′≥0and hus m′≥ +φH′(w:A) + φH′(Θ) + ΦL
H′(C′) + ΦL
H′(B′)as
equi ed o conclude his case.
Case PREPAY:The yping p emise is
Γ, ℓ:Tq′
0+q′(A)q+q′e:C
By in e sion o he ule PREPAY we ob ain
Γ, ℓ:Tq′
0(A)qe:C(5.87)
Le B′=B[ℓ7→ q′+B(ℓ)], i.e. B′is equal o Bexcep o loca ion ℓwhe e i inc eases by
q′. Assuming mas in p emise (5.9), we show ha i sa is ies he equi emen s o applying
induc ion o (5.87) wi h he modi ied B′:
m≥ +q+q′+φH(Γ, ℓ:Tq′
0+q′(A)) + φH(Θ) + ΦL
H(C) + ΦL
H(B)
≥ +q+φH(Γ, ℓ:Tq′
0(A)) + φH(Θ) + ΦL
H(C) + ΦL
HB′
The las inequali y holds because φH(ℓ:Tq′
0+q′(A)) = φH(ℓ:Tq′
0(A)) by De . 5.6 (po en ial)
and q′+ ΦL
H(B)≥ΦL
H(B′); no e ha he la e is an equali y when H(ℓ)is no a whn .
We need o ees ablish bo h global compa ibili y and ype consis ency in o de o apply
FCUP 67
5.5. Soundness 999.
he induc ion hypo hesis. Le T (A′) = M(ℓ). By he de ini ion o sha ing and global
compa ibili y (5.8) we ha e .T (A′)Tq′
0+q′(A)and hence q′
0+q′≥ . De ine k=
max( −q′,0), and M′=M[ℓ7→ Tk
(A′)].
To es ablish consis ency o M′, no e ha only he global ype o loca ion ℓchanges. Assume
ha (LOC2) applies, i.e. H(ℓ)is no in whn and ℓ /∈L, since o he wise he claim is i ial.
F om he consis ency p emise (5.7) we ha e
C(ℓ) +B(ℓ)H(ℓ) : A′(5.88)
By he de ini ion o kwe ha e k+q′= max( −q′,0)+q′≥ . Hence we can apply ule RELAX
o (5.88) and ob ain
C(ℓ)k+q′+B(ℓ)H(ℓ) : A′
By de ini ion o B′ his is equi alen o he equi ed
C(ℓ)k+B′(ℓ)H(ℓ) : A′.
To es ablish compa ibili y o M′we need o show
.Tk
(A′)Γ↾ℓ,Tq′
0(A),C↾ℓ
F om he compa ibili y p emise (5.8) we know
.T (A′)Γ↾ℓ,Tq′
0+q′(A),C↾ℓ(5.89)
Fi s we show ha .Tk
(A′)Tq′
0(A); by de ini ion o sha ing, we need o show q′
0≥k. By
de ini ion o k, we ha e q′
0≥k⇐⇒ q′
0≥max( −q′,0) ⇐⇒ q′
0≥ −q′∧q′
0≥0⇐⇒
q′
0+q′≥ ∧q′
0≥0; he la e holds by non-nega i i y assump ion, while he o me holds by
he compa ibili y p emise abo e.
Fo o he ypes Ts
(A′′)in ei he Γ↾ℓo C↾ℓ, obse e ha Tk
(A′)<:T (A′)by cons uc ion and
T (A′)<:Ts
(A′′)by he o iginal compa ibili y (5.89). By ansi i i y we ob ain he desi ed
esul .
Since he o he p emises emain unchanged, we can he e o e apply induc ion and ob ain
p ecisely he esul s equi ed o he conclusion o his case.
68 FCUP
999. 5. Amo ised Analysis
Case SHARE:The yping hypo hesis is Γ, ℓ:Aqe:C. By in e sion o ule SHARE we
ob ain Γ, ℓ:A1, ℓ:A2qe:Cand .(A|A1, A2). Assuming mas in p emise (5.9), we ob ain:
m≥ +φH(Γ, ℓ:A) + φH(Θ) + ΦL
H(C) + ΦL
H(B)
≥ +φH(Γ, ℓ:A1, ℓ:A2) + φH(Θ) + ΦL
H(C) + ΦL
H(B)
The las inequali y holds by Lemma 5.7 (Po en ial Spli ing) φH(H(ℓ):A)≥φH(H(ℓ):A1) +
φH(H(ℓ):A2). We can he e o e apply he induc ion hypo hesis o ewi h yping p emise
Γ, ℓ:A1, ℓ:A2qe:Cand ob ain as esul he equi ed conclusions o he case SHARE.
This concludes he p oo o his case.
Case SUPERTYPE:The ype ule gi es us Γ, x:Aqe:Cand A <:B. We show ha we
can apply induc ion o he p emise Γ, x:Bqe:C. Type consis ency holds unchanged
o he induc ion; by A <:Band he compa ibili y p emise (5.8) .(M|Γ, x:A, Θ,C), we
ha e .(M|Γ, x:B, Θ,C). The bound (5.9) also holds because φH(x:A)≥φH(x:B)by
A <:Band Lemma 5.9. Applying he induc ion gi es us he equi ed conclusions o he
case SUPERTYPE.
Case SUBTYPE:The ype ule gi es us Γqe:C; by in e sion we ob ain Γqe:Band
B <:C. Because he con ex is unchanged, we can apply induc ion hypo hesis di ec ly and
ob ain:
Γ′0w:B(5.90)
H,S,Lm′′ e⇓w, H′(5.91)
M<:M′(5.92)
C′,B′⊢MEM (H′,L) : M′(5.93)
.(M′|(Γ′,Θ),C′)(5.94)
m′≥ +φH′(w:B) + φH′(Θ) + ΦL
H′C′+ ΦL
H′B′(5.95)
m−m′≥m′′ (5.96)
Applying SUBTYPE o (5.90) gi es us Γ′0w:Cas equi ed o (5.10). Lemma 5.9 wi h
B <:Cgi es us φH′(w:B)≥φH′(w:C); subs i u ing in (5.95) es ablishes he bound (5.15).
Resul s (5.91), (5.92), (5.93), (5.94) and (5.96) di ec ly es ablish he emaining p oo obli-
FCUP 69
5.6. A Sys em o Eage E alua ion 999.
ga ions o his case.
5.6 A Sys em o Eage E alua ion
This sec ion emphasises he key poin s o he analysis o lazy e alua ion de eloped in his
hesis by con as o he minimal changes needed o de i e an analysis o eage e alua ion.
The comple e de ini ions and igu es o he eage sys em can be seen in Appendix A.
Fi s o all, he analysis needs a cos model o be alida ed agains . Fo ha pu pose we
de i e a cos model o eage e alua ion om Figu e 4.4 by eplacing ule LET⇓Cwi h he
ollowing:
ℓis esh Hℓ7→ be[ℓ/x],S,L∪ {ℓ}m′be[ℓ/x]⇓w′,H′
H′[ℓ7→ w′],S,Lme[ℓ/x]⇓w, H′′
H,S,L1 + m′+mle x=bein e⇓w, H′′ (EAGERLET⇓C)
The new ule EAGERLET⇓C o ces e alua ion o bebe o e e alua ing he body o he le
exp ession. No e ha he cos m′o his o ced e alua ion is immedia ely added o he
o e all cos o he le exp ession while, in a lazy se ing, an exp ession in a new loca ion
would only possibly incu a cos i i s e alua ion was needed indeed. Co espondingly, in
ule VAR⇓C he cos mis ze o since all loca ions in oduced by EAGERLET⇓Cmap o whn s
in he heap i hei e alua ion e mina es.
Al hough i is emp ing o simpli y he eage seman ics ( o example, in EAGERLET⇓we could
a oid adding o H he mapping o ℓwhen e alua ing be[ℓ/x]o we could al e ule VAR⇓ o
emo e he upda e since H′=H′[ℓ7→ w]) we mus e ain om doing so, emembe ing ha
he pu pose o p esen ing an eage sys em in his hesis is o be able o con as i wi h he
lazy sys em. The ewe he changes, he simple he con as .
Wi h espec o he ype sys em, om Figu es 5.4 and 5.5 we de i e a ype sys em sui able
o eage e alua ion by emo ing he now unneeded ule PREPAY and by eplacing ules
LET and VAR wi h
70 FCUP
999. 5. Amo ised Analysis
Γ, x:A′q′be:A∆, x:Aqe:C
x6∈ dom(Γ,∆) .(A|A, A′)q′= 0 i beis a whn
p=
p′,i be≡c ~y and A=µX.{· · · |c: (p′,~
B)|···}
0,o he wise
Γ,∆1 + q′+q+ple x=bein e:C
(EAGERLET)
and
x:A0x:A
(EAGERVAR)
espec i ely.
Since we emo ed all explici e e ences o hunk ypes om he ype sys em, we can also
de i e o he eage sys em bo h a new syn ax o allowed ypes (by emo ing he hunk
ypes om Figu e 5.1) and a new sha ing ela ion (by emo ing ule SHARETHUNK om
Figu e 5.2).
In o de o alida e he analysis o eage e alua ion agains i s espec i e cos model, we al-
e he in a ian s needed o he p oo o he soundness heo em. We s a by emo ing he
now unneeded balance B(lazy po en ial). Mo eo e , since we no longe ha e e e ences
o hunk ypes and he e is no need o accoun o exp essions ha a e simul aneously
no in whn and no unde e alua ion (se L), we can simpli y he de ini ion o po en ial
(Figu e 5.8) wi h espec o hunk ypes (also emo ing he auxilia y de ini ions o po en ial
o global con ex s Cand balance B) and u he mo e emo e case LOC2 om he de ini ion
o ype consis ency o loca ions (De ini ion 5.10).
The soundness heo em (Theo em 5.13) is es a ed acco ding o he changes in oduced
o he eage sys em in his sec ion:
Theo em 5.18 (Soundness o he Eage Sys em).I he ollowing s a emen s hold
Γqe:A(5.97)
H,S,L⊢e⇓w, H′(5.98)
C⊢MEM (H,L) : M(5.99)
.(M|(Γ,Θ),C)(5.100)
FCUP 71
5.7. Summa y 999.
hen o all ∈Q+
0and m∈Nwi h
m≥ +q+φH(Γ) + φH(Θ) (5.101)
he e exis Γ′,C′,M′and m′, m′′ ∈Nsuch ha he ollowing s a emen s also hold
Γ′0w:A(5.102)
H,S,Lm′′ e⇓w, H′(5.103)
M<:M′(5.104)
C′⊢MEM (H′,L) : M′(5.105)
.(M′|(Γ′,Θ),C′)(5.106)
m′≥ +φH′(w:A) + φH′(Θ) (5.107)
m−m′≥m′′ (5.108)
Excep o EAGERLET, he p oo o he eage sys em is omi ed since all cases a e simila
o (o simple han) he ones p esen ed in he soundness p oo o he lazy sys em (in
Sec ion 5.5.6.7). The p oo o he eage sys em can be seen in he Appendix A.2.
No e ha , apa om he expec ed changes o he ope a ional seman ics (EAGERLET⇓) and
i s co esponding ype ules (EAGERLET and EAGERVAR), he undamen al di e ence be-
ween he lazy and he eage sys ems p esen ed in his chap e is ule PREPAY, ha allows
he lazy sys em o p epay o o he wise de e he cos s o hunks. Wi hou ule PREPAY,
he eage sys em does no need hunk ypes no lazy po en ial (global balance B) and
consequen ly he e is no need o handle hose in he de ini ions o sha ing, po en ial and
ype consis ency.
5.7 Summa y
In his chap e we ha e p esen ed a ype-based amo ised analysis o o al heap alloca ions
o lazily e alua ed p og ams and p o ed ha i s s a ically de e mined bounds a e no
exceeded du ing un- ime. We ha e also emphasised he key elemen s needed in he
de elopmen o his analysis o lazy e alua ion by con as ing he lazy sys em wi h a
speci ically ailo ed eage sys em.
78 FCUP
999. 6. Expe imen al Resul s
q0has been p epaid, he cos o applying map1 o gand xs is ze o, which is also he cos
o ys. Since he ou pu o map1 has ype L0(pc, pn,T0(B)) and ys has cos ze o, he ype
o he inpu lis o map2 is T0
L0(pc, pn,T0(B)), he cos o applying map2 o and ys is
ze o and he ype o he ou pu o map2 is L0(0,0,T0(C)), he same ype as he ou pu o
p ogA. No e om he ype o map ha he ex a amoun s pcand pna e 3+q +0+0 and 1+0,
espec i ely. Now we can see whe e he cos s o he second and hi d pa s come om,
since 3+qg+q +pc= 3+qg+q +(3+q ) = 6+qg+q +q and 1+pn= 1+1 = 2. Since he cos
o map is an exac ma ch o i s ope a ional cos and no exp ession in p ogA is unaccoun ed
o , we conclude ha he cos o mula o p ogA shown abo e is accu a e.
We use a simila a gumen o demons a e ha he ype gi en o p ogB also co esponds
o i s expec ed cos . The cos o mula is now
1+q0+n(4+qg+q +q )+1
which we also di ide in h ee pa s: 1+q0,n(4+qg+q +q )and 1. The i s pa co esponds
again o a ixed cos o 1+q0, bu his ime he 1co esponds o alloca ing a heap cell o
binding h o he λ-abs ac ion (λx.le y=g x in y), while he q0is s ill p epaymen o
e alua ing xs o whn . Be o e looking a he second and hi d pa s, i is use ul o eason
abou he cos o applying unc ion h. We know unc ion halloca es a heap cell o he
binding o y o he applica ion o g o a gumen x, and e u ns applied o y. So, we know
hcos s qh= 1+qg+q o apply. Now going back o he second and hi d pa s o he cos
o mula o p ogB, since q0has been p epaid, he speci ic ype o map in p ogB is
T0
T0(T0(A)−→
qhC)−→
0T0(Lq (3+qh+q ,1,T0(A))) −→
0L0(0,0,T0(C))
and i is clea now ha he cos s o he second and hi d pa s o he cos o mula o
p ogB come om he po en ial assigned o he inpu lis o map, in pa icula he Cons nodes:
3+qh+q = 3+(1+qg+q )+q = 4+qg+q +q . Again, since he cos o map is an exac ma ch
o i s ope a ional cos and no exp ession in p ogB is unaccoun ed o , we conclude ha he
cos o mula o p ogB shown abo e is accu a e, indeed showing ha ou analysis is able o
measu e de o es a ion bene i s.
FCUP 79
6.3. In ini e Da a S uc u es: cycle 999.
6.3 In ini e Da a S uc u es: cycle
This sec ion se es o demons a e ha ou s a ic analysis can ob ain accu a e bounds
when applied o de ini ions o in ini e da a s uc u es.
Conside he ollowing p og am
le append′=λys.λxs.case xs o Nil -> ys,
Cons x xs′-> le ws′=append′ys xs′in
le ws =Cons x ws′in
ws in
le cycle =λzs.le zs′=append′zs′zs in zs′in
cycle
whe e cycle is a unc ion ha , gi en a ini e non-emp y lis as i s a gumen , gene a es
an in ini e lis by cons uc ing a copy o he inpu lis and connec ing i s end back wi h he
beginning, e ec i ely c ea ing a ci cula lis . The unc ion cycle uses he auxilia y append′,
which is de ined as he classical append, excep o ha ing i s a gumen o de e e sed.
This change is necessa y since ou sys em only allows po en ial in he inne mos a gumen
o a unc ion ( ule ABS o ou ype sys em o ces con ex Γ o be idempo en ) and hus, i
we wan he cos o applying append o be paid om he po en ial in he ecu si e a gumen ,
we mus swap he o de o a gumen s (as in his example) o use an uncu ied e sion o
he unc ion (as we will see in he nex sec ion).
In ou ype sys em we can de i e he ollowing ype o cycle:
T0
Tq0(Lin)−−−→
1+q0L′
ou
whe e Lin =Lq (2+q ,0, A)
L′
ou =L0(0,0, A′),wi h .(L′
ou |L′
ou ,L′
ou )and .(A|A, A′)
No e ha , since he ou e mos a gumen ys o append′canno ha e po en ial, he ou pu lis
o append′canno ha e po en ial as well, since o he case al e na i e o he Nil b anch,
he e u ning exp ession is ys. Howe e , gi en ha cycle ou pu s a ci cula lis and ou
sys em does no allow ci cula da a s uc u es wi h (posi i e) po en ial§, he es ic ion on
append′does no nega i ely a ec he ype o cycle, since we would no expec i s ou pu
§No e in Figu e 5.4 he use o an idempo en ype A′in he ecu si e yping o ule LET.
80 FCUP
999. 6. Expe imen al Resul s
lis L′
ou o ha e po en ial anyway.
We now show ha he bounds gi en by ou analysis a e igh . Acco ding o he ype o
cycle, we ha e he ollowing cos o mula
1+q0+n(2+q )
whe e nis he leng h o zs wi h n≥1(o he wise, cycle applied o he emp y lis would
ail o e mina e). We di ide he cos o mula in o wo pa s: a ixed pa 1+q0and a pa
ha depends on he leng h o he inpu lis n(2+q ). In he i s pa , he 1co esponds o
he heap alloca ion o he le -binding o zs′, while he q0co esponds o a p epaymen o
he cos o e alua ing zs o whn . The second pa co esponds o, o each Cons node o
xs in append′, he cos o alloca ing wo heap cells o he le -bindings o ws′and ws plus
a p epaymen o he e alua ion o xs′ o whn . No e ha ys ac s as a e e ence o a copy
o zs and can be seen as a hunk wi h ze o cos , p o ided he cos o cons uc ing a copy
o he Cons nodes o zs has been p epaid o , as in his case. Since we ha e co e ed he
cos o all he exp essions in he p og am, we conclude ha he cos o mula shown abo e
is igh , as long as q0and q a e ac ual cos s and no jus uppe bounds.
6.4 Nes ed Da a S uc u es: conca
In his sec ion we show he applicabili y o ou analysis o nes ed da a s uc u es, using a
unc ion conca . The classical lis conca ena ion unc ion is de ined as aking a lis o lis s as
i s a gumen and c ea ing a single lis by appending each o he inne lis s o he p e ious
one. He e, we de ine he ollowing al e na i e e sion o he classical lis conca ena ion,
using an auxilia y unc ion appendp:
le appendp =λp.case po Pai xs ys -> case xs o Nil -> ys,
Cons x xs′-> le p′=Pai xs′ys in
le zs′=appendp p′in
le zs =Cons x zs′in
zs in
FCUP 81
6.4. Nes ed Da a S uc u es: conca 999.
le conca =λxss.case xss o Nil -> le nil =Nil in nil,
Cons xs xss′-> le ys =conca xss′in
le p=Pai xs ys in
appendp p in
conca
We choose o de ine conca wi h appendp and no wi h he append′seen in he p e ious
sec ion. While his allows us o show ano he al e na i e e sion o append success ully
handled by ou analysis and a oids imposing unnecessa y cons ain s on he ou pu lis
(since he ou pu lis can now ha e po en ial, unlike he ou pu o append′), appendp does
ha e a highe cos due o he cons uc ion o a pai o each call o his uncu ied e sion
and his is e lec ed on he ollowing ype o conca
conca :T0
Tqo0(Lou e )−−→
qo0L inal
whe e Lou e =Lqo (2+qol +qi0,1+p′
n,Tqi0(Linne ))
Linne =Lqi (3+qi +p′
c,0, A)
L inal =L0(p′
c, p′
n, A)
qol =max(qo0, qo )
whose de i a ion uses he ollowing ype o appendp
T0
P(T0(Linne ),T0(L′
inal)) −→
0L′
inal
whe e P(A, B) = T0(µX.{Pai : (0,(A, B)) })
L′
inal =L0(p′
c,0, A)
whe e qo0and qo a e he usual cos s o a lis (as de ined in he in oduc ion o he cu en
chap e ), in his case o he ou e lis o conca , and qi0and qi a e he usual cos s applied
o he inne lis s, bu aking he maximum o such cos s o each o he inne lis s o conca ,
i.e. qi0is an uppe bound on he maximum o he cos s o e alua ing o whn each o he
inne lis s (xs) and qi is an uppe bound on he maximum o he cos s o e alua ing o whn
each o he ails o he Cons nodes o he inne lis s (xs′).
Assuming, o simplici y, ha we a e no in e es ed in he po en ial o he ou pu lis (p′
c= 0),
82 FCUP
999. 6. Expe imen al Resul s
he cos o mula ex ac ed om he ype o appendp is
l(3+qi )
whe e lis he leng h o he i s lis o he inpu . We s a by explaining how he cos
o mula ela es o he de ini ion o appendp. Fi s no e ha he ype assigned by ou analysis
assumes ha he i s lis o he inpu pai cos s ze o o e alua e o a whn (o assumes ha
his cos has been p epaid). Now, looking a he p og am de ini ion, he cos o he case
exp ession o he pai is equal o he cos o he case exp ession o he lis xs, since p, om
i s ype, cos s no hing o e alua e o whn . We can also see in he ype ha xs and ys cos
ze o o e alua e o whn , and hus, he cos o he case exp ession o he lis is equal o he
cos o he Cons case al e na i e, which in u n, o each Cons node o xs, co esponds o
a cos o 3 o he h ee heap cells s o ing he hunks e e enced by p′,zs′and zs, plus he
cos o p epaying qi o xs′since appendp expec s a pai o lis s ha cos ze o o e alua e
o whn (o ha e hose cos s p epaid, as in his case). No e ha applying appendp o p′
has no ex a cos and ha no only zs is in whn , bu also e alua ing each o i s Cons nodes
also has no ex a cos , acco ding o he ype L′
inal o he applica ion appendp p′. We ha e
hus ela ed each exp ession in he de ini ion o appendp o he cos o mula exp essed by
i s ype.
We now do he same wi h espec o conca . Acco ding o i s ype, and igno ing, o
simplici y, p′
cand p′
n, we ha e he ollowing cos o mula
qo0+1+n(2+qol +qi0)+m(3+qi )
whe e nis he leng h o ou e lis passed as inpu o conca and mis he sum o he
leng hs o he inne lis s (m=l1,...,ln). Connec ing he cos o mula o he de ini ion
o conca , we can see ha , once applied o a lis o lis s xss,conca e alua es he case
disc iminan (cos ing qo0). When conca eaches he end o he ou e lis , i cos s 1 o he
heap cell alloca ed by he le -binding o nil. Meanwhile, we ha e o conside he cos
o each Cons node o he ou e lis , and i use ul o conside i s pa on he cos o mula
n(2+qol +qi0)+m(3+qi )as
n
X
i=1
(2+qol +qi0+li(3+qi ))
So, o each inne lis o he inpu o conca , i cos s 2heap cells o c ea e he wo le -
bindings o ys and p. We also ha e o pay qol, as he wo s case be ween he cos qo o
FCUP 83
6.5. Known Limi a ion wi h Co-Recu si e De ini ions: ibs 999.
e alua ing xss′ o whn and he cos qo0 ha he ype o conca expec s o i s inpu lis .
Fu he mo e, we p epay he cos qi0o xs, since he ype o appendp expec s a lis wi h
no cos , and pay he cos li(3+qi )o applying appendp o p. Thus, we ha e ela ed each
exp ession in he de ini ion o conca o he cos o mula exp essed by i s ype.
No e ha mis he sum o he leng hs o he inne lis s, aking each leng h sepa a ely
in o accoun , and hus i does no in oduce a sou ce o elaxa ion on he cos , unlike, o
example, i we had conside ed m as n×max(l1,...,ln). The cos o mula o conca is an
exac ma ch o i s ope a ional cos , p o ided qo0,qo ,qi0,qi and qol a e exac alues and no
jus uppe bounds, and he e o e he quali y o he bounds is he bes we could hope o ¶.
6.5 Known Limi a ion wi h Co-Recu si e De ini ions: ibs
Non-s ic unc ional languages allow he use o an idiom ha consis s o concisely de ining
an in ini e lis whe e, o he han a ini e numbe o ini ial elemen s, each elemen depends
on p e ious ones. The classical de ini ion o he Fibonacci se ies is an example o such
idiom and is w i en in Haskell as
ibs = 0 : 1 : zipWi h (+) ibs ( ail ibs)
Un o una ely, al hough ibs has a linea cos wi h espec o he numbe o elemen s
needed om his in ini e lis , ou analysis canno cap u e ha ac and canno ind a solu ion
o his example. In ac , we ha e ound ha ou analysis canno handle such examples and
we discuss he di icul ies in he emainde o his sec ion.
In o de o isola e he p oblem, we highligh he di icul ies wi h wha we belie e o be one
o he simples examples o his idiom, concisely w i en in Haskell as
bools =T ue :map no bools
¶No e ha , by de ini ion, qo ,qi and qol a e likely o be a sou ce o elaxa ion o he cos . Howe e , his loss
o p ecision is expec ed o any s a ic analysis, since i esul s om he need o c ea e a single abs ac ion o
ep esen an in ini y o conc e e da a.
84 FCUP
999. 6. Expe imen al Resul s
and ansla ed in o ou Fun language as
le ue =T ue in
le alse =False in
le no =λb.case bo T ue -> alse,False -> ue in
le map =λ .λxs.case xs o Nil -> le nil =Nil in nil,
Cons x xs′-> le y= x in
le ys′=map xs′in
le ys =Cons y ys′in ys in
le bools =le bls′=map no bools in
le bls =Cons ue bls′in
bls in
bools
The bools example de ines an in ini e lis o al e na ing booleans (a bi a ily s a ing wi h
T ue) whe e each elemen , o he han he i s , is de ined as he nega ion o he p eceeding
elemen .
We s a by obse ing ha bools yields a cons an cos o each successi e elemen (and
hus has a linea cos wi h espec o i s leng h). E alua ing bools o a whn , in o de o
access i s i s elemen , cos s 2, co esponding o he alloca ion o wo heap cells ha hold
he hunk map no bools and he whn Cons ue bls′. Each subsequen elemen cos s 3
heap alloca ions, co esponding o he h ee le s in he Cons b anch o unc ion map. Gi en
his easoning, we would like o ob ain a yping such as bools :T2
L3(0,0,T0(Bool)),
whe e Bool de
=µX.{T ue : (0,()) | False : (0,()) }.
Recall he ype o map, o inpu lis s wi hou po en ial, as shown in Sec ion 6.1:
T0
T0(A′−→
q B)−→
0Tql(L′
in)−−−−−−−−−−−−−−→
3+q +ql+max(p′
c, p′
n−2) Lou
whe e L′
in =Lql(0,0, A′),wi h .(A′|A′, A′)
Lou =L3+q +ql
+p′
c(p′
c, p′
n,T0(B))
Applying o his conc e e example: A′=T0(Bool),q = 0 (since applying no o a boolean
has ze o cos ), B=Bool and, o simplici y, assuming we a e no in e es ed in ha ing
FCUP 85
6.5. Known Limi a ion wi h Co-Recu si e De ini ions: ibs 999.
po en ial in he ou pu lis , p′
c= 0 and p′
n= 0. We hus ha e
T0
T0(T0(Bool)−→
0Bool)−→
0Tql(L′
in)−−−→
3+qlLou
whe e L′
in =Lql(0,0,T0(Bool))
Lou =L3+ql(0,0,T0(Bool))
Since in bools he ou pu lis o map is passed back again as he inpu lis , he ypes Lou
and L′
in mus ma ch, bu hen ou analysis ails o p oduce a ype o bools due o he
impossibili y o inding a ini e solu ion o ql= 3+ql( he cos s in L′
in and Lou ).
Howe e , he eal p oblem wi h his co- ecu si e de ini ion is ha , because o lazy e al-
ua ion, he cos o he ecu si e call o map (3 + ql) is sha ed wi h he cos o ob aining
each elemen o he ou pu lis (also 3+ ql). Un o una ely, he ules o ou ype sys em
(including PREPAY) a e no enough o ack he ci cula sha ing dependencies which would
allow lowe ing he cos s o hunk ypes. The e o e, we conclude ha ou analysis canno
handle such examples o co- ecu si e unc ions.
I is impo an o no e ha bools can be ew i en in a way o which ou analysis ob ains
accu a e esul s. Fo example, in he ansla ion o ou Fun language o he ollowing Haskell
code
bools =i e no T ue
whe e i e x =x:i e ( x)
bools has ype
T3+pc
L3+pc(pc, pn,T0(Bool))
whe e any po en ial in he Cons nodes pcmus be paid o om he cos s o e alua ing bools,
and subsequen ails, o i s whn , while he po en ial in he Nil node pnhas no es ic ion
since bools ne e c ea es such node. We could do be e and ew i e bools as a ci cula
de ini ion ha ing cons an o e all cos , such as
le ue =T ue in
le alse =False in
le bools =le bls′=Cons alse bools in
le bls =Cons ue bls′in
bls in
bools
86 FCUP
999. 6. Expe imen al Resul s
(in Haskell i could be w i en as bools =T ue :False :bools), which has ype
T2
L0(0,0,T0(Bool))
and hus, al hough he e we could no ha e po en ial in bools i we wan ed ok, his e sion
has be e cos .
While we belie e he emaining examples wi h linea cos o his idiom can also be ew i en
in a way ou analysis can handle, such e o mula ions migh no eel na u al o some
examples. We would like o a oid o cing p og amme s ou o his s yle when using ou
analysis and we will pu sue a solu ion o his p oblem as u he wo k.
6.6 Summa y
In his chap e we ha e shown how ou analysis p o ides accu a e cos bounds o unc ions
such as map,cycle and conca , hus co e ing examples o highe -o de unc ions and he
use o in ini e and nes ed da a s uc u es. We ha e also seen how ou analysis can hin in o
which al e na i e p og am de ini ion has be e ope a ional cos .
Remembe hough, ha all s a ic analyses a e doomed o ail o some p og ams and we
did show some examples ha in pa icula ou analysis inds p oblema ic. Some limi a ions
such as ha o append ha e simple wo ka ounds by swapping he o de o a gumen s
o using an uncu ied e sion, bu each has i s d awbacks: es ic ed ou pu po en ial o
inc eased cos o uncu ying he inpu . O he limi a ions a e le as u he wo k, such as he
one ound on he co- ecu si e de ini ions o he p e ious sec ion and he one ha es ic s
ou analysis o p og ams wi h linea cos s wi h espec o he numbe o cons uc o s in da a
s uc u es.
kCi cula da a s uc u es in ou sys em canno ha e po en ial o he han ze o. This is simila o he es ic ion
ound in he ou pu o unc ion cycle in Sec ion 6.3.
7. Conclusion
In his chap e we summa ise he wo k desc ibed in his hesis and no e he limi a ions o
ou app oach oge he wi h a discussion o u he wo k.
7.1 Assessmen o Achie emen s
Analyses o lazily e alua ed p og ams we e es ic ed o i s -o de p og ams o we e no
au oma ic o depended on con ex in o ma ion cu en ly imp ac ical o ob ain o made he
ela ion be ween cos s and inpu s mo e opaque by no exp essing da a-dependencies in
he bounds.
This hesis has in oduced he i s au oma ic s a ic analysis o accu a ely de e mining
bounds on he execu ion cos s o lazy unc ional p og ams. The analysis uses an amo ised
analysis echnique ha is capable o di ec ly analysing highe -o de lazy p og ams, wi hou
equi ing de unc ionalisa ion o o he non-cos -p ese ing p og am ans o ma ions. Ou
analysis deals wi h use -de ined (po en ially in ini e) da a s uc u es and da a-dependencies
a e exp essed in he p oduced bounds. We ha e p esen ed a soundness p oo , alida ing
he analysis agains an ope a ional seman ics de i ed om Launchbu y’s na u al seman ics
o g aph educ ion, and analysed in de ail some non- i ial examples o lazy e alua ion
using he ules o ou sys em, while p o iding a URL o a web-p o o ype implemen a ion o
he analysis whe e mo e examples can be ound and use s can y hei own. F om ou
no el analysis o lazy e alua ion we ha e de i ed wi h minimal changes an analysis o
eage e alua ion, clea ly highligh ing he key elemen o ou esul : a ype ule (PREPAY)
ha allows cos s o be de e ed.
87
94 FCUP
999. BIBLIOGRAPHY
[BFGY08] V´
ıc o B abe man, Fede ico Fe n´
andez, Diego Ga be e sky, and Se gio
Yo ine. Pa ame ic P edic ion o Heap Memo y Requi emen s. In P oceedings
o he In e na ional Symposium on Memo y Managemen (ISMM’08), pages
141–150, Tucson, A izona, USA, June 2008. ACM. 2.4
[BH89] B o Bje ne and S¨
o en Holms ¨
om. A composi ional app oach o ime analysis
o i s o de lazy unc ional p og ams. In P oceedings o he ACM SIGPLAN
Con e ence on Func ional P og amming Languages and Compu e A chi ec u e
(FPCA’89), London, UK, Sep embe 1989. 2.2
[BHA86] Geo ey L. Bu n, Ch is Hankin, and Samson Ab amsky. S ic ness analysis o
highe -o de unc ions. Science o Compu e P og amming, 7:249–278, 1986.
2.1
[BR00] Adam Bakewell and Colin Runciman. A Model o Compa ing he Space Usage
o Lazy E alua o s. In P oceedings o he 2nd In e na ional ACM SIGPLAN
Con e ence on P inciples and P ac ice o Decla a i e P og amming (PPDP’00),
pages 151–162, Mon eal, Quebec, Canada, Sep embe 2000. 2.1
[BR01] Adam Bakewell and Colin Runciman. A Space Seman ics o Co e Haskell. In
G aham Hu on, edi o , ACM SIGPLAN Haskell Wo kshop 2000, olume 41 o
Elec onic No es in Theo e ical Compu e Science. Else ie , 2001. 2.1
[Cam08] B ian Campbell. Type-based amo ized s ack memo y p edic ion. PhD
hesis, Labo a o y o Founda ions o Compu e Science, School o In o ma ics,
Uni e si y o Edinbu gh, UK, 2008. 2.3, 7.2, 7.3
[Cam09] B ian Campbell. Amo ised Memo y Analysis Using he Dep h o Da a S uc-
u es. In Giuseppe Cas agna, edi o , P oceedings o he Eu opean Symposium
on P og amming (ESOP’09), Yo k, UK, Ma ch, 2009, olume 5502 o Lec u e
No es in Compu e Science, pages 190–204. Sp inge , 2009. 2.3, 3.2
[CNPQ08] Wei-Ngan Chin, Huu Hai Nguyen, Co neliu Popeea, and Shengchao Qin.
Analysing Memo y Resou ce Bounds o Low-Le el P og ams. In P oceedings
o he In e na ional Symposium on Memo y Managemen (ISMM’08), pages
151–160, Tucson, A izona, USA, June 2008. ACM. 2.4
[CW00] Ka l C a y and S ephanie Wei ich. Resou ce Bound Ce i ica ion. In P oceed-
ings o he ACM SIGPLAN-SIGACT Symposium on P inciples o P og amming
FCUP 95
BIBLIOGRAPHY 999.
Languages (POPL’00), pages 184–198, Bos on, Massachuse s, USA, Janua y
2000. 2.3
[Dan08] Nils Ande s Danielsson. Ligh weigh Semi o mal Time Complexi y Analysis o
Pu ely Func ional Da a S uc u es. In P oceedings o he ACM SIGPLAN-
SIGACT Symposium on P inciples o P og amming Languages (POPL’08),
pages 133–144, San F ancisco, Cali o nia, USA, Janua y 2008. 2.2
[DM82] Lu´
ıs Damas and Robin Milne . P incipal ype-schemes o unc ional p og ams.
In P oceedings o he ACM Symposium on P inciples o P og amming Lan-
guages (POPL’82), pages 207–212, Albuque que, New Mexico, USA, Janua y
1982. 1, 3.2.1
[DMMZ12] Oli ie Dan y, Ke in Millikin, Johan Munk, and Ian Ze ny. On In e -de i ing
Small-s ep and Big-s ep Seman ics: A Case S udy o S o eless Call-by-need
E alua ion. Theo e ical Compu e Science, 435(0):21–42, 2012. 7.3
[Enn03] Robe Ennals. Adap i e E alua ion o Non-S ic P og ams. PhD hesis, King’s
College, Uni e si y o Camb idge, Decembe 2003. 2.1
[EP02] Albe o de la Encina and Rica do Pe˜
na. P o ing he Co ec ness o he STG
Machine. In Thomas A s and Ma kus Mohnen, edi o s, Selec ed pape s
o he In e na ional Wo kshop on Implemen a ion o Func ional Languages
(IFL’01), S ockholm, Sweden, Sep embe , 2001, olume 2312 o Lec u e No es
in Compu e Science, pages 88–104. Sp inge , 2002. 2.1, 4, 4.2, †, 4.2, 4.2
[EP03a] Albe o de la Encina and Rica do Pe˜
na. Fo mally De i ing an STG Machine. In
P oceedings o he 5 h In e na ional ACM SIGPLAN Con e ence on P inciples
and P ac ice o Decla a i e P og amming (PPDP’03), pages 102–112, Uppsala,
Sweden, Augus 2003. ACM. 2.1, 4
[EP03b] Robe Ennals and Simon Pey on Jones. Op imis ic E alua ion: an adap i e
e alua ion s a egy o non-s ic p og ams. In P oceedings o he ACM
SIGPLAN In e na ional Con e ence on Func ional P og amming (ICFP’03),
pages 287–298, Uppsala, Sweden, Augus 2003. 2.1
[EP09] Albe o de la Encina and Rica do Pe˜
na. F om Na u al Seman ics o C: a Fo mal
De i a ion o wo STG Machines. Jou nal o Func ional P og amming, 19(1):47–
94, 2009. 2.1, 4.1
96 FCUP
999. BIBLIOGRAPHY
[Fax00] Ka l-Filip Fax´
en. Cheap eage ness: Specula i e e alua ion in a lazy unc ional
language. In P oceedings o he ACM SIGPLAN In e na ional Con e ence
on Func ional P og amming (ICFP’00), pages 150–161, Mon eal, Canada,
Sep embe 2000. 2.1
[GS99] J¨
o gen Gus a sson and Da id Sands. A Founda ion o Space-Sa e T ans o -
ma ions o Call-by-Need P og ams. In And ew D. Go don and And ew M. Pi s,
edi o s, Thi d In e na ional Wo kshop on Highe O de Ope a ional Techniques
in Seman ics, olume 26 o Elec onic No es in Theo e ical Compu e Science.
Else ie , 1999. 2.1
[HAH11] Jan Ho mann, Klaus Aehlig, and Ma in Ho mann. Mul i a ia e Amo ized
Resou ce Analysis. In P oceedings o he ACM SIGPLAN-SIGACT Symposium
on P inciples o P og amming Languages (POPL’11), pages 357–370, Aus in,
Texas, USA, Janua y 2011. 1, 2.3, 3.2, 3.2.1, 5.1, 7.2, 7.3
[HBH+07] Ch is oph A. He mann, A melle Bonen an , Ke in Hammond, S e en Jos ,
Hans-Wol gang Loidl, and Robe Poin on. Au oma ic amo ised wo s -case
execu ion ime analysis. In P oceedings o he 7 h In e na ional Wo kshop on
Wo s -Case Execu ion Time (WCET) Analysis, pages 13–18, Pisa, I aly, July
2007. 2.3
[HH10] Jan Ho mann and Ma in Ho mann. Amo ized Resou ce Analysis wi h
Polynomial Po en ial. In Giuseppe Cas agna, edi o , P oceedings o he
Eu opean Symposium on P og amming (ESOP’10), Paphos, Cyp us, Ma ch,
2010, olume 6012 o Lec u e No es in Compu e Science, pages 287–306.
Sp inge , 2010. 2.3, 3.2, 3.2.1
[HJ03] Ma in Ho mann and S e en Jos . S a ic P edic ion o Heap Space Usage
o Fi s -O de Func ional P og ams. In P oceedings o he ACM SIGPLAN-
SIGACT Symposium on P inciples o P og amming Languages (POPL’03),
pages 185–197, New O leans, Louisiana, USA, Janua y 2003. 1, 2.3, 3.2,
7.2, 7.3
[HJ06] Ma in Ho mann and S e en Jos . Type-Based Amo ised Heap-Space Anal-
ysis. In Pe e Ses o , edi o , P oceedings o he Eu opean Symposium
on P og amming (ESOP’06), Vienna, Aus ia, Ma ch, 2006, olume 3924 o
Lec u e No es in Compu e Science, pages 22–37. Sp inge , 2006. 2.3, 7.3
FCUP 97
BIBLIOGRAPHY 999.
[Ho 11] Jan Ho mann. Types wi h Po en ial: Polynomial Resou ce Bounds ia
Au oma ic Amo ized Analysis. PhD hesis, LMU Munich, Ge many, 2011. 7.2
[Hop08] Ca he ine Hope. A Func ional Seman ics o Space and Time. PhD hesis,
Uni e si y o No ingham, UK, 2008. 2.2
[HR09] Ma in Ho mann and Dulma Rod iguez. E icien Type-Checking o Amo ised
Heap-Space Analysis. In P oceedings o he CSL: Annual Con e ence o
he Eu opean Associa ion o Compu e Science Logic, Coimb a, Po ugal,
Sep embe , 2009, olume 5771 o Lec u e No es in Compu e Science, pages
317–331. Sp inge , 2009. 2.3
[Hug89] John Hughes. Why Func ional P og amming Ma e s. The Compu e Jou nal,
32(2):98–107, 1989. 1
[JLH+09] S e en Jos , Hans-Wol gang Loidl, Ke in Hammond, No man Scai e, and
Ma in Ho mann. “Ca bon C edi s” o Resou ce-Bounded Compu a ions Using
Amo ised Analysis. In Ana Ca alcan i and Dennis R. Dams, edi o s, FM 2009:
Fo mal Me hods, Eindho en, The Ne he lands, No embe , 2009, olume 5850
o Lec u e No es in Compu e Science, pages 354–369. Sp inge , 2009. 1, 2.3,
3.2, 4.3, 7.1, 7.2, 7.3
[JLHH10] S e en Jos , Hans-Wol gang Loidl, Ke in Hammond, and Ma in Ho mann.
S a ic De e mina ion o Quan i a i e Resou ce Usage o Highe -O de P o-
g ams. In P oceedings o he ACM SIGPLAN-SIGACT Symposium on P in-
ciples o P og amming Languages (POPL’10), pages 223–236, Mad id, Spain,
Janua y 2010. 1, 2.3, 3.2, 5.1, 5.5.5, 6.2, 7.1, 7.2, 7.2, 7.3
[Jon92] Simon Pey on Jones. Implemen ing Lazy Func ional Languages on S ock Ha d-
wa e: The Spineless Tagless G-Machine. Jou nal o Func ional P og amming,
2(2):127–202, 1992. 4
[Jos89] Ma k B. Josephs. The seman ics o lazy unc ional languages. Theo e ical
Compu e Science, 68(1):105–111, 1989. 2.1
[Jos10] S e en Jos . Au oma ed Amo ised Analysis. PhD hesis, Facul y o Ma hema -
ics, Compu e Science and S a is ics, LMU Munich, Ge many, 2010. 2.3, 5.5.5,
7.1, 7.2, 7.2, 7.3
98 FCUP
999. BIBLIOGRAPHY
[KCL+10] Gab iele Kelle , Manuel M.T. Chak a a y, Roman Leshchinskiy, Simon Pey-
on Jones, and Ben Lippmeie . Regula , shape-polymo phic, pa allel a ays
in haskell. In P oceedings o he ACM SIGPLAN In e na ional Con e ence
on Func ional P og amming (ICFP’10), pages 261–272, Bal imo e, Ma yland,
USA, Sep embe 2010. 7.3
[Lau93] John Launchbu y. A Na u al Seman ics o Lazy E alua ion. In P oceedings
o he ACM SIGPLAN-SIGACT Symposium on P inciples o P og amming
Languages (POPL’93), pages 144–154, Cha les on, Sou h Ca olina, USA,
Janua y 1993. 1, 1.1, 2.1, 4, 4.1, 4.2, 4.2
[LJ09] Hans-Wol gang Loidl and S e en Jos . Imp o emen s o a Resou ce Analysis
o Hume. In P oceedings o he 1s In e na ional Wo kshop on Founda ional
and P ac ical Aspec s o Resou ce Analysis (FOPARA), Eindho en, The Ne he -
lands, No embe 2009. Sp inge . 3.2.1
[Ma 98] Ralph Ma hes. Ex ensions o Sys em F by I e a ion and P imi i e Recu sion on
Mono one Induc ion Types. PhD hesis, LMU Munich, Ge many, 1998. 5.1, 7.2
[Mil78] Robin Milne . A heo y o ype polymo phism in p og amming. Jou nal o
Compu e and Sys em Sciences, 17:348–375, 1978. 1, 3.2.1
[MML+10] Simon Ma low, Pa ick Maie , Hans-Wol gang Loidl, Mus a a K. Aswad, and Phil
T inde . Seq no mo e: Be e s a egies o pa allel haskell. In P oceedings
o he hi d ACM SIGPLAN Haskell Symposium, pages 91–102, Bal imo e,
Ma yland, USA, 2010. ACM. 7.3
[MN92] Alan Myc o and A hu No man. Op imising compila ion — lazy unc ional
languages. In P oceedings o he 19 h So wa e Semina (SOFSEM),ˇ
Zdia ,
Czechoslo akia, 1992. 2.1
[MNPJ11] Simon Ma low, Ryan New on, and Simon Pey on Jones. A monad o
de e minis ic pa allelism. In P oceedings o he ou h ACM SIGPLAN Haskell
Symposium, pages 71–82, Tokyo, Japan, 2011. ACM. 7.3
[Mou98] Jon Moun joy. The Spineless Tagless G-machine, na u ally. In P oceedings
o he ACM SIGPLAN In e na ional Con e ence on Func ional P og amming
(ICFP’98), pages 163–173, Bal imo e, Ma yland, USA, Sep embe 1998. 2.1
FCUP 99
BIBLIOGRAPHY 999.
[MOW98] John Ma ais , Ma in Ode sky, and Philip Wadle . The Call-by-Need Lambda
Calculus. Jou nal o Func ional P og amming, 8:275–317, May 1998. 2.1
[MS99] And ew Mo an and Da id Sands. Imp o emen in a Lazy Con ex : An
Ope a ional Theo y o Call-by-Need. In P oceedings o he ACM SIGPLAN-
SIGACT Symposium on P inciples o P og amming Languages (POPL’99),
pages 43–56, San An onio, Texas, USA, Janua y 1999. 2.1
[MT91] Robin Milne and Mads To e. Co-induc ion in ela ional seman ics. Theo e ical
Compu e Science, 87(1):209–220, 1991. 5.5.5
[Myc80] Alan Myc o . The heo y and p ac ice o ans o ming call-by-need in o call-by-
alue. In P oceedings o he In e na ional Symposium on P og amming, Pa is,
F ance, Ap il, 1980, olume 83 o Lec u e No es in Compu e Science, pages
269–281. Sp inge , 1980. 2.1
[Myc81] Alan Myc o . Abs ac in e p e a ion and op imising ans o ma ions o applica-
i e p og ams. PhD hesis, Depa men o Compu e Science, Uni e si y o
Edinbu gh, UK, 1981. 2.1
[Oka98] Ch is Okasaki. Pu ely Func ional Da a S uc u es. Camb idge Uni e si y P ess,
1998. 2.3, 3.2
[PAB+99] Simon Pey on Jones (edi o ), Lenna Augus sson, B ian Bou el, F. Wa en
Bu on, Joseph H. Fasel, And ew D. Go don, Ke in Hammond, John Hughes,
Paul Hudak, Thomas Johnsson, Ma k P. Jones, John C. Pe e son, Alas ai
Reid, and Philip Wadle . Repo on he Non-S ic Func ional Language, Haskell
(Haskell98). Technical epo , Yale Uni e si y, 1999. 1
[PB10] Maciej Pi og and Da iusz Bie nacki. A Sys ema ic De i a ion o he STG
Machine Ve i ied in Coq. In P oceedings o he hi d ACM SIGPLAN Haskell
Symposium, pages 25–36, Bal imo e, Ma yland, USA, 2010. ACM. 2.1, 4
[Rey72] John C. Reynolds. De ini ional In e p e e s o Highe -O de P og amming
Languages. In P oceedings o he ACM Na ional Con e ence, pages 717–740.
ACM, Augus 1972. 2.2
[San90a] Da id Sands. Calculi o Time Analysis o Func ional P og ams. PhD hesis,
Impe ial College, Uni e si y o London, Sep embe 1990. 2.2
100 FCUP
999. BIBLIOGRAPHY
[San90b] Da id Sands. Complexi y Analysis o a Lazy Highe -O de Language. In
Neil Jones, edi o , P oceedings o he Eu opean Symposium on P og amming
(ESOP’90), Copenhagen, Denma k, May, 1990, olume 432 o Lec u e No es
in Compu e Science, pages 361–376. Sp inge , 1990. 2.2
[San98] Da id Sands. Compu ing wi h con ex s: A simple app oach. In And ew D.
Go don, And ew M. Pi s, and Ca olyn L. Talco , edi o s, Second Wo kshop
on Highe -O de Ope a ional Techniques in Seman ics, olume 10 o Elec onic
No es in Theo e ical Compu e Science. Else ie , 1998. 2.2
[Ses97] Pe e Ses o . De i ing a Lazy Abs ac Machine. Jou nal o Func ional
P og amming, 7(3):231–264, 1997. 2.1, 4, 4.1, 4.2, ∗, 4.2
[SHFV07] Hugo R. Sim˜
oes, Ke in Hammond, M´
a io Flo ido, and Ped o Vasconcelos.
Using In e sec ion Types o Cos -Analysis o Highe -O de Polymo phic Func-
ional P og ams. In Tho s en Al enki ch and Cono McB ide, edi o s, Re ised
Selec ed Pape s o he In e na ional Wo kshop on Types o P oo s and
P og ams (TYPES’06), No ingham, UK, Ap il, 2006, olume 4502 o Lec u e
No es in Compu e Science, pages 221–236. Sp inge , 2007. 1, 1.1
[SVF+12] Hugo Sim˜
oes, Ped o Vasconcelos, M´
a io Flo ido, S e en Jos , and Ke in
Hammond. Au oma ic Amo ised Analysis o Dynamic Memo y Alloca ion o
Lazy Func ional P og ams. In P oceedings o he ACM SIGPLAN In e na ional
Con e ence on Func ional P og amming (ICFP’12), pages 165–176, Copen-
hagen, Denma k, Sep embe 2012. 1.1, 2.3, 5.3, 7.3
[S 07] Olha Shka a ska, Ron an Kes e en, and Ma ko an Eekelen. Polynomial
Size Analysis o Fi s -O de Func ions. In P oceedings o he 8 h In e na ional
Con e ence on Typed Lambda Calculi and Applica ions (TLCA’07), Pa is,
F ance, June, 2007, olume 4583 o Lec u e No es in Compu e Science, pages
351–365. Sp inge , 2007. 2.3
[Ta 85] Robe E. Ta jan. Amo ized compu a ional complexi y. SIAM Jou nal on
Algeb aic and Disc e e Me hods, 6(2):306–318, Ap il 1985. 2.3, 3.1, ∗, 3.2
[THLPJ98] Phil W. T inde , Ke in Hammond, Hans-Wol gang Loidl, and Simon Pey-
on Jones. Algo i hm + s a egy = pa allelism. Jou nal o Func ional P og am-
ming, 8(1):23–60, 1998. 7.3
FCUP 101
BIBLIOGRAPHY 999.
[Vas08] Ped o Bal aza Vasconcelos. Space cos analysis using sized ypes. PhD
hesis, School o Compu e Science, Uni e si y o S And ews, No embe 2008.
1
[VH05] Ped o B. Vasconcelos and Ke in Hammond. In e ing Cos Equa ions o
Recu si e, Polymo phic and Highe -O de Func ional P og ams. In Phil T inde ,
G eg J. Michaelson, and Rica do Pe˜
na, edi o s, Re ised Pape s o he
In e na ional Wo kshop on Implemen a ion o Func ional Languages (IFL’03),
Edinbu gh, UK, Sep embe , 2003, olume 3145 o Lec u e No es in Compu e
Science, pages 88–101. Sp inge , 2005. 1
[Wad88] Philip Wadle . S ic ness Analysis aids Time Analysis. In P oceedings o he
ACM Symposium on P inciples o P og amming Languages (POPL’88), pages
119–132, San Diego, Cali o nia, USA, Janua y 1988. 2.2
[Wad92] Philip Wadle . The Essence o Func ional P og amming. In P oceedings o he
ACM SIGPLAN-SIGACT Symposium on P inciples o P og amming Languages
(POPL’92), pages 1–14, Albuque que, New Mexico, USA, Janua y 1992. 2.2
[WH87] Philip Wadle and John Hughes. P ojec ions o S ic ness Analysis. In
P oceedings o he ACM SIGPLAN Con e ence on Func ional P og amming
Languages and Compu e A chi ec u e (FPCA’87), Po land, O egon, USA,
Sep embe 1987. 2.1, 2.2
102 FCUP
999. BIBLIOGRAPHY
A. A Sys em o Eage E alua ion
A.1 De ini ions and Figu es
wis in whn
H,S,Lw⇓w, H(WHNF⇓)
ℓ6∈ L H,S,L∪ {ℓ}H(ℓ)⇓w, H′
H,S,Lℓ⇓w, H′[ℓ7→ w](VAR⇓)
H,S,Le⇓λx. e′,H′H′,S,Le′[ℓ/x]⇓w, H′′
H,S,Le ℓ ⇓w, H′′ (APP⇓)
ℓis esh Hℓ7→ be[ℓ/x],S,L∪ {ℓ}be[ℓ/x]⇓w′,H′
H′[ℓ7→ w′],S,Le[ℓ/x]⇓w, H′′
H,S,Lle x=bein e⇓w, H′′ (EAGERLET⇓C)
H,S∪Sn
i=1 ({−→
xi} ∪ BV(ei)) ,Le⇓ck~
ℓ, H′
H′,S,Lek[~
ℓ/−→
xk]⇓w, H′′
H,S,Lcase eo {ci−→
xi-> ei}n
i=1 ⇓w, H′′ (CASE⇓)
Figu e A.1: Eage ope a ional seman ics
103
110 FCUP
999. A. A Sys em o Eage E alua ion
I be[ℓ/x]is in whn :E alua ion (A.5) e mina es immedia ely by WHNF⇓and we ha e
w′=be[ℓ/x]and H1=H′=H2. We use ule WEAK⇓C o ob ain
H1,S,L10be[ℓ/x]⇓w′,H′(A.21)
We in end o apply he induc ion hypo hesis o e he e m e[ℓ/x], so we mus es ablish he
equi ed p emises i s .
Le C2=C[ℓ7→ Γ, ℓ:A′]and M2=M[ℓ7→ A].
Type consis ency (5.99) is ex ended o C2⊢MEM (H2,L) : M2by case (LOC1) o De ini-
ion A.2, using (A.3) and he ac ha q′= 0 om p emise o ule EAGERLET (5.97).
Compa ibili y .(M2|(∆, ℓ:A, Θ),C2) ollows om (5.100), ℓbeing sui ably esh, .(A|A, A′)
om p emise o ule EAGERLET (5.97), and De ini ion 5.12 (Global Compa ibili y).
Since exp ession be[ℓ/x]is in whn , i can ei he be a cons uc o applica ion o a λ-abs ac ion.
We now conside each case sepa a ely.
I be[ℓ/x]is in whn and be[ℓ/x]≡c ~y:F om p emise m≥ + 1 + q′+q+p+φH(Γ,∆) +
φH(Θ) (5.101) we wan o de i e m2≥( + 1 + q′) + q+φH2(∆, ℓ:A) + φH2(Θ) and o
ha pu pose we ha e o show + 1 + q′+q+p+φH(Γ,∆) + φH(Θ) ≥( + 1 + q′) + q+
φH2(∆, ℓ:A) + φH2(Θ), o equi alen ly p+φH(Γ,∆) + φH(Θ) ≥φH2(∆, ℓ:A) + φH2(Θ). Fi s
no e ha φH(Γ,∆,Θ) = φH2(Γ,∆,Θ) since ℓis sui ably esh, and hus we jus ha e o show
p+φH2(Γ) ≥φH2(ℓ:A). Since ype A′is idempo en by p emise o EAGERLET (5.97), we
ha e φH2(ℓ:A′) = 0 and hus p+φH2(Γ) = p+φH2(Γ, ℓ:A′). F om Lemma 5.3 (CONS In-
e sion) applied o (A.3) we ob ain .(Γ, ℓ:A′|y1:A1[B/X],...,yk:Ak[B/X]). By Lemma 5.7
gene alised o con ex s, we hen ha e φH2(Γ, ℓ:A′)≥φH2(y1:A1[B/X],...,yk:Ak[B/X])
and hus p+φH2(Γ, ℓ:A′)≥p+φH2(y1:A1[B/X],...,yk:Ak[B/X]). Finally, by he de ini ion
o po en ial (Figu e A.7) we ha e φH2(ℓ:A) = p+φH2(y1:A1[B/X],...,yk:Ak[B/X]) and
hus ob ain wha was needed o p o e p+φH2(Γ) ≥φH2(ℓ:A).
We ha e all he p emises equi ed o apply he induc ion hypo hesis o e e[ℓ/x], ob aining
m′
2,Γ′
2,C′
2,M′
2and m′′
2such ha :
Γ′
20w:C(A.22)
H2,S,Lm′′
2e[ℓ/x]⇓w, H′′ (A.23)
FCUP 111
A.2. P oo o he Soundness Theo em o he Eage Sys em 999.
M2<:M′
2(A.24)
C′
2⊢MEM (H′′,L) : M′
2(A.25)
.(M′
2|(Γ′
2,Θ),C′
2)(A.26)
m′
2≥( + 1 + q′) + φH′′ (w:C) + φH′′ (Θ) (A.27)
m2−m′
2≥m′′
2(A.28)
Le Γ′= Γ′
2,M′=M′
2and C′=C′
2. Equa ions (A.22) (A.25) (A.26) di ec ly es ablish he
p oo obliga ions (5.102) (5.105) (5.106) espec i ely.
Conclusion (5.104) ollows by (A.24) and he ansi i i y o sub yping.
By applying ule EAGERLET⇓Cwi h p emises (A.21), (A.23) and lbeing esh, we es ablish
p oo obliga ion (5.103), yielding
H,S,L1 + m′′
2le x=bein e⇓w, H′′
I we choose m′= +φH′′ (w:C) + φH′′ (Θ) all we need o comple e he p oo o case
EAGERLET is o show ha m−m′≥1 + (m2−m′
2)(≥1 + m′′
2=m′′).
m−m′≥1 + (m2−m′
2)
⇐⇒ m− −φH′′ (w:C)−φH′′ (Θ) ≥1 + m2− −1−q′−φH′′ (w:C)−φH′′ (Θ)
⇐⇒ { q′= 0 by p emise o EAGERLET (5.97), since be[ℓ/x]is in whn }
m≥m2
⇐⇒ + 1 + q′+q+p+φH(Γ,∆) + φH(Θ) ≥ + 1 + q′+q+φH2(∆, ℓ:A) + φH2(Θ)
No e hough ha we al eady showed his las inequali y is ue, when we es ablished he
induc ion p emise (5.101).
This concludes he p oo o case EAGERLET when be[ℓ/x]is in whn and be[ℓ/x]≡c ~y.
I be[ℓ/x]is in whn and be[ℓ/x]≡λy.e′:F om p emise m≥ + 1 + q′+q+p+φH(Γ,∆) +
φH(Θ) (5.101) we wan o de i e m2≥( + 1 + q′+p) + q+φH2(∆, ℓ:A) + φH2(Θ) and o
ha pu pose we ha e o show + 1 + q′+q+p+φH(Γ,∆) + φH(Θ) ≥( + 1 + q′+p) +
q+φH2(∆, ℓ:A) + φH2(Θ), o equi alen ly φH(Γ,∆) + φH(Θ) ≥φH2(∆, ℓ:A) + φH2(Θ). No e
112 FCUP
999. A. A Sys em o Eage E alua ion
ha φH(Γ,∆,Θ) = φH2(Γ,∆,Θ) since ℓis sui ably esh, and hus we jus ha e o show
φH2(Γ) ≥φH2(ℓ:A). This inequali y holds, since by he de ini ion o po en ial (Figu e A.7)
we ha e φH2(ℓ:A) = 0, gi en ha H2(ℓ)is a λ-abs ac ion.
We ha e all he p emises equi ed o apply he induc ion hypo hesis o e e[ℓ/x], ob aining
m′
2,Γ′
2,C′
2,M′
2and m′′
2such ha :
Γ′
20w:C(A.29)
H2,S,Lm′′
2e[ℓ/x]⇓w, H′′ (A.30)
M2<:M′
2(A.31)
C′
2⊢MEM (H′′,L) : M′
2(A.32)
.(M′
2|(Γ′
2,Θ),C′
2)(A.33)
m′
2≥( + 1 + q′+p) + φH′′ (w:C) + φH′′ (Θ) (A.34)
m2−m′
2≥m′′
2(A.35)
Le Γ′= Γ′
2,M′=M′
2and C′=C′
2. Equa ions (A.29) (A.32) (A.33) di ec ly es ablish he
p oo obliga ions (5.102) (5.105) (5.106) espec i ely.
Conclusion (5.104) ollows by (A.31) and he ansi i i y o sub yping.
By applying ule EAGERLET⇓Cwi h p emises (A.21), (A.30) and lbeing esh, we es ablish
p oo obliga ion (5.103), yielding
H,S,L1 + m′′
2le x=bein e⇓w, H′′
I we choose m′= +φH′′ (w:C) + φH′′ (Θ) all we need o comple e he p oo o case
EAGERLET is o show ha m−m′≥1 + (m2−m′
2)(≥1 + m′′
2=m′′).
m−m′≥1 + (m2−m′
2)
⇐⇒ m− −φH′′ (w:C)−φH′′ (Θ) ≥1 + m2− −1−q′−φH′′ (w:C)−φH′′ (Θ)
⇐⇒ { q′= 0 by p emise o EAGERLET (5.97), since be[ℓ/x]is in whn }
m≥m2
⇐⇒ + 1 + q′+q+p+φH(Γ,∆) + φH(Θ) ≥ + 1 + q′+p+q+φH2(∆, ℓ:A) + φH2(Θ)
FCUP 113
A.2. P oo o he Soundness Theo em o he Eage Sys em 999.
No e hough ha we al eady showed his las inequali y is ue, when we es ablished he
induc ion p emise (5.101).
This las sub-case concludes he p oo o case EAGERLET and since he emaining cases
a e simila o (o simple han) he ones p esen ed in he soundness p oo o he lazy sys em
(in Sec ion 5.5.6.7) his also concludes he p oo o he soundness heo em o he eage
sys em.
114 FCUP
999. A. A Sys em o Eage E alua ion
B. Comple e De i a ions
B.1 Simple Example: Analysing Call-By-Need
VAR
z:Tq′′A′q′′
z:A′
VAR
y:Tq(B)qy:BABS
∅0λy.y:Tq(B)−→
qBWEAK
x:Tq′′A′0λy.y:Tq(B)−→
qBABS
∅0λx.λy.y:Tq′′A′−→
0Tq(B)−→
qBAPP
z:Tq′′A′0(λx.λy.y)z:Tq(B)−→
qBLET
∅1le z=zin (λx.λy.y)z:Tq(B)−→
qB
whe e .(A′|A′, A′)
Figu e B.1: Type de i a ion o a non-s ic e alua ion example
115
116 FCUP
999. B. Comple e De i a ions
(Figu e B.1,whe e q=0)WEAK
:T1(T0
(B)−→
0B)1le z=zin (λx.λy.y)z:T0
(B)−→
0B
VAR
x:Tq′(C)q′
x:CABS
∅0λx.x:BWEAK
i:T0(B)0λx.x:B
VAR
:T0(T0
(B)−→
0B)0 :T0
(B)−→
0BAPP
:T0(T0
(B)−→
0B),i:T0(B)0 i :BWEAK
:T0(T0
(B)−→
0B),i:T0(B), :T0(B)0 i :B
VAR
:T0(T0
(B)−→
0B)0 :T0
(B)−→
0BAPP
:T0(T0
(B)−→
0B), :T0(B)0 :BLET
:T0(T0
(B)−→
0B),
:T0(T0
(B)−→
0B),i:T0(B)1le = i in :BSHARE
:T0(T0
(B)−→
0B),i:T0(B)1le = i in :BPREPAY
:T1(T0
(B)−→
0B),i:T0(B)2le = i in :BLET
:T1(T0
(B)−→
0B)3le i=λx.xin ...:BLET
∅4le = (le z=zin (λx.λy.y)z)in le i=λx.xin le = i in :B
whe e B = Tq′(C)−→
q′
C
Figu e B.2: Type de i a ion o a lazy-e alua ion example
FCUP 117
B.2. Highe -O de Func ions: map 999.
B.2 Highe -O de Func ions: map
(Figu e B.4) ABS
map:T0
T0(A−→
q B)−→
0Tq0(Lin)−→
q0Lou , :T0(A−→
q B)
0λxs.case xs o Nil -> le nil =Nil in nil,
Cons x xs′-> le y= x in
le ys′=map xs′in
le ys =Cons y ys′in ys
:Tq0(Lin)−→
q0Lou ABS
map:T0
T0(A−→
q B)−→
0Tq0(Lin)−→
q0Lou
0λ .λxs.case xs o Nil -> le nil =Nil in nil,
Cons x xs′-> le y= x in
le ys′=map xs′in
le ys =Cons y ys′in ys
:T0(A−→
q B)−→
0Tq0(Lin)−→
q0Lou
map:T0
T0(A−→
q B)−→
0Tq0(Lin)−→
q0Lou
0map :T0(A−→
q B)−→
0Tq0(Lin)−→
q0Lou LET
∅1le map =λ .λxs.case xs o Nil -> le nil =Nil in nil,
Cons x xs′-> le y= x in
le ys′=map xs′in
le ys =Cons y ys′in ys
in map :T0(A−→
q B)−→
0Tq0(Lin)−→
q0Lou
whe e
Lin =Lq (3+q +ql+p′
c,1+p′
n, A)
Lou =L0(p′
c, p′
n,T0(B))
L′
in =Lq (0,0, A′),wi h .(A|A, A′)
L′
ou =L0(0,0,T0(B′)),wi h .(B|B, B′)
ql=max(q0, q )
Figu e B.3: Type de i a ion o map applied o a lis wi h po en ial
118 FCUP
999. B. Comple e De i a ions
VAR
xs:Tq0(Lin)q0xs :Lin
CONS
∅0Nil :Lou WEAK
nil:T0(L′
ou )0Nil :Lou
VAR
nil:T0(Lou )0nil :Lou LET
∅1+p′
nle nil =Nil in nil :Lou WEAK
map:T0
T0(A−→
q B)−→
0Tq0(Lin)−→
q0Lou
1+p′
nle nil =Nil in nil :Lou WEAK
map:T0
T0(A−→
q B)−→
0Tq0(Lin)−→
q0Lou , :T0(A−→
q B)
1+p′
nle nil =Nil in nil :Lou
VAR
:T0(A−→
q B)0 :A−→
q BAPP
:T0(A−→
q B),x:Aq x :BWEAK
:T0(A−→
q B),x:A, y:Tq (B′)q x :B
(Figu e B.5) LET
map:T0
T0(A−→
q B)−→
0Tq0(Lin)−→
q0Lou ,
:T0(A−→
q B), :T0(A−→
q B),x:A, xs′:Tq (Lin)
3+q +ql+p′
cle y= x in
le ys′=map xs′in
le ys =Cons y ys′in ys :Lou SHARE
map:T0
T0(A−→
q B)−→
0Tq0(Lin)−→
q0Lou ,
:T0(A−→
q B),x:A, xs′:Tq (Lin)
3+q +ql+p′
cle y= x in
le ys′=map xs′in
le ys =Cons y ys′in ys :Lou CASE
map:T0
T0(A−→
q B)−→
0Tq0(Lin)−→
q0Lou , :T0(A−→
q B),xs:Tq0(Lin)
q0case xs o Nil -> le nil =Nil in nil,
Cons x xs′-> le y= x in
le ys′=map xs′in
le ys =Cons y ys′in ys :Lou
Figu e B.4: Auxilia y ype de i a ion o map applied o a lis wi h po en ial
FCUP 119
B.2. Highe -O de Func ions: map 999.
VAR
map:T0
T0(A−→
q B)−→
0Tq0(Lin)−→
q0Lou
0map :T0(A−→
q B)−→
0Tq0(Lin)−→
q0Lou APP
map:T0
T0(A−→
q B)−→
0Tq0(Lin)−→
q0Lou , :T0(A−→
q B)
0map :Tq0(Lin)−→
q0Lou SUBTYPE
map:T0
T0(A−→
q B)−→
0Tq0(Lin)−→
q0Lou , :T0(A−→
q B)
0map :Tmin(q0,q )(Lin)−→
q0Lou APP
map:T0
T0(A−→
q B)−→
0Tq0(Lin)−→
q0Lou , :T0(A−→
q B),
xs′:Tmin(q0,q )(Lin)q0map xs′:Lou WEAK
map:T0
T0(A−→
q B)−→
0Tq0(Lin)−→
q0Lou , :T0(A−→
q B),
xs′:Tmin(q0,q )(Lin),ys′:Tq0(L′
ou )q0map xs′:Lou
CONS
y:T0(B),ys′:T0(Lou )0Cons y ys′:Lou WEAK
y:T0(B),ys′:T0(Lou ),ys:T0(L′
ou )0Cons y ys′:Lou
VAR
ys:T0(Lou )0ys :Lou LET
y:T0(B),ys′:T0(Lou )1+p′
cle ys =Cons y ys′in ys :Lou PREPAY
y:T0(B),ys′:Tq0(Lou )1+q0+p′
cle ys =Cons y ys′in ys :Lou LET
map:T0
T0(A−→
q B)−→
0Tq0(Lin)−→
q0Lou , :T0(A−→
q B),
xs′:Tmin(q0,q )(Lin),y:T0(B)
2+q0+p′
cle ys′=map xs′in le ys =Cons y ys′in ys :Lou PREPAY*
map:T0
T0(A−→
q B)−→
0Tq0(Lin)−→
q0Lou , :T0(A−→
q B),
xs′:Tq (Lin),y:T0(B)
2+ql+p′
cle ys′=map xs′in le ys =Cons y ys′in ys :Lou PREPAY
map:T0
T0(A−→
q B)−→
0Tq0(Lin)−→
q0Lou , :T0(A−→
q B),
xs′:Tq (Lin),y:Tq (B)
2+q +ql+p′
cle ys′=map xs′in le ys =Cons y ys′in ys :Lou
∗No e ha ule PREPAY jus i ies he yping xs′:Tq (Lin) om xs′:Tmin(q0,q )(Lin)
by p epaying he amoun max(q −q0,0).
Figu e B.5: Auxilia y ype de i a ion o map applied o a lis wi h po en ial (con .)