|
|
计算机科学技术学报 1998
A crash course in λ-calculus
|
Abstract:
Thetalkpresentedthebasicresultsofλ-calculus.Aftergivingthesyntaxofterms(concretesyntax,abstractsyntaxusingdeBruijn'sindices)andthedefinitionofsubstitution,theβ-reductionrelation(strongreduction)ispresentedanditsmainpropertieslisted:.parallel-moveslemma,leadingtoconfluenceandtheChurch-Rosserpropertyofβ-conversion,anduniquenessofnormalforms.standardisationandthecompletenessofthenormalreductionstrategy(leftmost-outermost).finally,η-conversionisdiscussed,andtheseparabilityproperty(Bohmtheorem…
