User loginNavigation |
Specifying Solvers?In parsing, (non-dependent) type systems, and semantics, we have made remarkable progress in specification. In the first two areas, we have reference processing models and reference specification languages that tell us, definitively, whether a program is admissible or not. That is: they are definitive both positively and negatively. In the last, we have definitive specification provided the program is well-formed and well-typed. The situation seems less clear for solvers. We appear to have reference models for how a solver operates, and reference languages for specifying what a solver may do (that is: the legal operations) but no way of specifying what the solver must do, nor the conditions under which convergence with a solution (or at least certain types of convergence) are guaranteed. One consequence of this is that the specification of languages that rely on general-purpose solvers is necessarily reduced to "the implementation is the definition", and in some cases this leaves us in a state where the admissibility of a program may depend on the details of a particular solver implementation or even the performance of the CPU on which the compile occurs. I see no problem with stronger vs weaker compilers. My concern here is to ensure that there exists a precise specification of the language that all correct implementations must accept in order to be conforming implementations. Is there work or progress along these lines that I should look at? By shap at 2010-04-07 20:24 | LtU Forum | previous forum topic | next forum topic | other blogs | 5793 reads
|
Browse archives
Active forum topics |
Recent comments
25 weeks 4 days ago
25 weeks 4 days ago
25 weeks 4 days ago
47 weeks 5 days ago
52 weeks 15 hours ago
1 year 1 week ago
1 year 1 week ago
1 year 4 weeks ago
1 year 8 weeks ago
1 year 8 weeks ago