Name
Abstract | ||
|---|---|---|
We prove that the full completeness theorem for MLL+Mix holds by the simple interpretation via formulas as objects and proofs as Z-invariant morphisms in the ∗-autonomous category of topologized vector spaces. We do this by generalizing the recent work of Blute and Scott (Ann. Pure Appl. Logic 77 (1996) 101–142) where they used the semantical framework of dinatural transformation introduced by Girard–Scedrov–Scott (in: Y. Moschovakis (Ed.), Logic from Computer Science, vol. 21, Springer, Berlin, 1992, pp. 217–241). By omitting the use of dinatural transformation, our semantics evidently allows the interpretation of the cut-rule, while the original Blute–Scott's does not. Moreover, our interpretation for proofs is preserved automatically under the cut elimination procedure. (In this sense, our semantics is considered as a denotational semantics.) In our semantics proofs themselves are characterized by the concrete algebraic notion “Z-invariance”, and our denotational semantics provides the full completeness. Our semantics is naturally extended to the full completeness semantics for CyLL+Mix owing to an elegant method of Blute–Scott (J. Symbolic Logic 63(4) (1998) 1413–1436) (which is a sequel to (Blute and Scott (Ann. Pure Appl. Logic 77 (1996) 101–142))). |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1016/S0168-0072(00)00029-4 | Annals of Pure and Applied Logic |
Keywords | Field | DocType |
03F07,03F52,18A15,18B30,68Q55 | Denotational semantics of the Actor model,Discrete mathematics,Operational semantics,Normalisation by evaluation,Gödel's completeness theorem,Algebra,Denotational semantics,Domain theory,Complete partial order,Higher-order logic,Mathematics | Journal |
Volume | Issue | ISSN |
107 | 1-3 | 0168-0072 |
Citations | PageRank | References |
1 | 0.38 | 6 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Masahiro Hamano | 1 | 39 | 7.66 |