I still don’t get the goal of what you are trying to do (the puzzle this work should clarify), which I feel like I should’ve. As a shot in the dark, maybe abstract interpretation[1] in general and abstracted abstract machines[2] in particular might be useful for something here.
Thanks for the pointers, I hadn’t seen the Abstracting Abstract Machines paper before.
If you mean you specifically don’t get the goal of minimal abstractions under this partial order: I’m much less convinced they’re useful for anything than I used to be, currently not sure.
If you mean you don’t get the goal of the entire agenda, as described in the earlier agenda post: I’m currently mostly thinking about mechanistic anomaly detection. Maybe it’s not legible right now how that would work using abstractions, I’ll write up more on that once I have some experimental results (or maybe earlier). (But happy to answer specific questions in the meantime.)
I meant the general agenda. For abstract interpretation, I think the relevant point is that quotienting a state space is not necessarily a good way of expressing abstractions about it, for some sense of “abstraction” (the main thing I don’t understand is the reasons for your choice of what to consider abstraction). Many things want a set of subspaces (like a topology, or a logic of propositions) instead of a partition, so that a point of the space doesn’t admit a unique “abstracted value” (as in equivalence class it belongs to), but instead has many “abstracted values” of different levels of precision simultaneously (the neighborhood filter of a point, or the theory of a model).
With abstract interpretation, there can be even more distinctions, the same concrete point can be the image of multiple different abstract points, which are only distinct in the abstract space, not in terms of their concretization in the concrete space.
Another way of approaching this is to ask for partial models of a phenomenon instead of models that fully specify it. This is natural for computations, which can be described by operators that gradually build a behavior out of its partial versions. But in other contexts, a space of partial models can also be natural, with some models specifying more details than other models, and a process of characterizing some object of study could be described by an operator/dynamic that discovers more details, moves from less detailed models to more detailed ones.
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:
I still don’t get the goal of what you are trying to do (the puzzle this work should clarify), which I feel like I should’ve. As a shot in the dark, maybe abstract interpretation[1] in general and abstracted abstract machines[2] in particular might be useful for something here.
ND Jones, F Nielson (1994) Abstract Interpretation: A Semantics-Based Tool for Program Analysis
D Van Horn, M Might (2011) Abstracting Abstract Machines: A Systematic Approach to Higher-Order Program Analysis
Thanks for the pointers, I hadn’t seen the Abstracting Abstract Machines paper before.
If you mean you specifically don’t get the goal of minimal abstractions under this partial order: I’m much less convinced they’re useful for anything than I used to be, currently not sure.
If you mean you don’t get the goal of the entire agenda, as described in the earlier agenda post: I’m currently mostly thinking about mechanistic anomaly detection. Maybe it’s not legible right now how that would work using abstractions, I’ll write up more on that once I have some experimental results (or maybe earlier). (But happy to answer specific questions in the meantime.)
I meant the general agenda. For abstract interpretation, I think the relevant point is that quotienting a state space is not necessarily a good way of expressing abstractions about it, for some sense of “abstraction” (the main thing I don’t understand is the reasons for your choice of what to consider abstraction). Many things want a set of subspaces (like a topology, or a logic of propositions) instead of a partition, so that a point of the space doesn’t admit a unique “abstracted value” (as in equivalence class it belongs to), but instead has many “abstracted values” of different levels of precision simultaneously (the neighborhood filter of a point, or the theory of a model).
With abstract interpretation, there can be even more distinctions, the same concrete point can be the image of multiple different abstract points, which are only distinct in the abstract space, not in terms of their concretization in the concrete space.
Another way of approaching this is to ask for partial models of a phenomenon instead of models that fully specify it. This is natural for computations, which can be described by operators that gradually build a behavior out of its partial versions. But in other contexts, a space of partial models can also be natural, with some models specifying more details than other models, and a process of characterizing some object of study could be described by an operator/dynamic that discovers more details, moves from less detailed models to more detailed ones.
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