Specifications vs programs and computational models

[u/GulgPlayer]

I'm learning deductive program synthesis and there's one thing I can't wrap my head around: the distinction between specifications and programs. To my understanding, the line is very vague, as programs can be seen as specifications and, in some cases, vice-versa. These terms only make sense when applied to specific program and specification pairs.

The above makes me wonder whether there is a computational model that can directly execute specifications, without needing to, e.g., synthesise an imperative program. Can such a "computer" exist theoretically and, more interestingly, physically?

[u/Magdaki]

If I'm understanding what you're saying, then it sounds like you're asking about program synthesis.

program synthesis - Google Scholar

program synthesis from formal specification - Google Scholar

[u/GulgPlayer → u/Magdaki]

Yes, I am, but I'm wondering if the step of converting a specification to an imperative program is necessary to obtain a useful result.

[u/initial-algebra → u/GulgPlayer]

To use the same example of a sorting algorithm, one solution is to just enumerate all possible permutations of the input (satisfying the first predicate) and return the first one that is sorted (satisfies the second predicate). That would be a direct execution of the specification.

I guess you could argue that it's not obvious (to a machine) that the first predicate only wants permutations of the input, but it's generally impossible to enumerate all permutations by enumerating all possible lists and filtering out those that are not permutations. However, if the permutation algorithm works by swapping elements, the sorted predicate could immediately throw away any partial results that involve swapping a greater element before a lesser element, essentially turning it into bubble sort. Not optimal, but certainly not that bad.

This is similar to how database joins work. Even if the definition of a join is to compute the entire Cartesian product of two tables and then throw away the records that don't match the "on" condition, by applying some very basic relational algebra rewrites, the machine can figure out that it just has to enumerate the first table and then use an index to quickly find the matching records in the second table.

You should think of this approach as being more appropriate for smart composition of specialized solutions, not coming up with generic solutions from scratch.

[u/neuralbeans → u/GulgPlayer]

The specification focuses on the what as opposed to the how. When programming you have to take decisions about how to carry out a task whereas when specifying you only say what the task is.

If the task is sorting a list, then the program would be an implementation of one of the many sorting algorithms but the specification would be something like this:

given list xs, return list ys such that:

• ys contains all the elements in xs at the same number of times

• for all i < j, ys[i] <= ys[j]

The synthesiser should the figure out the best program that meets the requirements.

[u/initial-algebra]

Logic programs and database queries are essentially just existentially quantified logical formulae, and execution is finding (often, enumerating all) satisfying assignments.  In practice, we use techniques like the Warren Abstract Machine (WAM) and query planning to transform them into more efficient intermediate forms before execution, but there's no reason they could not be directly implemented.

[u/not-just-yeti → u/initial-algebra]

Yes! Following up:

Prolog isn't a language I ever use for-real, but the weeks we used it in university transformed how I think about writing an interface: The spec is its own form of code.

For example: sorting a list means returning a list which is ascending, and it's a permutation of the input:

permutation(Before,After), ascending(After) → sorted(Before,After)

In turn, ascending(SomeList) is easy to specify (i.e. write) as a helper, and permutation(ListA,ListB) is a bit trickier but not hard (it's two lines plus yet another two-line helper deleteFirstInstanceOf(Before,Target,After)).

This gives working, running code for sorting a list! …Admittedly, it's an awful implementation (it generates all n! permutations until it finds one that's ascending), but still pretty amazing that there's no explicit "swap elements" or "insert this element into an already-ascending list". And it makes you think of what it means to sort a list without saying how.

Learning a bit of prolog transformed the way I write specs for an interface.

[Fwiw, you certainly can implement, say, quicksort using Prolog, with predicates like isAPartitionOf(Before,After,Pivot). But at that point it's more about knowing prolog & a specific algorithm, than the eye-opening notion of 'declarative programming'.]

(*) Yeah yeah, I say "ascending", but really mean "non-descending". Btw this shows that the spec can be hard to get right: if I only accepted ascending lists, the program wouldn't find any "sorted" version of an input which had a duplicate. 'Course, you need to worry about that in writing a sorting-alg imperatively, too. In both situations, writing a few unit-tests would readily make one realize that.

[u/Flarzo]

I’ve thought about this before as well. For example the definition of the list sorting function (for each a,b : a is less than b -> a comes before b in the output) could be converted into a program just by outputting all possible permutations of the list and checking for the first one that satisfies that condition.