The Lazy Lambda Calculus: an investigation into the foundations of functional programming
C.-H. Luke Ong · Spiral (Imperial College London) · 2021
T he com m only accepted basis for functional program m ing is the A-calculus; and it is folklore th a t A-calculus is th e prototypical functional language in puri fied form.T here is, nonetheless, a fundam ental m ism atch betw een theory and practice:• M uch of w hat is known ab o u t th e model theory an d proof theory of the A-calculus is s e n s ib le in n atu re, i.e. all unsolvables are identified.Crucially, Ax._L = _L where _L represents any divergent te rm (or program ).• In practice, however, m ost im plem entations of functional languages are la z y , i.e. program s are reduced in n o r m a l o rd e r to w e a k h e a d n o r m a l fo r m s (w hnf), corresponding to a c a ll-b y -n a m e sem antics.Consequently, Ax._L ^ _L, because all abstractions, being in whnf, are deem ed to be legitim ate and m eaningful program s.T his thesis seeks to develop a th eo ry of la z y functional program m ing th a t corresponds to practice in th e fram ew ork of the classical A-calculus.T h e m ain topics studied in this thesis are as follows:• T he fundam ental notions of solvability, A-definability (of num eric func tions) , A-theories and tree sem antics in th e classical sensible A-calculus are reviewed and revised in th e light of th e lazy regime.• Different form ulations of la z y X -m o d e ls are presented an d shown equivalent.We prove a L o c a l S tr u c t u r e T h e o re m for th e class of fre e la z y P S E -m o d e ls .• T h e full a b strac tio n problem recast in th e lazy A-calculus, a la A bramsky, is studied.We focus on th e la z y X -c a lc u lu s w ith co n ve rg e n ce te s tin g and stu d y th e problem of call-by-value sim ulation.A general m ethod for constructing fully a b stra c t m odels w hich are re tra c ts of D -th e initial solution of th e dom ain equation D = [ D -> D ]± -w ith respect to a class of sufficiently expressive variants of A bram sky's At is developed.T he full a b strac tio n problem of At is reduced by this m ethod to an open question of th e c o n s e r v a t iv it y of a labelled version of Ai over itself.• A proof system for the lazy A-calculus (w ith convergence testing) based on S co tt's logic of existence w hich is c o rre c t w ith resp ect to A i s introduced and given a s o u n d and c o m p le te in te rp re ta tio n in p a rtia l categories.L a z y re fle x iv e o b je c ts w ith enough p o in ts in p a r t ia l C a r t e s ia n c lo s e d d o m in ic a l c a te g o rie s give rise to lazy A-models in w hich convergence testing is defin able, th ereb y yielding a p artial categories sem antics.P h D Thesis M ay 31, 1988 r C h a p ter 1 In tr o d u c tio n 1.1 P ream ble Functional languages have had a sm all group of predom inantly B ritish advo cates and cognoscenti for m any years, u n til, it would seem, th e fateful Turing A w ard speech delivered by J. W. Backus in 1978 [Bac78].Since th en , m any m ore functional program m ing languages have sprung up, notably: LM L [Aug84], M IRAN D A [Tur85], PO N D E R [Fai85], L IS P K IT [Hen80], TA L E [BvL86] and O RW ELL [Wad85].A growing in terest in th e theory and practice of functional program m ing and the allocation of sizable resources to research in th e area over th e p a st few years are clear gestures of recognition and ap p reciatio n by th e com p u tin g com m unity a t large.Functional languages are now beginning to a ttra c t a m uch w ider interest; and several developm ents including th e advent of highly parallel VLSI architectures are prom ising to tra n slate th e theoretical and pro gram m ing advantages into practical reality.See e.g.[DR81].F unctional languages trace th eir origins to th e lam b d a calculus developed by C hurch in th e 1930's [Chu36] and recursion equations n o ta tio n developed by K leene, also in th e 1930's [Kle36].L am bda Calculus arose from research work in th e th eo ry of co m putability and in p a rtic u la r, in an a tte m p t by C hurch to pin dow n m athem atically th e notion of num erical functions w hich are com putable in a m echanical or algorithm ic fashion.C h u rch 's proposal, or C h u rch 's thesis, as it becam e know n later, was to identify th e intuitively apprehensible class of effectively com putable num erical functions w ith those th a t are definable in th e lam b d a calculus given a suitable coding of th e n atu ral num bers in th e calculus.T h ere were other proposals to cap tu re th is class of com putable functions, notably: /i-recursive and p a rtia l recursive functions by Godel and K leene in 1936; Turing M achine com putable functions by A lan T uring [Tur36] an d U niversal R egister M achine com putable functions by Shepherdson and Sturgis [SS63].A lthough th e re is great diversity am ong these various approaches an d each has its own 8 r PROOF Unpacking the definitions, we see that for all d, e E D: d C e d ^/= J> [el|p & V cE D .f{c)C ^(c)].Thus the domain ordering is an applicative bisimulation, and so is included in For the converse, we prove a stronger statement.Wlog, suppose d\J.and e]].. CLAIM: Vd, e E D.\fk E w.d e =>■ d* C e*. which clearly implies d e => d C e since d = Ukeu d*.The base case k = 0 is trivial.Suppose true for k.Wlog, assume d\f and el]..Then, let d Ef+1 e.By definition, V/ E D.dfk £ f efk.Invoking the induction hypothesis, we have V / E D.(dfk)k C («/*)*.which implies V/ E D .dk+ if Q ek+1 f.Now, dk+ity and ejb+1l|, the result that follows from the above Proposition.□ As a corollary, we see that D is an aswd.Define an interpretation of A-terms in D as follows: for c l E D and M