4 ms·

Are there type systems where these axioms can be encoded? Dependent typing, perhaps.

im3w1l 9y ago
Instead of having a function that says whether one object is bigger than another, you could define an ordering by having a function that maps objects to say natural numbers or real numbers or some other object with a known good comparison, and then compare the mapped objects. So instead of implementing f in f(a, b), you'd implement f in f(a) < f(b)
- abecedarius 9y ago
  Also you could resolve hashing in the same way: i.e. making sure that hashing is consistent with equality. Two objects of the same type are equal if f(a) == f(b), and have hashcode hash(type, f(a)).
aweinstock 9y ago
As an exercise in learning Coq, I've implemented a proof-carrying version of the partial-ordering relation: https://github.com/aweinstock314/coq-stuff/blob/a1831f9e1e957c0038996a5a65fcb4391967660a/poset_lattice.v#L3-L24 https://github.com/aweinstock314/coq-stuff/blob/a1831f9e1e95... There's four different types there: POSET, POSET_PROOFS, Pord, and POSET'. - POSET only has an underlying type t and a function "leq" that takes two elements of type t and returns a bool (but doesn't enforce semantics of that bool). - POSET_PROOFS embeds a POSET, and carries three proofs (reflexivity, antisymmetry, and transitivity) certifying that the underlying "leq" function is actually the less-than-or-equal function of a partial ordering. - Pord is a result type with 4 values meant to denote the exhaustive possiblities of "strictly less"/"equal"/"strictly greater"/"uncomparable". - POSET' has a type t', a function "pcomp" that takes two elements of type t' and returns a Pord, and a proof for transitivity in the "strictly less" case. POSET' has fewer fields to instantiate, but POSET_PROOFS allows writing proofs that are closer to traditional math. Fortunately, the fact that it's possible to write conversions between POSET_PROOFS and POSET' (done in the code as "from" and "to" in the POSET_ISOMORPHIMS module right below) indicate that they have the same properties.
- deleted 9y ago
  [deleted]

Instead of having a function that says whether one object is bigger than another, you could define an ordering by having a function that maps objects to say natural numbers or real numbers or some other object with a known good comparison, and then compare the mapped objects. So instead of implementing f in f(a, b), you'd implement f in f(a) < f(b)

abecedarius 9y ago
Also you could resolve hashing in the same way: i.e. making sure that hashing is consistent with equality. Two objects of the same type are equal if f(a) == f(b), and have hashcode hash(type, f(a)).

aweinstock 9y ago

As an exercise in learning Coq, I've implemented a proof-carrying version of the partial-ordering relation: https://github.com/aweinstock314/coq-stuff/blob/a1831f9e1e957c0038996a5a65fcb4391967660a/poset_lattice.v#L3-L24 https://github.com/aweinstock314/coq-stuff/blob/a1831f9e1e95... There's four different types there: POSET, POSET_PROOFS, Pord, and POSET'. - POSET only has an underlying type t and a function "leq" that takes two elements of type t and returns a bool (but doesn't enforce semantics of that bool). - POSET_PROOFS embeds a POSET, and carries three proofs (reflexivity, antisymmetry, and transitivity) certifying that the underlying "leq" function is actually the less-than-or-equal function of a partial ordering. - Pord is a result type with 4 values meant to denote the exhaustive possiblities of "strictly less"/"equal"/"strictly greater"/"uncomparable". - POSET' has a type t', a function "pcomp" that takes two elements of type t' and returns a Pord, and a proof for transitivity in the "strictly less" case. POSET' has fewer fields to instantiate, but POSET_PROOFS allows writing proofs that are closer to traditional math. Fortunately, the fact that it's possible to write conversions between POSET_PROOFS and POSET' (done in the code as "from" and "to" in the POSET_ISOMORPHIMS module right below) indicate that they have the same properties.

deleted 9y ago
[deleted]