Not logged in. · Lost password · Register

gabriel2029
Member since Nov 2018
49 posts
Subject: Wann = und wann \equiv
Hallo,
muss man bei äquivalenten, aber nicht syntaktisch gleichen Formeln, das LaTeX-Äquivalenz zu \equiv verwenden oder reicht das = aus?

LG Gabriel
Marcel[Inf]
#faui2k15, GTI-Tutor a. D.
Member since Nov 2015
538 posts
\equiv wird afair in GLoIn für logische Äquivalenz genutzt. = wird für syntaktische Gleichheit genutzt, ggf. modulo einer Operation auf der Metaebene. Beispiele:

A -> true \equiv true
B = B
C -> B = C -> B
(A -> true)[A |-> B] = B -> true   // Per Definition der Substitution
(\x. y)[y |-> x] = \z. x  // Aber auf = \w. x. Das ist eine nichttriviale Sache von Substitutionen, um Capture-Avoidance zu vermeiden.

Später in ThProg wird =_{alpha,beta,eta} dafür genutzt auch modulo \alpha, \beta, \eta-Reduktion & -Expansion Gleichheit zu haben. Es wird also bisschen schwammiger.

Allgemein empfiehlt es sich immer über die eigene Nutzung von = nachzudenken. Inwiefern ist 1 + 1 = 2? Unter welchem Formalismus? Wenn f,g: X -> Y zwei Funktionen und \forall x. f(x) = g(x), ist dann f = g? Unter welchem Axiom? (Stichwort "functional extensionality") Inwiefern ist R x R = R^2? Ist das Gleichheit oder nur ein Vektorraumisomorphismus? :)
This post was edited 2 times, last on 2019-12-12, 08:37 by Marcel[Inf].
Close Smaller – Larger + Reply to this post:
Verification code: VeriCode Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Special characters:
Go to forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen