Thanks for the input! (and sorry for the slow response)
If we understand an abstraction to mean a quotient of the full computation/model/..., then we can consider the space of all abstractions of a specific computation. Some of these will be more fine-grained than others, they will contain different aspects of information, etc. (specifically, this is just the poset of partitions of a set). To me, that sounds pretty similar to what you’re talking about, in which case this would mainly be a difference in terminology about what “one” abstraction is? But there might also be differences I haven’t grasped yet. Looking into abstract interpretation is still on my reading list, I expect that will help clear things up.
For my agenda specifically, and the applications I have in mind, I do currently think abstractions-as-quotients is the right approach. Most of the motivation is about throwing away unimportant information/low-level details, whereas it sounds like the abstractions you’re describing might add details in some sense (e.g. a topology contains additional information compared to just the set of points).
You might also want to look into predicate abstraction (which is a quotienting abstraction) and CEGAR (which is a way of making a quotienting abstraction progressively more detailed in order to prove a particular specification). I can’t think of an introductory text I like, but the topic could be bootstrapped from these:
Thanks for the input! (and sorry for the slow response)
If we understand an abstraction to mean a quotient of the full computation/model/..., then we can consider the space of all abstractions of a specific computation. Some of these will be more fine-grained than others, they will contain different aspects of information, etc. (specifically, this is just the poset of partitions of a set). To me, that sounds pretty similar to what you’re talking about, in which case this would mainly be a difference in terminology about what “one” abstraction is? But there might also be differences I haven’t grasped yet. Looking into abstract interpretation is still on my reading list, I expect that will help clear things up.
For my agenda specifically, and the applications I have in mind, I do currently think abstractions-as-quotients is the right approach. Most of the motivation is about throwing away unimportant information/low-level details, whereas it sounds like the abstractions you’re describing might add details in some sense (e.g. a topology contains additional information compared to just the set of points).
You might also want to look into predicate abstraction (which is a quotienting abstraction) and CEGAR (which is a way of making a quotienting abstraction progressively more detailed in order to prove a particular specification). I can’t think of an introductory text I like, but the topic could be bootstrapped from these:
E Clarke, D Kroening, N Sharygina, K Yorav (2004) Predicate Abstraction of ANSI–C Programs using SAT
D Beyer, A Cimatti, A Griggio, ME Keremoglu, R Sebastiani (2009) Software Model Checking via Large-Block Encoding