欢迎来到天天文库
浏览记录
ID:39813715
大小:192.92 KB
页数:13页
时间:2019-07-11
《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
此文档下载收益归作者所有