Computational Lambda-Calculus and Monads-英文文献.pdf

Computational lamb dacalculus and monads Eugenio Moggi LFCS Dept of Comp Sci University of Edinburgh EH JZ Edinburgh UK emlfcsedacuk Octob er Abstract The calculus is considered an useful mathematical to ol in the study of programming languages since programs can b e identied with terms However if one go es further and uses   conversion to prove equivalence of programs then a gross simplication 1 is intro duced that may jeopardise the applicability of theoretical results to real situations In this pap er we intro duce a new calculus based on a categorical semantics for computations This calculus provides a correct basis for proving equivalence of programs indep endent from any sp ecic computational mo del Intro duction This pap er is ab out logics for reasoning ab out programs in particular for proving equivalence of programs Following a consolidated tradition in theoretical computer science we identify programs with the closed terms p ossibly containing extra constants corresp onding to some features of the programming language under con sideration There are three approaches to proving equivalence of programs The op erational approach starts from an op erational semantics eg a par tial function mapping every program ie closed term to its resulting value if any which induces a congruence relation on op en terms called op erational equivalence see eg Plo Then the problem is to prove that two terms are op erationally equivalent  On leave from Universita di Pisa Research partially supp orted by the Joint Collab oration Cont