0
# Mathematical Types
1
2
High-precision mathematical types for arbitrary precision arithmetic and ordinal number operations. These types preserve mathematical accuracy and implement Dafny's mathematical semantics in Python.
3
4
## Capabilities
5
6
### Arbitrary Precision Rational Numbers (BigRational)
7
8
Extends Python's Fraction class with Dafny-specific decimal formatting and arithmetic operations. Provides exact rational arithmetic without floating-point precision loss.
9
10
```python { .api }
11
class BigRational(Fraction):
12
def __dafnystr__(self):
13
"""
14
Returns Dafny-specific string representation with decimal formatting.
15
16
Returns:
17
str: Decimal representation or fraction notation for non-decimal rationals
18
"""
19
20
def is_integer(self):
21
"""
22
Tests if the rational number is an integer.
23
24
Returns:
25
bool: True if the rational equals an integer value
26
"""
27
28
def __add__(self, other):
29
"""
30
Addition returning BigRational.
31
32
Parameters:
33
- other: Another BigRational, Fraction, or numeric type
34
35
Returns:
36
BigRational: Sum as a BigRational
37
"""
38
39
def __sub__(self, other):
40
"""
41
Subtraction returning BigRational.
42
43
Parameters:
44
- other: Another BigRational, Fraction, or numeric type
45
46
Returns:
47
BigRational: Difference as a BigRational
48
"""
49
50
def __mul__(self, other):
51
"""
52
Multiplication returning BigRational.
53
54
Parameters:
55
- other: Another BigRational, Fraction, or numeric type
56
57
Returns:
58
BigRational: Product as a BigRational
59
"""
60
61
def __truediv__(self, other):
62
"""
63
Division returning BigRational.
64
65
Parameters:
66
- other: Another BigRational, Fraction, or numeric type
67
68
Returns:
69
BigRational: Quotient as a BigRational
70
"""
71
72
@staticmethod
73
def isolate_factor(f, x):
74
"""
75
Factors out powers of f from x.
76
77
Parameters:
78
- f: Factor to isolate
79
- x: Number to factor
80
81
Returns:
82
tuple: (remaining_factor, exponent)
83
"""
84
85
@staticmethod
86
def divides_a_power_of_10(x):
87
"""
88
Checks if x divides a power of 10 (for decimal representation).
89
90
Parameters:
91
- x: Denominator to check
92
93
Returns:
94
tuple or None: (compensation, shift) if divisible, None otherwise
95
"""
96
```
97
98
#### Usage Examples
99
100
```python
101
from _dafny import BigRational
102
103
# Create rational numbers
104
half = BigRational(1, 2) # 1/2
105
third = BigRational(1, 3) # 1/3
106
decimal_val = BigRational(25, 100) # 0.25
107
108
# Arithmetic operations
109
sum_val = half + third # 5/6
110
product = half * decimal_val # 1/8 = 0.125
111
division = BigRational(7, 3) / BigRational(2, 1) # 7/6
112
113
# String representations
114
print(half.__dafnystr__()) # "0.5"
115
print(third.__dafnystr__()) # "(1.0 / 3.0)" - non-decimal
116
print(decimal_val.__dafnystr__()) # "0.25"
117
118
# Type checking
119
print(BigRational(4, 1).is_integer()) # True
120
print(third.is_integer()) # False
121
122
# Exact arithmetic (no floating-point errors)
123
result = BigRational(1, 10) + BigRational(2, 10) + BigRational(7, 10)
124
print(result == BigRational(1, 1)) # True (exactly 1.0)
125
```
126
127
### Ordinal Numbers (BigOrdinal)
128
129
Operations on ordinal numbers. At runtime, all ordinals are represented as natural numbers, but the class provides the conceptual framework for ordinal arithmetic.
130
131
```python { .api }
132
class BigOrdinal:
133
@staticmethod
134
def is_limit(ord):
135
"""
136
Tests if ordinal is a limit ordinal.
137
138
Parameters:
139
- ord: Ordinal number (represented as int at runtime)
140
141
Returns:
142
bool: True if ord is a limit ordinal (currently: ord == 0)
143
"""
144
145
@staticmethod
146
def is_succ(ord):
147
"""
148
Tests if ordinal is a successor ordinal.
149
150
Parameters:
151
- ord: Ordinal number (represented as int at runtime)
152
153
Returns:
154
bool: True if ord is a successor ordinal (currently: ord > 0)
155
"""
156
157
@staticmethod
158
def offset(ord):
159
"""
160
Returns the offset of the ordinal.
161
162
Parameters:
163
- ord: Ordinal number
164
165
Returns:
166
int: The ordinal value itself (at runtime)
167
"""
168
169
@staticmethod
170
def is_nat(ord):
171
"""
172
Tests if ordinal is a natural number.
173
174
Parameters:
175
- ord: Ordinal number
176
177
Returns:
178
bool: Always True (all ordinals are natural numbers at runtime)
179
"""
180
```
181
182
#### Usage Examples
183
184
```python
185
from _dafny import BigOrdinal
186
187
# Ordinal operations (all ordinals are natural numbers at runtime)
188
ord_zero = 0
189
ord_five = 5
190
191
# Test ordinal properties
192
print(BigOrdinal.is_limit(ord_zero)) # True (0 is limit ordinal)
193
print(BigOrdinal.is_limit(ord_five)) # False
194
195
print(BigOrdinal.is_succ(ord_zero)) # False
196
print(BigOrdinal.is_succ(ord_five)) # True (successor ordinal)
197
198
print(BigOrdinal.offset(ord_five)) # 5
199
print(BigOrdinal.is_nat(ord_five)) # True (always true at runtime)
200
```
201
202
## Character Arithmetic
203
204
Mathematical operations on Unicode characters, treating them as their numeric code point values.
205
206
```python { .api }
207
def plus_char(a, b):
208
"""
209
Adds the Unicode code points of two characters.
210
211
Parameters:
212
- a: str - First character
213
- b: str - Second character
214
215
Returns:
216
str: Character with code point equal to sum of input code points
217
"""
218
219
def minus_char(a, b):
220
"""
221
Subtracts the Unicode code point of second character from first.
222
223
Parameters:
224
- a: str - First character
225
- b: str - Second character
226
227
Returns:
228
str: Character with code point equal to difference of input code points
229
"""
230
```
231
232
### Usage Examples
233
234
```python
235
from _dafny import plus_char, minus_char
236
237
# Character arithmetic
238
result1 = plus_char('A', '\x01') # 'B' (65 + 1 = 66)
239
result2 = minus_char('Z', '\x01') # 'Y' (90 - 1 = 89)
240
241
# Working with numeric offsets
242
offset = plus_char('a', '\x05') # 'f' (97 + 5 = 102)
243
back = minus_char(offset, '\x05') # 'a' (back to original)
244
```
245
246
## Euclidean Division and Modulus
247
248
Mathematical division and modulus operations following Euclidean division rules, ensuring consistent behavior across positive and negative numbers.
249
250
```python { .api }
251
def euclidian_division(a, b):
252
"""
253
Performs Euclidean division.
254
255
Parameters:
256
- a: int - Dividend
257
- b: int - Divisor
258
259
Returns:
260
int: Quotient following Euclidean division rules
261
"""
262
263
def euclidian_modulus(a, b):
264
"""
265
Performs Euclidean modulus operation.
266
267
Parameters:
268
- a: int - Dividend
269
- b: int - Divisor
270
271
Returns:
272
int: Non-negative remainder following Euclidean modulus rules
273
"""
274
```
275
276
### Usage Examples
277
278
```python
279
from _dafny import euclidian_division, euclidian_modulus
280
281
# Euclidean division (consistent with mathematical definition)
282
print(euclidian_division(7, 3)) # 2
283
print(euclidian_division(-7, 3)) # -3
284
print(euclidian_division(7, -3)) # -2
285
print(euclidian_division(-7, -3)) # 3
286
287
# Euclidean modulus (remainder is always non-negative)
288
print(euclidian_modulus(7, 3)) # 1
289
print(euclidian_modulus(-7, 3)) # 2 (not -1)
290
print(euclidian_modulus(7, -3)) # 1
291
print(euclidian_modulus(-7, -3)) # 2
292
293
# Property: a = (euclidian_division(a, b) * b) + euclidian_modulus(a, b)
294
a, b = -7, 3
295
div = euclidian_division(a, b) # -3
296
mod = euclidian_modulus(a, b) # 2
297
print(a == div * b + mod) # True: -7 == (-3 * 3) + 2
298
```