| |
| Autor |
 Notation der komplexen Zahlen nicht gerechtfertigt |
|
tactac
Senior 
Dabei seit: 15.10.2014
Mitteilungen: 2537
 |  Beitrag No.40, eingetragen 2021-08-28
|
\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]}
\newcommand{\name}[1]{\ulcorner#1\urcorner}
\newcommand{\upamp}{\mathbin {⅋}}\)
Ich meine: Die Elemente von $\IC$ können einfach Paare von reellen Zahlen sein. Und dann kann man sagen, dass die Notation "$x + \mathrm i y$", wenn $x$ und $y$ Terme sind, die für reelle Zahlen stehen, als Bedeutung das Paar $(x,y)$ erhält. Die Aussage aus #38 ist dann trivialerweise wahr.\(\endgroup\)
|
 Profil
|
carlox
Aktiv 
Dabei seit: 22.02.2007
Mitteilungen: 1390
 | Beitrag No.41, vom Themenstarter, eingetragen 2021-08-29
|
\quoteon(2021-08-28 21:16 - tactac in Beitrag No. 40)
Ich meine: Die Elemente von $\IC$ können einfach Paare von reellen Zahlen sein. Und dann kann man sagen, dass die Notation "$x + \mathrm i y$", wenn $x$ und $y$ Terme sind, die für reelle Zahlen stehen, als Bedeutung das Paar $(x,y)$ erhält. Die Aussage aus #38 ist dann trivialerweise wahr.
\quoteoff
1)
"trivialerweise wahr".
Du meinst damit wie man die Notationsfrage rechtfertigen kann?
Man muss eigentlich beweisen, dass die Notation widerspruchsfrei ist.
Wenn man Notationen "ungeschickt" wählt kann man sich Widersprüche einfangen.
Triviales Beispiel:
c = 300000 und
c = 1
ergibt einen Widerspruch.
2)
"Bedeutung"
Ich verstehe, was du anschaulich damit meinst.
Kann man das auch formalisieren ?
mfg
cx
|
Profil
|
tactac
Senior
Dabei seit: 15.10.2014
Mitteilungen: 2537
| Beitrag No.42, eingetragen 2021-09-04
|
\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]}
\newcommand{\name}[1]{\ulcorner#1\urcorner}
\newcommand{\upamp}{\mathbin {⅋}}\)
\quoteon(2021-08-29 08:43 - carlox in Beitrag No. 41)
\quoteon(2021-08-28 21:16 - tactac in Beitrag No. 40)
Ich meine: Die Elemente von $\IC$ können einfach Paare von reellen Zahlen sein. Und dann kann man sagen, dass die Notation "$x + \mathrm i y$", wenn $x$ und $y$ Terme sind, die für reelle Zahlen stehen, als Bedeutung das Paar $(x,y)$ erhält. Die Aussage aus #38 ist dann trivialerweise wahr.
\quoteoff
1)
"trivialerweise wahr".
Du meinst damit wie man die Notationsfrage rechtfertigen kann?
Man muss eigentlich beweisen, dass die Notation widerspruchsfrei ist.
Wenn man Notationen "ungeschickt" wählt kann man sich Widersprüche einfangen.
Triviales Beispiel:
c = 300000 und
c = 1
ergibt einen Widerspruch.
\quoteoff
Klar.
Wobei es in dem Beispiel ja so sein dürfte, dass es entweder von vorn herein als illegal erkannt wird, oder bei der Benutzung der Notation "c" bemerkt wird, dass eine Mehrdeutigkeit vorliegt, oder einfach eine der Definitionen benutzt wird.
\quoteon
2)
"Bedeutung"
Ich verstehe, was du anschaulich damit meinst.
Kann man das auch formalisieren ?
mfg
cx
\quoteoff
Sicherlich. In Coq und Lean zum Beispiel kann man recht komplexe Notationen definieren. Die Dokumentation dieser Mechanismen (oder deren Quellcode) kann man als Formalisierung sehen. Beide legen übrigens keinen großen Wert darauf, alle Arten von Schindluder zu unterbinden.
Und hier mal etwas Lean-Code; da kommt allerdings nicht die in #40 vorgeschlagene Notation vor, aber mehr oder weniger die Aussage aus #0 samt Beweis (foo). Da wird eine implizite Konversion benutzt, und die Möglichkeit dazu durch die has_coe-Typklasseninstanz festgelegt:
\sourceon Lean
import .Ring
structure Complex(R : Type) := mk ::
(re : R)
(im : R)
@[reducible]
def i{R : Type}[Ring R]: Complex R := Complex.mk 0 1
@[reducible]
instance(R : Type)[Ring R]: Ring (Complex R) := {
add := λ p q, Complex.mk (p.re + q.re) (p.im + q.im),
zero := Complex.mk 0 0,
neg := λ p, Complex.mk (-p.re) (-p.im),
mul := λ p q, Complex.mk (p.re*q.re - p.im*q.im) (p.re*q.im + p.im*q.re),
one := Complex.mk 1 0,
add_zero := λ x, by { cases x, simp },
add_assoc := λ x y z, by { cases x, cases y, cases z, simp },
add_neg := λ x, by { cases x, simp },
add_comm := λ x y, by { cases x, cases y, simp, split; apply Ab.add_comm },
one_mul := λ x, by { cases x, simp },
mul_one := λ x, by { cases x, simp },
mul_assoc := λ x y z, by { cases x, cases y, cases z, simp [Ring.mul_assoc], split; ac_refl },
add_mul_distr_l := λ x y z, by { cases x, cases y, cases z, simp, split; ac_refl },
add_mul_distr_r := λ x y z, by { cases x, cases y, cases z, simp, split; ac_refl },
}
@[reducible]
instance(R : Type)[Ring R]: has_coe R (Complex R) := ⟨λ r, Complex.mk r 0⟩
theorem foo(R : Type)[Ring R](x y : R): (⟨x,y⟩: Complex R) = x + i*y :=
begin
simp, split,
calc x = x + -0 : by simp
... = (x:Complex R).re + -(y:Complex R).im : by refl,
calc y = 0 + y : by simp
... = (x:Complex R).im + (y:Complex R).re : by refl
end
\sourceoff
\(\endgroup\)
|
Profil
|
carlox
Aktiv
Dabei seit: 22.02.2007
Mitteilungen: 1390
| Beitrag No.43, vom Themenstarter, eingetragen 2021-09-06
|
Hallo tactac,
\quoteon
In Coq und Lean zum Beispiel kann man recht komplexe Notationen definieren.
\quoteoff
Also könnte man (z.B. in Lean oder Coq) Mengen definieren:
(wobei:
$\{-n \mid n \in \mathbb{N} \} $
$\{\frac{p}{q} \mid p \in \mathbb{Z} \land q \in \mathbb{Z} \setminus \{ 0 \} \} $
$\{x+iy : x,y \in \mathbb{R} \} $
Symbolmengen (Mengen von selbst gebastelten Symbolen) sind.
)
1)
$ \mathbb{Z} = \mathbb{N} \quad \cup \quad \{-n \mid n \in \mathbb{N} \} $
mit
0 = -0
und noch zu definierender Addition auf $ \mathbb{Z} $
2)
$ \mathbb{Q} = \mathbb{Z} \quad \cup \quad \{\frac{p}{q} \mid p \in \mathbb{Z} \land q \in \mathbb{Z} \setminus \{ 0 \} \} $
mit:
$ \frac{p}{1} = p $
$ \frac{0}{p} = 0 $ für $p \neq 0 $
$ \frac{p}{q} = \frac{p \oplus c}{q \oplus c} $ für $q \oplus c \ \neq 0 $ und $ \oplus $ ist Addition auf $ \mathbb{Z} $
und noch zu definierender Addition auf $ \mathbb{Q} $
3)
$ \mathbb{C} = \mathbb{R} \quad \cup \quad i \mathbb{R} \quad \cup \quad \{x+iy : x,y \in \mathbb{R} \} \quad \cup \quad \{i\} $
mit:
x := x + i0
iy := 0 + iy
und noch zu definierender Addition und Multiplikation auf $ \mathbb{C} $
Ist das richtig?
Erlaubt ZFC, daß man diese Mengen bilden kann ?
Wenn das erlaubt ist, verstehe ich nicht warum du schreibst:
\quoteon
Vor allem sollte man auch nicht versuchen, C als Menge von Notationsinstanzen zu definieren.
\quoteoff
mfg
cx
|
Profil
|
tactac
Senior
Dabei seit: 15.10.2014
Mitteilungen: 2537
| Beitrag No.44, eingetragen 2021-09-17
|
\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]}
\newcommand{\name}[1]{\ulcorner#1\urcorner}
\newcommand{\upamp}{\mathbin {⅋}}\)
\quoteon(2021-09-06 14:50 - carlox in Beitrag No. 43)
Hallo tactac,
\quoteon
In Coq und Lean zum Beispiel kann man recht komplexe Notationen definieren.
\quoteoff
Also könnte man (z.B. in Lean oder Coq) Mengen definieren:
(wobei:
$\{-n \mid n \in \mathbb{N} \} $
$\{\frac{p}{q} \mid p \in \mathbb{Z} \land q \in \mathbb{Z} \setminus \{ 0 \} \} $
$\{x+iy : x,y \in \mathbb{R} \} $
Symbolmengen (Mengen von selbst gebastelten Symbolen) sind.
)
1)
$ \mathbb{Z} = \mathbb{N} \quad \cup \quad \{-n \mid n \in \mathbb{N} \} $
mit
0 = -0
und noch zu definierender Addition auf $ \mathbb{Z} $
2)
$ \mathbb{Q} = \mathbb{Z} \quad \cup \quad \{\frac{p}{q} \mid p \in \mathbb{Z} \land q \in \mathbb{Z} \setminus \{ 0 \} \} $
mit:
$ \frac{p}{1} = p $
$ \frac{0}{p} = 0 $ für $p \neq 0 $
$ \frac{p}{q} = \frac{p \oplus c}{q \oplus c} $ für $q \oplus c \ \neq 0 $ und $ \oplus $ ist Addition auf $ \mathbb{Z} $
und noch zu definierender Addition auf $ \mathbb{Q} $
3)
$ \mathbb{C} = \mathbb{R} \quad \cup \quad i \mathbb{R} \quad \cup \quad \{x+iy : x,y \in \mathbb{R} \} \quad \cup \quad \{i\} $
mit:
x := x + i0
iy := 0 + iy
und noch zu definierender Addition und Multiplikation auf $ \mathbb{C} $
Ist das richtig?
Erlaubt ZFC, daß man diese Mengen bilden kann ?
\quoteoff
Wenn man soetwas wie ZFC benutzt, gibt es die Frage, ob man etwas "bilden kann", eigentlich nicht. ZFC gibt Axiome vor, die u.a. behaupten, dass unter gewissen Voraussetzungen irgendwelche Mengen existieren (die dann meist extensional spezifiziert werden).
Aber ich verstehe in etwa, was du meinst, und ja, man kann die angedeuteten Dinge in sowas wie Coq oder Lean nachbauen. Es ist nur in speziell dieser Form (zumindest für $\IC$) recht aufwendig und unsinnig.
\quoteon
Wenn das erlaubt ist, verstehe ich nicht warum du schreibst:
\quoteon
Vor allem sollte man auch nicht versuchen, C als Menge von Notationsinstanzen zu definieren.
\quoteoff
\quoteoff
Eine Orientierung an einer möglichen Semantik ist besser.
Ein notationsorientiertes Vorgehen (so mit "prä"-komplexen Zahlen $R\times R + R + R + 1$ und einer hinterher dafür definierten Äquivalenzrelation, die in einem Setoid der komplexen Zahlen für die Gleichheit stehen soll) ist zwar möglich, bringt aber zu viele Fallunterscheindungen mit sich und anderen Kram. Wenn man das ganze allgemein für $R \to R[i]$ machen will statt nur für $\IR \to \IC$, merkt man zum Beispiel recht schnell, dass allein für eine uniforme Definition der richtigen Äquivalenzrelation auf der Syntax erforderlich ist, dass in beliebigen Ringen entweder $0=1$ oder $0\neq 1$ gilt.
\(\endgroup\)
|
Profil
|
carlox
Aktiv
Dabei seit: 22.02.2007
Mitteilungen: 1390
| Beitrag No.45, vom Themenstarter, eingetragen 2021-09-18
|
\quoteon
In Coq und Lean zum Beispiel kann man recht komplexe Notationen definieren.
\quoteoff
Hallo tactac,
Danke für dein Feedback.
Dein Umgang mit Lean haben mein Interesse geweckt, mich damit mal zu beschäftigen, wenn ich Zeit habe.
Wie lange hast du gebraucht, um mit Lean umzugehen bzw. dies einigermaßen zu erlernen?
Wie lange braucht man als "Normalsterblicher" dazu?
Was meinst du ?
mfg
cx
|
Profil
|
tactac
Senior
Dabei seit: 15.10.2014
Mitteilungen: 2537
| Beitrag No.46, eingetragen 2021-09-18
|
\quoteon(2021-09-18 11:43 - carlox in Beitrag No. 45)
\quoteon
In Coq und Lean zum Beispiel kann man recht komplexe Notationen definieren.
\quoteoff
Hallo tactac,
Danke für dein Feedback.
Dein Umgang mit Lean haben mein Interesse geweckt, mich damit mal zu beschäftigen, wenn ich Zeit habe.
Wie lange hast du gebraucht, um mit Lean umzugehen bzw. dies einigermaßen zu erlernen?
\quoteoff
Viele der Konzepte kannte ich schon von Haskell und Coq. Ich musste also zum Losspielen nur ein neues Vokabular (bzw. Teile davon) und ein paar neue Syntax-Bits lernen. Das ging recht schnell: Tage bis wenige Wochen, bis ich komfortabel damit umgehen konnte. Aber natürlich weiß ich auch nach Jahren nicht „alles“ und lerne immer wieder etwas hinzu.
Die Standardbibliothek und etwa mathlib sollte man wohl auch einigermaßen kennen — das ist aber ein Fass ohne Boden. 😄
\quoteon
Wie lange braucht man als "Normalsterblicher" dazu?
Was meinst du ?
\quoteoff
Auch bei Null beginnend dürfte es nicht viel länger als in paar Wochen dauern, bis man nichttriviale Dinge basteln kann. Natürlich nicht auf einem Niveau, das erfahrene Benutzer davon abhält, die Hände über dem Kopf zusammenzuschlagen und/oder sehr hilfreiche Tipps zu geben, wenn sie deinen Code lesen.
|
Profil
|
| carlox hat die Antworten auf ihre/seine Frage gesehen. | | carlox wird per Mail über neue Antworten informiert. | | Seite 2 | Gehe zur Seite: 1 | 2 |
|
All logos and trademarks in this site are property of their respective owner. The comments are property of their posters, all the rest © 2001-2022 by Matroids Matheplanet
This web site was originally made with PHP-Nuke, a former web portal system written in PHP that seems no longer to be maintained nor supported. PHP-Nuke is Free Software released under the GNU/GPL license.
Ich distanziere mich von rechtswidrigen oder anstößigen Inhalten, die sich trotz aufmerksamer Prüfung hinter hier verwendeten Links verbergen mögen.
Lesen Sie die
Nutzungsbedingungen,
die Distanzierung,
die Datenschutzerklärung und das Impressum.
[Seitenanfang]
|
Home / Seite ohne Frame
Wie unterstütze ich den Matheplaneten mit Geld?
