Discussion
incoming thread about program synthesis!
specifically, about how feasible it is to start from a fairly intuitive description of a problem (sorting) in natural language and transform that into a mathematical statement, similar to how we do word problems in mathematics or physics
in order to make use of this definition, we need to have definitions for each of the parts on the RHS of the equation
`inOrder` is one such thing on the RHS there, and defining it is an interesting little puzzle
here is a correct definition:
inOrder [] = True
inOrder (x :: zs) = True
inOrder (x :: y :: zs) = x <= y && inOrder (y :: zs)
but when we say that that definition is correct, what we mean is that it does what we as the programmer, specifier, researcher, etc. intend by `inOrder`, namely that it, you know, ensures that the elements are in order
Install bonfire.cafe
Get the full app experience
so, one of the classic ways of specifying a sorting algorithm in the functional program synthesis/derivation literature is more or less as follows:
sort xs = head (filter inOrder (permutations xs))