Galois connections and computer science applications. (English) Zbl 0622.06004
Category theory and computer programming, Workshop Guildford/U.K. 1985, Lect. Notes Comput. Sci. 240, 299-312 (1986).
[For the entire collection see Zbl 0607.00015.]
For a function between two posets it is proved that there arises a Galois connection iff (1) the function preserves all existing joins and (2) the preimage of each principle ideal has a join. The result is applied to proving the correctness of compilers.
For a function between two posets it is proved that there arises a Galois connection iff (1) the function preserves all existing joins and (2) the preimage of each principle ideal has a join. The result is applied to proving the correctness of compilers.
Reviewer: J.Adámek
MSC:
| 06A15 | Galois correspondences, closure operators (in relation to ordered sets) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68P05 | Data structures |
