aboutsummaryrefslogtreecommitdiffstats
path: root/docs/infinite-relations.puml
blob: cd6aa0fc6ca5991dd15cf2ad96a5393a814fd77a (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
@startuml infinite-relations
!theme plain
title Infinite Type Relations: Unfold Pattern & Membership

abstract class InfiniteTypeRelation {
  + name: atom()
  + cardinality: aleph_zero | continuum
  + erlang_type: type()
  + membership_predicate: function()
  + unfold_generator: function()
  + constraints: constraints()
}

class Naturals {
  Erlang Type: integer()
  Membership: natural[X] :-
    erlang:is_integer(X),
    X >= 0.

  Unfold Generator:
  unfold(0, fun(N) -> N + 1 end)
  → 0, 1, 2, 3, ...

  Cardinality: aleph_zero
}

class Integers {
  Erlang Type: integer()
  Membership: integer[X] :-
    erlang:is_integer(X).

  Unfold Generator:
  unfold({0, 1}, fun({N, S}) ->
    case S of
      1 -> {N, -1};
      -1 -> {N+1, 1}
    end
  end)
  → 0, 1, -1, 2, -2, ...

  Cardinality: aleph_zero
}

class Rationals {
  Erlang Type: {integer(), integer()}
  Membership: rational[X] :-
    X is (P, Q),
    integer[P], integer[Q],
    Q ≠ 0.

  Unfold Generator:
  Stern-Brocot tree unfold
  → (0,1), (1,1), (1,2), ...

  Cardinality: aleph_zero
}

class Reals {
  Erlang Type: float()
  Membership: real[X] :-
    erlang:is_float(X).

  Unfold Generator:
  IEEE 754 float enumeration
  (impractical, continuum)

  Cardinality: continuum
}

class Strings {
  Erlang Type: string()
  Membership: string[X] :-
    erlang:is_list(X),
    all_chars(X).

  Unfold Generator:
  Length-ordered, lexicographic
  → "", "a", "b", ..., "aa", ...

  Cardinality: aleph_zero
}

class Plus {
  Erlang Type: {integer(), integer(), integer()}
  Membership: plus[A, B, Sum] :-
    integer[A], integer[B],
    Sum is A + B.

  Unfold Generator:
  Diagonalization of ℤ × ℤ
  → (0,0,0), (0,1,1), (1,0,1), ...

  Cardinality: continuum (ℤ × ℤ)
}

package "Constraint Application" {
  class ConstrainedGenerator {
    Pattern: Apply constraints during unfold
    base_generator: unfold()
    constraints: [constraint()]
    ..
    filter_unfold(Gen, Constraints) ->
      filter(Gen, satisfies_all(Constraints))
  }

  note bottom of ConstrainedGenerator
    **Example 1: Bounded Naturals**
    natural[X], X >= 0, X =< 100
    → Generates: 0, 1, 2, ..., 100 (finite!)

    **Example 2: Constrained Plus**
    plus[5, B, 12]
    → Solves: B = 7
    → Generates: single tuple (5, 7, 12)

    **Example 3: Range Query**
    integer[X], X >= -10, X =< 10
    → Generates: 0, 1, -1, 2, -2, ..., 10, -10
  end note
}

package "Composite Type Relations (Views)" {
  class Complex {
    Type Definition (Karuta):
    complex[X] :-
      X is (A, B),
      real[A], real[B].

    Implementation:
    Unfold real × real with
    product enumeration

    Not primitive: Defined as view
    over primitive real relation
  }
}

InfiniteTypeRelation <|-- Naturals
InfiniteTypeRelation <|-- Integers
InfiniteTypeRelation <|-- Rationals
InfiniteTypeRelation <|-- Reals
InfiniteTypeRelation <|-- Strings
InfiniteTypeRelation <|-- Plus

Naturals --> ConstrainedGenerator: apply\nconstraints
Integers --> ConstrainedGenerator
Rationals --> ConstrainedGenerator
Plus --> ConstrainedGenerator

Reals --> Complex: used in\nproduct
Complex : (view relation)

note right of Naturals
  **Core Pattern:** Infinite relations use unfold
  to generate members. Primitive types are
  infinite relations.

  **Membership:** Erlang type + constraints

  **Unfold Pattern:**
  unfold(Seed, Step) generates infinite sequence:
  Seed, Step(Seed), Step(Step(Seed)), ...

  This enables lazy evaluation and
  constraint-based pruning.
end note

note left of Plus
  **Function Relations:**
  Mathematical functions like plus, multiply, etc.
  are relations with continuum cardinality.

  Membership = evaluation
  Generation = enumeration
end note

@enduml