Directed sets intervals (#77)

* A join semi-lattice is a directed set. * Add definition of empty set. * Declare enumeration of countable sets. * Rename: Interval -> ConvexSet. * Adding ConnectedSpace. * Adding bounded (semi-)lattice. * Adding singleton set and union.
vincentk · Dec 30, 2024 · afaf4c5 · afaf4c5
1 parent af9e761
commit afaf4c5
Show file tree

Hide file tree

Showing 37 changed files with 602 additions and 122 deletions.
diff --git a/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/algebra/numbers/Ds.java b/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/algebra/numbers/Ds.java
@@ -55,6 +55,7 @@ public Ds times(Ds that) {
 	return of(re.x(that.re), ri.十(ir));
     }
 
+    @Override
     public boolean eq(Ds that) {
 	return this.re.eq(that.re) && this.ep.eq(that.ep);
     }

diff --git a/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/algebra/numbers/N.java b/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/algebra/numbers/N.java
@@ -11,7 +11,7 @@
 import com.github.vincentk.dedekind.geometry.NumberLine;
 import com.github.vincentk.dedekind.sets.Cardinality;
 import com.github.vincentk.dedekind.sets.Finite;
-import com.github.vincentk.dedekind.sets.ordered.Interval;
+import com.github.vincentk.dedekind.sets.ordered.ConvexSet;
 import com.github.vincentk.dedekind.sets.ordered.TotallyOrdered;
 
 /**
@@ -27,7 +27,7 @@ public interface N<
 SemiRings.Naturals,
 Finite<N.Nat, Cardinality.Finite, T>,
 NumberLine<N.Nat, Cardinality.Finite, T>,
-Interval.HalfOpen.Right<N.Nat, T, T, Cardinality.Finite, T>
+ConvexSet.HalfOpen.Right<N.Nat, T, Cardinality.Finite, T>
 {
     /**
      * Elements &isin; {@link Z}.

diff --git a/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/algebra/numbers/Z.java b/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/algebra/numbers/Z.java
@@ -8,7 +8,7 @@
 import com.github.vincentk.dedekind.geometry.NumberLine;
 import com.github.vincentk.dedekind.sets.Cardinality;
 import com.github.vincentk.dedekind.sets.Set;
-import com.github.vincentk.dedekind.sets.ordered.Interval;
+import com.github.vincentk.dedekind.sets.ordered.ConvexSet;
 
 /**
  * The integer numbers.
@@ -44,7 +44,7 @@ interface Integer<E extends Integer<E>>
     interface Z64
     extends
     Z<Z64.Int64, Z64>,
-    Interval.Closed<Z64.Int64, Z64, Z64, Cardinality.Countable, Z64>
+    ConvexSet.Closed<Z64.Int64, Z64, Cardinality.Countable, Z64>
     {
 	public interface Int64
 	extends Integer<Int64>

diff --git a/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/algebra/structures/Magma.java b/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/algebra/structures/Magma.java
@@ -1,5 +1,6 @@
 package com.github.vincentk.dedekind.algebra.structures;
 
+import com.github.vincentk.dedekind.sets.Element;
 import com.github.vincentk.dedekind.sets.Set;
 import com.github.vincentk.dedekind.sets.binary.function.arithmetic.Addition;
 import com.github.vincentk.dedekind.sets.binary.function.arithmetic.Multiplication;
@@ -23,7 +24,7 @@ public interface Magma<
 {
     interface Oe<E extends Oe<E>>
     extends
-    Set.Element<E>,
+    Element<E>,
     BinaryOperation<E, E>
     {
     }

diff --git a/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/algebra/structures/Ring.java b/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/algebra/structures/Ring.java
@@ -27,6 +27,7 @@ interface Re<R extends Re<R>>
 	 * @param that
 	 * @return this - that
 	 */
+	@Override
 	default R minus(R that) {
 	    return plus(that.negate());
 	}

diff --git a/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/families/Enumeration.java b/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/families/Enumeration.java
@@ -2,12 +2,12 @@
 
 import java.util.Optional;
 
-import com.github.vincentk.dedekind.sets.Set;
+import com.github.vincentk.dedekind.sets.Element;
 
 @FunctionalInterface
 public interface Enumeration<
-T extends Set.Element<T>,
-E extends Enumeration<T, E> & Set.Element<E>
+T extends Element<T>,
+E extends Enumeration<T, E> & Element<E>
 >
 {
     /**

diff --git a/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/families/Family.java b/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/families/Family.java
@@ -1,6 +1,7 @@
 package com.github.vincentk.dedekind.families;
 
 import com.github.vincentk.dedekind.sets.Cardinality;
+import com.github.vincentk.dedekind.sets.Element;
 import com.github.vincentk.dedekind.sets.Set;
 
 /**
@@ -9,10 +10,10 @@
 @FunctionalInterface
 public interface Family<
 // Range:
-R extends Set.Element<R>,
+R extends Element<R>,
 C extends Cardinality,
 // Domain and its elements:
-E extends Set.Element<E>,
+E extends Element<E>,
 D extends Set<E, D>
 >
 {

diff --git a/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/families/Pair.java b/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/families/Pair.java
@@ -1,20 +1,20 @@
 package com.github.vincentk.dedekind.families;
 
-import com.github.vincentk.dedekind.sets.Set;
+import com.github.vincentk.dedekind.sets.Element;
 
 /**
  * @see https://en.wikipedia.org/wiki/Ordered_pair
  * @see https://en.wikipedia.org/wiki/Cartesian_product
  */
 public interface Pair<
 // Domain:
-A extends Set.Element<A>,
+A extends Element<A>,
 // Range:
-B extends Set.Element<B>,
+B extends Element<B>,
 // Implementation type:
 P extends Pair<A, B, P>>
 extends
-Set.Element<P>
+Element<P>
 {
     A fst();
     B snd();
@@ -25,16 +25,16 @@ default boolean eq(P that) {
     }
 
     interface Homogeneous<
-    E extends Set.Element<E>,
+    E extends Element<E>,
     H extends Homogeneous<E, H>
     >
     extends Pair<E, E, H>
     {}
 
     public record Impl<
-    A extends Set.Element<A>,
+    A extends Element<A>,
     // Range:
-    B extends Set.Element<B>
+    B extends Element<B>
     > 
     (A fst, B snd)
     implements Pair<A, B, Impl<A, B>>

diff --git a/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/families/Sequence.java b/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/families/Sequence.java
@@ -3,23 +3,48 @@
  */
 package com.github.vincentk.dedekind.families;
 
+import com.github.vincentk.dedekind.algebra.structures.Magma;
 import com.github.vincentk.dedekind.sets.Cardinality;
-import com.github.vincentk.dedekind.sets.Set;
-import com.github.vincentk.dedekind.sets.ordered.Interval;
+import com.github.vincentk.dedekind.sets.Element;
+import com.github.vincentk.dedekind.sets.ordered.ConvexSet;
 import com.github.vincentk.dedekind.sets.ordered.TotallyOrdered;
 
 /**
  * @see https://en.wikipedia.org/wiki/Sequence#Definition
+ * @see https://en.wikipedia.org/wiki/Stream_(computing)
  */
-@FunctionalInterface
 public interface Sequence<
-R extends Set.Element<R>,
+R extends Element<R>,
 C extends Cardinality.Countable,
 
 E extends TotallyOrdered.Oe<E>,
 D extends TotallyOrdered<E, C, D>,
-I extends Interval<E, D, D, C, I>
+I extends ConvexSet.HalfOpen.Right<E, D, C, I>
 >
 extends Family<R, C, E, I>
 {
+    I interval();
+
+    /**
+     * @param <R>
+     * @param <C>
+     * @param <E>
+     * @param <D>
+     * @param <I>
+     * 
+     * @see https://en.wikipedia.org/wiki/Sequence#Finite_and_infinite
+     * @see https://en.wikipedia.org/wiki/List_(abstract_data_type)
+     */
+    interface Finite<
+    R extends Element<R>,
+    C extends Cardinality.Finite,
+
+    E extends TotallyOrdered.Oe<E> & Magma.Oe<E>,
+    D extends TotallyOrdered<E, C, D>,
+    I extends ConvexSet.Closed<E, D, C, I>
+    >
+    extends Sequence<R, C, E, D, I>{
+
+	E length();
+    }
 }
diff --git a/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/families/Tuple.java b/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/families/Tuple.java
@@ -3,7 +3,7 @@
 import com.github.vincentk.dedekind.algebra.sets.SemiRings;
 import com.github.vincentk.dedekind.algebra.structures.Magma;
 import com.github.vincentk.dedekind.sets.Cardinality;
-import com.github.vincentk.dedekind.sets.ordered.Interval;
+import com.github.vincentk.dedekind.sets.ordered.ConvexSet;
 import com.github.vincentk.dedekind.sets.ordered.TotallyOrdered;
 
 /**
@@ -18,15 +18,14 @@ public interface Tuple<
 C extends Cardinality.Finite,
 
 // Declaration of domain elements and the domain:
-E extends SemiRings.Naturals & TotallyOrdered.Oe<E>,
+E extends SemiRings.Naturals & TotallyOrdered.Oe<E> & Magma.Oe<E>,
 D extends TotallyOrdered<E, C, D>,
-I extends Interval.Bounded<E, D, D, C, I>,
+I extends ConvexSet.Closed<E, D, C, I>,
 
 // Self-reference to the implementation type:
 T extends Tuple<M, C, E, D, I, T>
 >
 extends
-Sequence<E, C, E, D, I>
+Sequence.Finite<E, C, E, D, I>
 {
-    int length();
 }
diff --git a/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/geometry/ConnectedSpace.java b/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/geometry/ConnectedSpace.java
@@ -0,0 +1,16 @@
+package com.github.vincentk.dedekind.geometry;
+
+/**
+ * @param <E> typically something like the real numbers.
+ * @param <M>
+ * 
+ * @see https://en.wikipedia.org/wiki/Connected_space#Formal_definition
+ */
+public interface ConnectedSpace<
+E extends TopologicalSpace.Me<E>,
+M extends ConnectedSpace<E, M>
+>
+extends
+TopologicalSpace<E, M>
+{
+}
diff --git a/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/geometry/MetricSpace.java b/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/geometry/MetricSpace.java
@@ -12,7 +12,7 @@
  * @param <T> often equal to {@link M}.
  */
 public interface MetricSpace<
-T extends Magma.M.Me<T>,
+T extends Magma.Oe<T>,
 E extends MetricSpace.Me<T, E>,
 M extends MetricSpace<T, E, M>
 >
@@ -21,7 +21,7 @@ public interface MetricSpace<
 {
 
     interface Me<
-    T extends Magma.M.Me<T>,
+    T extends Magma.Oe<T>,
     E extends Me<T, E>
     >
     extends
@@ -51,6 +51,7 @@ interface MeG<
 	 * @param other
 	 * @return the distance from this element to the argument.
 	 */
+	@Override
 	default T distance(E other) {
 	    return minus(other).abs();
 	}

diff --git a/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/geometry/NumberLine.java b/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/geometry/NumberLine.java
@@ -6,12 +6,13 @@
 import com.github.vincentk.dedekind.sets.ordered.TotallyOrdered;
 
 /**
- * A specialization of the {@link MetricSpace} to sets which are {@link TotallyOrdered}.
+ * A specialization of a {@link MetricSpace} to sets which are {@link TotallyOrdered}.
  * 
  * @param <C>
  * @param <T>
  * 
  * @see https://en.wikipedia.org/wiki/Number_line
+ * @see https://en.wikipedia.org/wiki/Interval_(mathematics)#Properties
  */
 public interface NumberLine<
 E extends MetricSpace.Me<E, E> & TotallyOrdered.Oe<E> & SemiRing.SmrE<E>,

diff --git a/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/geometry/TopologicalSpace.java b/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/geometry/TopologicalSpace.java
@@ -1,6 +1,7 @@
 package com.github.vincentk.dedekind.geometry;
 
 
+import com.github.vincentk.dedekind.sets.Element;
 import com.github.vincentk.dedekind.sets.Set;
 
 /**
@@ -20,7 +21,7 @@ interface Me<
     E extends Me<E>
     >
     extends
-    Set.Element<E>
+    Element<E>
     {
     }
 }
diff --git a/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/sets/Countable.java b/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/sets/Countable.java
@@ -1,15 +1,31 @@
 package com.github.vincentk.dedekind.sets;
 
+import com.github.vincentk.dedekind.families.Sequence;
+import com.github.vincentk.dedekind.sets.ordered.TotallyOrdered;
+import com.github.vincentk.dedekind.sets.unary.function.Lambda;
+
 /**
- * A countable set. Its elements can be enumerated.
+ * A {@link Countable} set. Its elements can be enumerated.
  * 
  * @param <C> cardinality
  * @param <T> implementation type
  */
 public interface Countable<
-E extends Set.Element<E>,
+E extends Element<E>,
 C extends Cardinality.Countable,
 T extends Countable<E, C, T>
 >
-extends Set<E, T> {
+extends
+Set<E, T>
+{
+    /**
+     * 
+     * @param <N> natural numbers
+     * @param enumeration
+     * @return
+     * 
+     * @see https://en.wikipedia.org/wiki/Enumeration#Set_theory
+     */
+    <N extends TotallyOrdered.Oe<N>>
+    Sequence<E, C, N, ?, ?> enumerate(Lambda<N, E, ?> enumeration);
 }
diff --git a/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/sets/Element.java b/dedekind-ontology/src/main/java/com/github/vincentk/dedekind/sets/Element.java
@@ -0,0 +1,23 @@
+package com.github.vincentk.dedekind.sets;
+
+import com.github.vincentk.dedekind.sets.binary.relation.homogeneous.Identity;
+
+/**
+ * An {@link Element} of a {@link Set}.
+ * 
+ * @see https://en.wikipedia.org/wiki/Element_(mathematics)
+ */
+public interface Element<E extends Element<E>>
+extends Identity<E>
+{
+    @SuppressWarnings("unchecked")
+    @Override
+    default boolean eq(E that) {
+	return ((E) this).equals(that);
+    }
+
+    @SuppressWarnings("unchecked")
+    default boolean isin(Set<E, ?> set) {
+	return set.contains((E) this);
+    }
+}