Programming in the λ-Calculus - From Church to Scott and Back

《Programming in the λ-Calculus - From Church to Scott and Back》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、Programmingintheλ-Calculus:FromChurchtoScottandBackJanMartinJansenFacultyofMilitarySciences,NetherlandsDefenceAcademy,DenHelder,TheNetherlandsjm.jansen.04@nlda.nlAbstract.Althoughtheλ-calculusiswellknownasauniversalpro-gramminglanguage,itisseldomusedforactualpr

2、ogrammingorexpressingalgorithms.Herewedemonstratethatitispossibletousetheλ-calculusasacomprehensiveformalismforprogrammingbyshow-inghowtoconvertprogramswritteninfunctionalprogramminglan-guageslikeCleanandHaskelltoclosedλ-expressions.Thetransformationisbasedonus

3、ingtheScott-encodingforAlgebraicDataTypesinsteadofthemorecommonChurchencoding.Inthiswaywenotonlyobtainanencodingthatisbettercomprehensiblebutthatisalsomoreefficient.AsaproofofthepuddingweprovideanimplementationofEratos-thenes’primesievealgorithmasaself-contained,

4、143characterlength,λ-expression.1TheChurchandScottEncodingsforAlgebraicDataTypesTheλ-calculuscanbeconsideredasthemotherofall(functional)program-minglanguages.Everycourseortextbookonλ-calculus(e.g.[1])spendssometimeonshowinghowwell-knownprogrammingconstructscanb

5、eexpressedintheλ-calculus.ItcommonlystartsbyexplaininghowtorepresentFornaturalnumbers,inalmostallcasestheChurchnumeralsarechosenastheleadingex-ample.ThedefinitionofChurchnumeralsandoperationsonthemshowsthatitispossibletousetheλ-calculusforallkindsofcomputationsa

6、ndthatitisindeedauniversalprogramminglanguage.TheChurchencodingcanbegener-alizedfortheencodingofgeneralAlgebraicDataTypes(see[2]).Thisencodingallowsforastraightforwardimplementationofiterative(primitiverecursive)orfold-likefunctionsondatastructures,butoftenrequ

7、irescomplexandinefficientconstructionsforexpressinggeneralrecursion.Itislesscommonlyknownthatthereexistanalternativeencodingofnum-bersandalgebraicdatastructuresintheλ-calculus.Thisencodingisrelativelyunknown,andindependently(re)discoveredbyseveralauthors(e.g.[9,8

8、,10]andtheauthorofthispaper[6]),butoriginallyattributedtoScottinanunpub-lishedlecturewhichiscitedinCurry,HindleyandSeldin([4],page504)as:DanaScott,Asystemoffunctionalabstrac