On Sunday, June 5, 2016 at 10:21:06 AM UTC+3, Stephan Merz wrote:
On constructing the data structure vs. relying on assumptions: I think both have their place. For example, in mathematics one typically constructs, say, the real numbers via Dedekind cuts, but presents algebraic structures such as groups through characteristic axioms. For our purposes, presentation through ASSUME leaves more freedom for later implementations of the data structure later, since only the stated properties have to be satisfied – but knowing when you have stated enough properties can be difficult.
Doesn't your approach essentially use CHOOSE to magically choose a model (basically, pull it out of thin air) in case the axiomatization isn't complete, in a way that is equally opaque to proofs? I mean, in the end, all the proofs have to work with is your assumptions, not any other property of a model that's been CHOsen (unless maybe those properties are known through existing algebras, like Nat ???)
Case in point: your last conjunct (trivially) follows from the induction rule for S that was included in my specification, but does not imply that rule. To see this, consider a structure where S is the set of finite *and infinite* sequences over X
Ah, right. Whenever you're confused about axioms, the answer lies with uncountable models! But I still don't see how your approach addresses this. You might as well have mistakenly included my axiom instead of yours, and CHOOSE would still work (wouldn't it?), and so the problem of knowing when you've stated enough properties remains, no?
Ron