Publication
The HasCASL Prologue - Categorical Syntax and Semantics of the Partial $lambda$-calculus
Lutz Schröder
In: Theoretical Computer Science, Vol. 353, Pages 1-25, 2006.
Abstract
We develop the semantic foundations of the specification language HasCASL, which combines algebraic specification and functional programming on the basis of Moggi's partial $lambda$-calculus. Generalizing Lambek's classical equivalence between the simply typed $lambda$-calculus and cartesian closed categories, we establish an equivalence between partial cartesian closed categories (pccc's) and partial $lambda$-theories. Building on these results, we define (set-theoretic) notions of intensional Henkin model and syntactic $lambda$-algebra for Moggi's partial $lambda$-calculus. These models are shown to be equivalent to the originally described categorical models in pccc's via the global element construction. The semantics of HasCASL is defined in terms of syntactic $lambda$-algebras. Correlations between logics and classes of categories facilitate reasoning both on the logical and on the categorical side; as an application, we pinpoint unique choice as the distinctive feature of topos logic (in comparison to intuitionistic higher-order logic of partial functions, which by our results is the logic of pccc's with equality). Finally, we give some applications of the model-theoretic equivalence result to the semantics of HasCASL and its relation to first-order CASL.