-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathmath1.py
More file actions
1724 lines (1306 loc) · 59.8 KB
/
math1.py
File metadata and controls
1724 lines (1306 loc) · 59.8 KB
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
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
from typing import Union
import pyirk as p
# noinspection PyUnresolvedReferences
from ipydex import IPS, activate_ips_on_exception # noqa
ag = p.irkloader.load_mod_from_path("./agents1.py", prefix="ag")
__URI__ = "irk:/ocse/0.2/math"
keymanager = p.KeyManager()
p.register_mod(__URI__, keymanager)
p.start_mod(__URI__)
# data store on module level
ds = {}
I5000 = p.create_item(
R1__has_label="scalar zero",
R2__has_description="entity representing the zero-element in the set of complex numbers and its subsets",
R4__is_instance_of=p.I38["non-negative integer"],
R24__has_LaTeX_string="$0$",
)
I5001 = p.create_item(
R1__has_label="scalar one",
R2__has_description="entity representing the one-element in the set of complex numbers and its subsets",
R4__is_instance_of=p.I39["positive integer"],
R24__has_LaTeX_string="$1$",
)
I4895 = p.create_item(
R1__has_label="mathematical operator",
R2__has_description="general (unspecified) mathematical operator",
R3__is_subclass_of=p.I12["mathematical object"],
)
# make all instances of operators callable:
I4895["mathematical operator"].add_method(p.create_evaluated_mapping, "_custom_call")
I9904 = p.create_item(
R1__has_label="matrix",
R2__has_description="matrix of (in general) complex numbers, i.e. matrix over the field of complex numbers",
R3__is_subclass_of=p.I18["mathematical expression"],
)
I7151 = p.create_item(
R1__has_label="vector",
R2__has_description="vector of (in general) complex numbers, i.e. vector over the field of complex numbers",
R3__is_subclass_of=p.I18["mathematical expression"],
)
I3240 = p.create_item(
R1__has_label="matrix element",
R2__has_description=(
"mathematical operation wich maps a Matrix A, and two integers i, j to the scalar matrix entry A[i, j]. "
"Index counting starts at 1"
),
R4__is_instance_of=I4895["mathematical operator"],
R8__has_domain_of_argument_1=I9904["matrix"],
R9__has_domain_of_argument_2=p.I39["positive integer"],
R10__has_domain_of_argument_3=p.I39["positive integer"],
R11__has_range_of_result=p.I34["complex number"],
R13__has_canonical_symbol=r"$\mathrm{elt}$",
R18__has_usage_hint=(
"This operator is assumed be used as callable , e.g. `A_3_6 = I3240['matrix element'](A, 3, 6)`"
),
)
I3240["matrix element"].add_method(p.create_evaluated_mapping, "_custom_call")
I9192 = p.create_item(
R1__has_label="matrix property",
R2__has_description="property of a matrix",
R3__is_subclass_of=p.I54["mathematical property"],
)
# currently we do not need this (we attach start, stop, step to the range-element directly)
I1195 = p.create_item(
R1__has_label="integer range",
R2__has_description="represents an integer range with start-, stop- and step-value",
R4__is_instance_of=p.I2["Metaclass"],
)
R1616 = p.create_relation(
R1__has_label="has start value",
R2__has_description="...",
R8__has_domain_of_argument_1=I1195["integer range"],
R11__has_range_of_result=p.I37["integer number"],
R22__is_functional=True,
)
R1617 = p.create_relation(
R1__has_label="has stop value",
R2__has_description="...",
R8__has_domain_of_argument_1=I1195["integer range"],
R11__has_range_of_result=p.I37["integer number"],
R22__is_functional=True,
)
R1618 = p.create_relation(
R1__has_label="has step value",
R2__has_description="...",
R8__has_domain_of_argument_1=I1195["integer range"],
R11__has_range_of_result=p.I37["integer number"],
R22__is_functional=True,
)
# TODO: this is probably obsolete
def Range(start, stop, step=1, r1: str = None, r2: str = None):
range_item = p.instance_of(I1195["integer range"], r1, r2)
range_item.R1616__has_start_value = start
range_item.R1617__has_stop_value = stop
range_item.R1618__has_step_value = step
return range_item
I6012 = p.create_item(
R1__has_label="integer range element",
R2__has_description="class whose instances represent an element from a specified range (I1195)",
R3__is_subclass_of=p.I37["integer number"],
R18__has_usage_hint=(
"Should always have an R3240__has_associated_range relation; "
"should be created via the context manager IntegerRangeElement (see below)"
),
)
R3240 = p.create_relation(
R1__has_label="has associated range",
R2__has_description="...",
R8__has_domain_of_argument_1=I6012["integer range element"],
R11__has_range_of_result=I1195["integer range"],
R22__is_functional=True,
)
class IntegerRangeElement:
"""
Context manager to model that a statement (or more) have an assertive claim for all elements of a sequence.
```
with RangeElement(start=1, end=3) as i:
I456["some item"].R789_has_some_property(i)
```
Has (roughly) the same meaning as
```
I456["some item"].R789_has_some_property(1)
I456["some item"].R789_has_some_property(2)
I456["some item"].R789_has_some_property(3)
```
Note, however, that the defining attributes of RangeElement, i.e. `start`, `stop`, `step` can be also variables.
Behind the sc
"""
def __init__(self, start: Union[int, p.Item], stop: Union[int, p.Item], step: Union[int, p.Item] = 1):
self.start = start
self.stop = stop
self.step = step
# these might serve to provide optional information to the range_element_item
self.r1 = None
self.r2 = None
@staticmethod
def is_positive(i: Union[int, p.Item]) -> bool:
if isinstance(i, int):
return i > 0
else:
return p.is_instance_of(i, p.I39["positive integer"])
@staticmethod
def is_nonnegative(i: Union[int, p.Item]) -> bool:
if isinstance(i, int):
return i >= 0
else:
return p.is_instance_of(i, p.I38["non-negative integer"])
def __enter__(self):
"""
implicitly called in the head of the with statement
:return:
"""
if self.is_positive(self.start) and self.is_positive(self.step):
class_item = p.I39["positive integer"]
elif self.is_nonnegative(self.start) and self.is_nonnegative(self.step):
class_item = p.I38["non-negative integer"]
else:
class_item = p.I37["integer number"]
element = p.instance_of(class_item, self.r1, self.r2)
element.R30__is_secondary_instance_of = I6012["integer range element"]
# run this explicitly in the context of this module (otherwise R1616 etc. is not defined)
with p.uri_context(uri=__URI__):
element.R1616__has_start_value = self.start
element.R1617__has_stop_value = self.stop
element.R1618__has_step_value = self.step
element.finalize()
return element
def __exit__(self, exc_type, exc_val, exc_tb):
# this is the place to handle exceptions
pass
I9905 = p.create_item(
R1__has_label="zero matrix",
R2__has_description="like its superclass but with all entries equal to zero",
R3__is_subclass_of=I9904["matrix"],
)
I9906 = p.create_item(
R1__has_label="square matrix",
R2__has_description="a matrix for which the number of rows and columns are equal",
R3__is_subclass_of=I9904["matrix"],
# TODO: formalize the condition inspired by OWL
)
R5938 = p.create_relation(
R1__has_label="has row number",
R2__has_description="specifies the number of rows of a matrix",
R8__has_domain_of_argument_1=I9904["matrix"],
R11__has_range_of_result=p.I38["non-negative integer"],
R22__is_functional=True,
)
# todo: specifies that this item defines I9905
R5939 = p.create_relation(
R1__has_label="has column number",
R2__has_description="specifies the number of columns of a matrix",
R8__has_domain_of_argument_1=I9904["matrix"],
R11__has_range_of_result=p.I38["non-negative integer"],
R22__is_functional=True,
)
# start definition
I9223 = p.create_item(
R1__has_label="definition of zero matrix",
R2__has_description="the defining statement of what a zero matrix is",
R4__is_instance_of=p.I20["mathematical definition"],
)
with I9223["definition of zero matrix"].scope("setting") as cm:
cm.new_var(M=p.uq_instance_of(I9904["matrix"]))
cm.new_var(nr=p.uq_instance_of(p.I39["positive integer"]))
cm.new_var(nc=p.instance_of(p.I39["positive integer"]))
cm.new_rel(cm.M, R5938["has row number"], cm.nr)
cm.new_rel(cm.M, R5939["has column number"], cm.nc)
with I9223["definition of zero matrix"].scope("premise") as cm:
with IntegerRangeElement(start=1, stop=cm.nr) as i:
with IntegerRangeElement(start=1, stop=cm.nc) as j:
# create an auxiliary variable (not part part of the graph)
M_ij = I3240["matrix element"](cm.M, i, j)
cm.new_equation(lhs=M_ij, rhs=I5000["scalar zero"])
with I9223["definition of zero matrix"].scope("assertion") as cm:
cm.new_rel(cm.M, p.R30["is secondary instance of"], I9905["zero matrix"])
# end definition
# ---------------------------------------------------------------------------------------------------------------------
# start definition
I1608 = p.create_item(
R1__has_label="identity matrix", # TODO: also known as "unit matrix"
R2__has_description="square matrix with only ones at the main diagonal and every other element zero",
R3__is_subclass_of=I9906["square matrix"],
)
I7169 = p.create_item(
R1__has_label="definition of identity matrix",
R2__has_description="the defining statement of what an identity matrix is",
R4__is_instance_of=p.I20["mathematical definition"],
R67__is_definition_of=I1608["identity matrix"],
)
I1608["identity matrix"].set_relation(p.R37["has definition"], I7169["definition of identity matrix"])
with I7169["definition of identity matrix"].scope("setting") as cm:
cm.new_var(M=p.uq_instance_of(I9906["square matrix"]))
cm.new_var(nr=p.uq_instance_of(p.I39["positive integer"]))
cm.new_rel(cm.M, R5938["has row number"], cm.nr)
with I7169["definition of identity matrix"].scope("premise") as cm:
# todo: the running indices should be related to the context cm
# there should be a context stack
with IntegerRangeElement(start=1, stop=cm.nr) as i:
with IntegerRangeElement(start=1, stop=cm.nr) as j:
# create an auxiliary variable (not part part of the graph)
M_ij = I3240["matrix element"](cm.M, i, j)
# Condition in human-readable form:
# In case i != j, the matrix element M_ij must be 0
# In case i == j, the matrix element M_ij must be 1
# These are two implications (as logical statement, with their specific truth table)
# Both implications must be fulfilled for the premise of the definition to be fulfilled
with p.ImplicationStatement() as imp1:
imp1.antecedent_relation(lhs=i, rsgn="!=", rhs=j)
imp1.consequent_relation(lhs=M_ij, rsgn="==", rhs=I5000["scalar zero"])
with p.ImplicationStatement() as imp2:
imp2.antecedent_relation(lhs=i, rsgn="==", rhs=j)
imp2.consequent_relation(lhs=M_ij, rsgn="==", rhs=I5001["scalar one"])
with I7169["definition of identity matrix"].scope("assertion") as cm:
cm.new_rel(cm.M, p.R30["is secondary instance of"], I1608["identity matrix"])
# end definition
# ---------------------------------------------------------------------------------------------------------------------
I8133 = p.create_item(
R1__has_label="field of numbers",
R1__has_label__de="Zahlenkörper",
R2__has_description="general field of numbers; baseclass for the fields of real and complex numbers",
R3__is_subclass_of=p.I13["mathematical set"],
)
# R3033 = p.create_relation(
# R1__has_label="has type of elements",
# R2__has_description=(
# "specifies the item-type of the elements of a mathematical set; "
# "should be a subclass of I12['mathematical object']"
# ),
# R8__has_domain_of_argument_1=p.I13["mathematical set"],
# R11__has_range_of_result=p.I42["mathematical type (metaclass)"],
# )
I5006 = p.create_item(
R1__has_label="imaginary part",
R2__has_description="returns the imaginary part of a complex number",
R4__is_instance_of=I4895["mathematical operator"],
R8__has_domain_of_argument_1=p.I34["complex number"],
R11__has_range_of_result=p.I35["real number"],
)
I5807 = p.create_item(
R1__has_label="sign",
R2__has_description="returns the sign of a real number, i.e. on element of {-1, 0, 1}",
R4__is_instance_of=I4895["mathematical operator"],
R8__has_domain_of_argument_1=p.I35["real number"],
R11__has_range_of_result=p.I37["integer number"],
)
I2738 = p.create_item(
R1__has_label="field of complex numbers",
R2__has_description="field of complex numbers",
R4__is_instance_of=I8133["field of numbers"],
R13__has_canonical_symbol=r"$\mathbb{C}$",
# R3033__has_type_of_elements=p.I34["complex number"],
)
I2739 = p.create_item(
R1__has_label="open left half plane",
R2__has_description="set of all complex numbers with negative real part",
R4__is_instance_of=p.I13["mathematical set"],
R14__is_subset_of=I2738["field of complex numbers"],
)
I1979 = p.create_item(
R1__has_label="definition of open left half plane",
R2__has_description="the defining statement of what I2739['open left half plane'] is",
R4__is_instance_of=p.I20["mathematical definition"],
R67__is_definition_of=I2739["open left half plane"],
)
with I1979["definition of open left half plane"].scope("setting") as cm:
# Let HP be an arbitrary subset of complex numbers
cm.new_var(HP=p.instance_of(p.I13["mathematical set"]))
cm.new_rel(cm.HP, p.R14["is subset of"], I2738["field of complex numbers"])
cm.new_var(z=p.instance_of(p.I34["complex number"]))
# the premise should hold for all elements z of the subset HP
cm.new_rel(cm.z, p.R15["is element of"], cm.HP, qualifiers=p.univ_quant(True))
imag = I5006["imaginary part"]
cm.new_var(y=imag(cm.z))
with I1979["definition of open left half plane"].scope("premise") as cm:
cm.new_math_relation(cm.y, "<", I5000["scalar zero"])
with I1979["definition of open left half plane"].scope("assertion") as cm:
cm.new_rel(cm.HP, p.R47["is same as"], I2739["open left half plane"])
I6259 = p.create_item(
R1__has_label="sequence",
R2__has_description="common (secondary) base class of sequence of mathematical objects",
R3__is_subclass_of=p.I12["mathematical object"],
)
R7490 = p.create_relation(
R1__has_label="has sequence element",
R2__has_description=(
"specifies the item-type of the elements of a mathematical set; "
"should be a subclass of I12['mathematical object']"
),
R8__has_domain_of_argument_1=I6259["sequence"],
R11__has_range_of_result=p.I12["mathematical object"],
)
I3237 = p.create_item(
R1__has_label="column stack",
R2__has_description="sequence of columns of equal length which are stacked horizontally",
R3__is_subclass_of=I9904["matrix"],
R30__is_secondary_instance_of=I6259["sequence"],
R18__has_usage_hint="see unittest in `test_package.Test_01_math.test_c01_column_stack`",
)
I5177 = p.create_item(
R1__has_label="matmul",
R2__has_description=("matrix multiplication operator"),
R4__is_instance_of=I4895["mathematical operator"],
R8__has_domain_of_argument_1=I9904["matrix"],
R9__has_domain_of_argument_2=I9904["matrix"],
R11__has_range_of_result=I9904["matrix"],
)
I1474 = p.create_item(
R1__has_label="matpow",
R2__has_description=("power function for matrices like A**0 = I, A**1 = A, A**2 = A*A"),
R4__is_instance_of=I4895["mathematical operator"],
R8__has_domain_of_argument_1=I9904["matrix"],
R9__has_domain_of_argument_2=p.I38["non-negative integer"],
R11__has_range_of_result=I9904["matrix"],
)
I9493 = p.create_item(
R1__has_label="matadd",
R2__has_description="matrix addition operator",
R4__is_instance_of=I4895["mathematical operator"],
R8__has_domain_of_argument_1=I9904["matrix"],
R9__has_domain_of_argument_2=I9904["matrix"],
R11__has_range_of_result=I9904["matrix"],
)
I1536 = p.create_item(
R1__has_label="matneg",
R2__has_description="negation operator for matrices",
R4__is_instance_of=I4895["mathematical operator"],
R8__has_domain_of_argument_1=I9904["matrix"],
R11__has_range_of_result=I9904["matrix"],
)
I3263 = p.create_item(
R1__has_label="transpose",
R2__has_description="matrix transposition operator",
R4__is_instance_of=I4895["mathematical operator"],
R8__has_domain_of_argument_1=I9904["matrix"],
R11__has_range_of_result=I9904["matrix"],
)
def I3263_cc_pp(self, res: p.Item, *args, **kwargs):
"""
:param self: mapping item (to which this function will be attached)
:param res: result item (instance of I9904["matrix"] (determined by R11__has_range_of_result))
:param args: arg tuple (len 1) with which the mapping is called
"""
assert len(args) == 1
matrix_item, = args
# define uri context to make the reference `R3326__has_dimension` work in other modules
with p.uri_context(uri=__URI__):
n = matrix_item.R5938__has_row_number
m = matrix_item.R5939__has_column_number
if res.R5938__has_row_number is None and m is not None:
res.set_relation(R5938["has row number"], m)
if res.R5939__has_column_number is None and n is not None:
res.set_relation(R5939["has column number"], n)
else:
# this might be the case if the operator res comes from cache
pass
return res
I3263["transpose"].add_method(I3263_cc_pp, "_custom_call_post_process")
# copied from control_theory1:
I5484 = p.create_item(
R1__has_label="finite set of complex numbers",
R2__has_description="...",
R3__is_subclass_of=p.I13["mathematical set"],
)
I1060 = p.create_item(
R1__has_label="general function",
R2__has_description="function that maps from some set (domain) into another (range);",
R3__is_subclass_of=p.I18["mathematical expression"],
R18__has_usage_hint="this is the base class for more specific types of functions",
)
I5094 = p.create_item(
R1__has_label="linear function",
R2__has_description="linear map from some set (domain) into another (range)",
R3__is_subclass_of=I1060["general function"],
)
R9493 = p.create_relation(
R1__has_label="has assigned linear map",
R2__has_description="a matrix is assigned a linear map, that describes the transformation between two vector spaces",
R8__has_domain_of_argument_1=I9904["matrix"],
R11__has_range_of_result=I5094["linear function"],
R22__is_functional=True,
)
I1063 = p.create_item(
R1__has_label="scalar function",
R2__has_description="function that has one (in general complex) number as result",
R3__is_subclass_of=I1060["general function"],
R46__is_secondary_subclass_of=p.I42["scalar mathematical object"],
)
I4237 = p.create_item(
R1__has_label="monovariate rational function",
R2__has_description="...",
R3__is_subclass_of=I1063["scalar function"],
)
I4237["monovariate rational function"].add_method(p.create_evaluated_mapping, "_custom_call")
I6209 = p.create_item(
R1__has_label="scalneg",
R2__has_description="negation operator for scalars",
R4__is_instance_of=I4895["mathematical operator"],
R8__has_domain_of_argument_1=p.I42["scalar mathematical object"],
R11__has_range_of_result=p.I42["scalar mathematical object"],
)
I4239 = p.create_item(
R1__has_label="abstract monovariate polynomial",
R2__has_description=(
"abstract monovariate polynomial (argument might be a complex-valued scalar, a matrix, an operator, etc.)"
),
R3__is_subclass_of=I4237["monovariate rational function"],
)
R1757 = p.create_relation(
R1__has_label="has set of roots",
R2__has_description="set of roots for a monovariate function",
R8__has_domain_of_argument_1=p.I18["mathematical expression"], # todo: this is too broad
R11__has_range_of_result=I5484["finite set of complex numbers"],
)
I1594 = p.create_item(
R1__has_label="Stodolas necessary condition for polynomial coefficients",
R2__has_description=(
"establishes the fact that if all roots of a polynomial are located in the open left half plane, "
"then all coefficients have the same sign."
),
R4__is_instance_of=p.I15["implication proposition"],
# TODO: test this feature (attribute name beginning with prefix) in pyirk.test_core
ag__R6876__is_named_after=ag.I2276["Aurel Stodola"],
)
I9739 = p.create_item(
R1__has_label="finite scalar sequence",
R2__has_description="base class of a finite sequence of (in general) complex numbers; can be indexed",
R3__is_subclass_of=I6259["sequence"],
)
R3668 = p.create_relation(
R1__has_label="has sequence of coefficients",
R2__has_description="object is the enumerated sequence of coefficients of a monovariate polynomial",
R8__has_domain_of_argument_1=I4239["abstract monovariate polynomial"],
R11__has_range_of_result=I9739["finite scalar sequence"],
)
with I1594["Stodolas necessary condition for polynomial coefficients"].scope("setting") as cm:
cm.new_var(p=p.instance_of(I4239["abstract monovariate polynomial"]))
cm.new_var(set_of_roots=p.instance_of(I5484["finite set of complex numbers"]))
cm.new_var(seq_of_coeffs=p.instance_of(I9739["finite scalar sequence"]))
cm.new_var(c1=p.instance_of(p.I35["real number"]))
cm.new_var(c2=p.instance_of(p.I35["real number"]))
cm.new_rel(cm.p, R1757["has set of roots"], cm.set_of_roots)
cm.new_rel(cm.p, R3668["has sequence of coefficients"], cm.seq_of_coeffs)
cm.new_rel(cm.c1, p.R15["is element of"], cm.seq_of_coeffs, qualifiers=p.univ_quant(True))
cm.new_rel(cm.c2, p.R15["is element of"], cm.seq_of_coeffs, qualifiers=p.univ_quant(True))
with I1594["Stodolas necessary condition for polynomial coefficients"].scope("premise") as cm:
cm.new_rel(cm.set_of_roots, p.R14["is subset of"], I2739["open left half plane"])
with I1594["Stodolas necessary condition for polynomial coefficients"].scope("assertion") as cm:
cm.new_math_relation(lhs=I5807["sign"](cm.c1), rsgn="==", rhs=I5807["sign"](cm.c2))
I4240 = p.create_item(
R1__has_label="matrix polynomial",
R2__has_description="monovariate polynomial of quadratic matrices",
R3__is_subclass_of=I4239["abstract monovariate polynomial"],
R8__has_domain_of_argument_1=I9906["square matrix"],
R11__has_range_of_result=I9906["square matrix"],
)
I1935 = p.create_item(
R1__has_label="polynomial matrix",
R2__has_description="matrix whose entries contain (scalar) polynomials",
R3__is_subclass_of=I9904["matrix"],
R50__is_different_from=I4240["matrix polynomial"],
)
I5030 = p.create_item(
R1__has_label="variable",
R2__has_description="symbol which can represent another mathematical object",
R3__is_subclass_of=p.I12["mathematical object"],
)
R8736 = p.create_relation(
R1__has_label="depends polynomially on",
R2__has_description="subject has a polynomial dependency object",
R8__has_domain_of_argument_1=p.I12["mathematical object"],
R11__has_range_of_result=I5030["variable"],
R18__has_usage_hint=("This relation is intentionally not functional to model multivariate polynomial dependency"),
)
# eigenvalues
I6324 = p.create_item(
R1__has_label="canonical first order monic polynomial matrix",
R2__has_description="for a given square matrix A returns the polynomial matrix (s·I - A)",
R4__is_instance_of=I4895["mathematical operator"],
R8__has_domain_of_argument_1=I9906["square matrix"],
R9__has_domain_of_argument_2=I5030["variable"],
R11__has_range_of_result=I1935["polynomial matrix"],
)
def I6324_cc_pp(self, res, *args, **kwargs):
"""
:param self: mapping item (to which this function will be attached)
:param res: instance of I1935["polynomial matrix"] (determined by R11__has_range_of_result)
:param args: arg tuple (<matrix>, <variable>) with which the mapping is called
"""
assert len(args) == 2
matrix, var = args
# check that `var` is an instance of I5030["variable"]
assert ("R4", I5030["variable"]) in p.get_taxonomy_tree(var)
res.set_relation(R8736["depends polynomially on"], var)
return res
I6324["canonical first order monic polynomial matrix"].add_method(I6324_cc_pp, "_custom_call_post_process")
I5359 = p.create_item(
R1__has_label="determinant",
R2__has_description="returns the determinant of a square matrix",
R4__is_instance_of=I4895["mathematical operator"],
R8__has_domain_of_argument_1=I9906["square matrix"],
R11__has_range_of_result=p.I42["scalar mathematical object"],
)
def I5359_cc_pp(self, res, *args, **kwargs):
"""
Function which will be attached as custom-call-post-process-method to I5359["determinant"].
The I5359["determinant"] is an I4895__mathematical_operator. If it is called it creates an instance of
I32__evaluated_mapping. The the `_custom_call_post_process`-method (i.e. this function) of the operator is called.
:param self: determinant operator item (to which this function will be attached)
:param res: instance of I7765["scalar mathematical object"] (determined by R11__has_range_of_result)
:param args: arg tuple (<matrix>) with which the mapping is called
"""
assert len(args) == 1
(matrix,) = args
if poly_vars := matrix.R8736__depends_polynomially_on:
for var in poly_vars:
assert ("R4", I5030["variable"]) in p.get_taxonomy_tree(var)
res.set_relation(R8736["depends polynomially on"], var)
return res
I5359["determinant"].add_method(I5359_cc_pp, "_custom_call_post_process")
I9160 = p.create_item(
R1__has_label="set of eigenvalues of a matrix",
R2__has_description="returns the set of eigenvalues of a matrix",
R4__is_instance_of=I4895["mathematical operator"],
R8__has_domain_of_argument_1=I9906["square matrix"],
R11__has_range_of_result=I5484["finite set of complex numbers"],
)
I1373 = p.create_item(
R1__has_label="definition of set of eigenvalues of a matrix",
R2__has_description="the defining statement of what a zero matrix is",
R4__is_instance_of=p.I20["mathematical definition"],
R67__is_definition_of=I9160["set of eigenvalues of a matrix"],
)
with I1373["definition of set of eigenvalues of a matrix"].scope("setting") as cm:
cm.new_var(A=p.instance_of(I9906["square matrix"]))
cm.new_var(s=p.instance_of(I5030["variable"]))
cm.new_var(r=p.instance_of(I5484["finite set of complex numbers"]))
# auxiliary variables
M = I6324["canonical first order monic polynomial matrix"](cm.A, cm.s)
# TODO: __automate_typing__
M.R30__is_secondary_instance_of = I9906["square matrix"]
d = I5359["determinant"](M)
with I1373["definition of set of eigenvalues of a matrix"].scope("premise") as cm:
cm.new_rel(d, R1757["has set of roots"], cm.r)
with I1373["definition of set of eigenvalues of a matrix"].scope("assertion") as cm:
cm.new_equation(I9160["set of eigenvalues of a matrix"](cm.A), cm.r)
# TODO: relate/unify this with R3668__has_sequence_of_coefficients
I3058 = p.create_item(
R1__has_label="coefficients of characteristic polynomial",
R2__has_description="...",
R4__is_instance_of=I4895["mathematical operator"],
R8__has_domain_of_argument_1=I9906["square matrix"],
R11__has_range_of_result=I9739["finite scalar sequence"],
)
# the following theorem demonstrate the usage of the existential quantifier ∃ (expressed as qualifiers)
# see also https://pyirk-core.readthedocs.io/en/develop/userdoc/overview.html#universal-and-existential-quantification
# TODO: drop branch name in above link, once the docs are in main
I1566 = p.create_item(
R1__has_label="theorem on the successor of integer numbers",
R2__has_description=(
"establishes the fact that for every integer x there exists another integer y which is bigger."
),
R4__is_instance_of=p.I15["implication proposition"],
)
with I1566["theorem on the successor of integer numbers"].scope("setting") as cm:
cm.new_var(x=p.uq_instance_of(p.I37["integer number"]))
with I1566["theorem on the successor of integer numbers"].scope("premise") as cm:
# no further condition apart from the setting
pass
with I1566["theorem on the successor of integer numbers"].scope("assertion") as cm:
# technical note: the qualifier is passed to `instance_of()`, not to `new_var`
cm.new_var(y=p.instance_of(p.I37["integer number"], qualifiers=[p.exis_quant(True)]))
cm.new_math_relation(cm.y, ">", cm.x)
# preparation for next theorem
R5940 = p.create_relation(
R1__has_label="has characteristic polynomial",
R2__has_description="specifies the characteristic polynomial of a square matrix A, i.e. det(s·I-A)",
R8__has_domain_of_argument_1=I9906["square matrix"],
R11__has_range_of_result=I4239["abstract monovariate polynomial"],
)
# <definition>
I9907 = p.create_item(
R1__has_label="definition of square matrix",
R2__has_description="the defining statement of what a square matrix is",
R4__is_instance_of=p.I20["mathematical definition"],
)
with I9907.scope("setting") as cm:
cm.new_var(M=p.uq_instance_of(I9904["matrix"]))
cm.new_var(nr=p.uq_instance_of(p.I39["positive integer"]))
cm.new_var(nc=p.instance_of(p.I39["positive integer"]))
cm.new_rel(cm.M, R5938["has row number"], cm.nr)
cm.new_rel(cm.M, R5939["has column number"], cm.nc)
with I9907.scope("premise") as cm:
# number of rows == number of columns
cm.new_equation(lhs=cm.nr, rhs=cm.nc)
with I9907.scope("assertion") as cm:
cm.new_rel(cm.M, p.R30["is secondary instance of"], I9906["square matrix"])
# </definition>
I9906["square matrix"].set_relation(p.R37["has definition"], I9907["definition of square matrix"])
# <theorem>
I3749 = p.create_item(
R1__has_label="Cayley-Hamilton theorem",
R2__has_description="establishes that every square matrix is a root of its own characteristic polynomial",
R4__is_instance_of=p.I15["implication proposition"],
)
# TODO: specify universal quantification for A and n
with I3749["Cayley-Hamilton theorem"].scope("setting") as cm:
cm.new_var(A=p.uq_instance_of(I9906["square matrix"]))
cm.new_var(n=p.uq_instance_of(p.I39["positive integer"]))
cm.new_var(coeffs_cp_A=I3058["coefficients of characteristic polynomial"](cm.A))
cm.new_var(P=p.instance_of(I4240["matrix polynomial"]))
cm.new_var(Z=p.instance_of(I9905["zero matrix"]))
cm.new_rel(cm.A, R5938["has row number"], cm.n)
cm.new_rel(cm.A, R5940["has characteristic polynomial"], cm.P)
cm.new_rel(cm.Z, R5938["has row number"], cm.n)
cm.new_rel(cm.Z, R5939["has column number"], cm.n)
cm.new_rel(cm.Z, p.R24["has LaTeX string"], r"$\mathbf{0}$")
with I3749["Cayley-Hamilton theorem"].scope("assertion") as cm:
cm.new_equation(lhs=cm.P(cm.A), rhs=cm.Z)
# </theorem>
I7559 = p.create_item(
R1__has_label="cardinality",
R2__has_description="returns the cardinality of a set or multiset",
R4__is_instance_of=I4895["mathematical operator"],
R8__has_domain_of_argument_1=p.I13["mathematical set"], # TODO: introduce multiset
R11__has_range_of_result=p.I38["non-negative integer"],
)
I3589 = p.create_item(
R1__has_label="monovariate polynomial degree",
R2__has_description="returns degree of a monovariate polynomial",
R4__is_instance_of=I4895["mathematical operator"],
R8__has_domain_of_argument_1=I4239["abstract monovariate polynomial"],
R11__has_range_of_result=p.I38["non-negative integer"],
)
I9628 = p.create_item(
R1__has_label="theorem on the number of roots of a polynomial",
R2__has_description=(
"establishes the fact that a polynomial of degree n has exactly n roots "
"(counting multiplicities)"
),
R4__is_instance_of=p.I15["implication proposition"],
)
with I9628["theorem on the number of roots of a polynomial"].scope("setting") as cm:
P = cm.new_var(P=p.instance_of(I4239["abstract monovariate polynomial"]))
r = cm.new_var(r=p.instance_of(I5484["finite set of complex numbers"]))
with I9628["theorem on the number of roots of a polynomial"].scope("premise") as cm:
cm.new_rel(P, R1757["has set of roots"], r)
deg = I3589["monovariate polynomial degree"](P)
card = I7559["cardinality"](r)
with I9628["theorem on the number of roots of a polynomial"].scope("assertion") as cm:
cm.new_math_relation(deg, "==", card)
I6709 = p.create_item(
R1__has_label="Lipschitz continuity",
R2__has_description="states that the slope of a function is bounded",
R4__is_instance_of=p.I54["mathematical property"],
ag__R6876__is_named_after=ag.I7906["Rudolf Lipschitz"],
R33__has_corresponding_wikidata_entity="https://www.wikidata.org/wiki/Q652707",
R78__is_applicable_to=I1060["general function"],
)
# imported entities from control_theory1.py:
R3326 = p.create_relation(
R1__has_label="has dimension",
R2__has_description="specifies the dimension of a (dimensional) mathematical object",
R8__has_domain_of_argument_1=p.I12["mathematical object"],
R11__has_range_of_result=p.I38["non-negative integer"],
R22__is_functional=True,
)
# TODO: improve taxonomy here
I5166 = p.create_item(
R1__has_label="vector space",
R2__has_description="type for a vector space",
R3__is_subclass_of=p.I13["mathematical set"],
R33__has_corresponding_wikidata_entity="https://www.wikidata.org/wiki/Q125977",
R41__has_required_instance_relation=R3326["has dimension"],
)
# TODO: consider "state manifold"
I5167 = p.create_item(
R1__has_label="state space",
R2__has_description="type for a state space of a dynamical system (I6886)",
R3__is_subclass_of=I5166["vector space"],
# this should be defined via inheritance from vector space
# TODO: test that this is the case
# R41__has_required_instance_relation=R3326["has dimension"],
)
R5405 = p.create_relation(
R1__has_label="has associated state space",
R2__has_description="specifies the associated state space of the subject (e.g. a I9273__explicit...ode_system)",
R8__has_domain_of_argument_1=p.I12["mathematical object"],
R11__has_range_of_result=I5167["state space"],
R22__is_functional=True,
)
# TODO: it might be worth to generalize this: creating a type from a set (where the set is an instance of another type)
I1169 = p.create_item(
R1__has_label="point in vector space",
R2__has_description="type for a point in a given vector space",
R3__is_subclass_of=p.I12["mathematical object"],
)
I1168 = p.create_item(
R1__has_label="point in state space",
R2__has_description="type for a point in a given state space",
R3__is_subclass_of=I1169["point in vector space"],
R41__has_required_instance_relation=R5405["has associated state space"],
)
R9651 = p.create_relation(
R1__has_label="has domain",
R2__has_description="specifies that the subject (a function or operator) is defined for all values of the object (a set)",
R8__has_domain_of_argument_1=I4895["mathematical operator"],
R11__has_range_of_result=p.I13["mathematical set"],
R22__is_functional=True,
)
R3798 = p.create_relation(
R1__has_label="has origin",
R2__has_description="specifies that the subject (a vector space) has the object as origin",
R8__has_domain_of_argument_1=I5166["vector space"],
R11__has_range_of_result=I1169["point in vector space"],
R22__is_functional=True,
)
I9923 = p.create_item(
R1__has_label="scalar field",
R2__has_description="...",