Benutzer:Daniel5Ko/Zeug

Bookmarks

... Browser- und Arbeitsplatz- unabhängig.

Foo

Konstruktives und ge-curry-tes $\lnot (\phi \leftrightarrow \lnot \phi )$ :

{\begin{aligned}&q\colon ((\phi \to \bot )\to \phi )\to (\phi \to \phi \to \bot )\to \bot \\&qfg:=h(fh){\text{ mit}}\\&\,\ h\colon \phi \to \bot \\&\,\ hx:=gxx\end{aligned}}

Domains

Scott-Topologie einer DCPO

$(D,\leq )$ eine DCPO. (Suprema von gerichteten Teilmengen)
$U\subseteq D$ heißt Scott-offen, wenn
- $U$ Oberhalbmenge, also $x\leq y\Rightarrow (x\in U\Rightarrow y\in U)$ ,
- für alle gerichteten Mengen $S\subseteq D$ gilt $\textstyle \bigvee _{D}S\in U\Rightarrow S\cap U\neq \emptyset$ .

Spezialisierungsordnung eines top. Raumes

$X$ topologischer Raum mit offenen Mengen ${\mathcal {O}}X$ .
Für Punkte $p\in X$ und Mengen $V\subseteq X$ Notation für Umgebungsrelation: $p\prec V:\Longleftrightarrow \exists U\in {\mathcal {O}}X.\ p\in U\subseteq V$
Auf Punktmenge von $X$ definiere die Spezialisierungsordnung durch $x\sqsubseteq y:\Longleftrightarrow \forall V\subseteq X.\ x\prec V\Rightarrow y\prec V$
- $\sqsubseteq$ offensichtlich reflexiv, transitiv.
- ( $T_{0}$ -Axiom fordert: $\sqsubseteq$ ist außerdem antisymmetrisch,
- ( $T_{1}$ -Axiom fordert: $\sqsubseteq$ ist außerdem antisymmetrisch und symmetrisch.)

Hin und zurück

Ist $(D,\leq )$ eine DCPO, dann ist die Spezialisierungsordnung $\sqsubseteq$ von D-mit-Scott-Topologie wieder $\leq$ .

Ein Satz Definitionen

Im folgenden immer $(D,\leq )$ eine DCPO.
Way-below: ${\ll }\subseteq D^{2}$ , $x\ll y$ falls für alle gerichteten $S\subseteq D$ gilt, $y\leq \bigvee S\Rightarrow \exists s\in S.\ x\leq s$ .
Stetige DCPO: $\{x\mid x\ll y\}$ ist gerichtet, und $\bigvee \{x\mid x\ll y\}=y$ .
Stetige Scott-Domain: Stetige DCPO, $\bigwedge X$ ex. für alle nichtleeren $X\subseteq D$ .
Stetiger Verband: Vollständiger Verband, der stetige DCPO ist. (Oder auch: stetige DCPO, $\bigvee X$ ex. für alle endlichen $X\subseteq D$ ).
Algebraische DCPO: alle $x\in D$ sind darstellbar als ein $\bigvee B$ , wobei für alle $b\in B$ gilt $b\ll b$ und $b\leq x$ . (Algebraische DCPOs sind stetig).
Scott-Domain: Stetige Scott-Domain, die algebraische DCPO ist.

Test

Lawvere-FP

In einer kart. abgeschl. Kat....

Def.: $f\colon X\to Z^{Y}$ heißt schwach punktsurjektiv, wenn für alle $g\colon Y\to Z$ ex. ein $x\colon 1\to X$ , sodass für alle $y\colon 1\to Y$
$\operatorname {ev} \langle fx,y\rangle =gy$ .
Def.: $Z$ hat Fixpunkteigenschaft, wenn für alle $t\colon Z\to Z$ ein $z\colon 1\to Z$ , sodass
$z=tz$ .
Satz: Gibt's ein Objekt $Y$ und ein schwach punktsurjektives $e\colon Y\to Z^{Y}$ , so hat $Z$ die Fixpunkteigenschaft.
Beweis
- Sei $t\colon Z\to Z$ beliebig. Definiere $g\colon Y\to Z$ per $g=t\operatorname {ev} \langle e,\operatorname {id} _{Y}\rangle$
- Sei $x\colon 1\to Y$ jenes mit für alle $y\colon 1\to Y$ : $\operatorname {ev} \langle ex,y\rangle =gy$ .
- Dann ist $\operatorname {ev} \langle ex,x\rangle =gx=t\operatorname {ev} \langle e,\operatorname {id} _{Y}\rangle x=t\operatorname {ev} \langle ex,x\rangle \quad \square$ .
Korollare
- In Set mit $Z=2$ und Kontraposition: Satz von Cantor.
- Und noch paar andere, z.B. in Richtung Bbkeit.

Haskell-Typechecker als Mikro-Proof-Assistant...

{-# LANGUAGE RankNTypes #-}
import Prelude hiding (not)
import Control.Arrow ((&&&))

data Absurd = Absurd { efq :: forall a. a }

type Not a = a -> Absurd
not :: (a -> b) -> Not b -> Not a
not = flip (.)

type Classic a = Not (Not a)
classic :: (a -> b) -> Classic a -> Classic b
classic = not . not

tripleNegElim :: Classic (Not a) -> Not a
tripleNegElim = not eta

eta :: a -> Classic a
eta = flip id

mu :: Classic (Classic a) -> Classic a
mu = tripleNegElim

s :: (a -> b -> c) -> (a -> b) -> (a -> c)
s f g x = (f x) (g x)

excludedMiddle :: Classic (Either (Not a) a)
excludedMiddle = s (not Left) (not Right)

doubleNegElim :: Classic (Classic a -> a)
doubleNegElim = classic disjunctiveSyllogism excludedMiddle

disjunctiveSyllogism :: Either a b -> Not a -> b
disjunctiveSyllogism = foo efq

foo :: (Absurd -> b) -> Either a b -> Not a -> b
foo efb = either (flip $ (.) efb) const

-- Some DeMorgan stuff
forth :: (Not a, Not b) -> Not (Either a b)
forth = uncurry either

back :: Not (Either a b) -> (Not a, Not b)
back = not Left &&& not Right

forth2 :: Not (Not a, Not b) -> Classic (Either a b)
forth2 = not back

back2 :: Classic (Either a b) -> Not (Not a, Not b)
back2 = not forth

Das Supremum der Menge der Postfixpunkte einer monotonen Funktion f ist ein Fixpunkt von f...

{-# LANGUAGE RankNTypes, TypeOperators #-}

tarski :: (forall x y z. (x ≤ y, y ≤ z) -> x ≤ z)
       -> (forall x y. x ≤ y -> f x ≤ f y)
       -> (forall x. x ≤ f x -> x ≤ p)
       -> (forall q. (forall x. x ≤ f x -> x ≤ q) -> p ≤ q)
       -> (f p ≤ p, p ≤ f p)
tarski transitive monotone upperBound least = (pre, post) where
    pre  = upperBound (monotone post)
    post = least $ \h -> transitive (h, monotone (upperBound h))

$(fx\leq a)\Longleftrightarrow (x\sqsubseteq ua)$ impliziert Monotonität von $f$ und $u$ ...

aLemma :: (forall x. x ≤ x)
       -> (forall x y z. x ≤ y -> y ≤ z -> x ≤ z)
       -> (forall a. a ⊑ a)
       -> (forall a b c. a ⊑ b -> b ⊑ c -> a ⊑ c)
       -> (forall a x. f x ⊑ a -> x ≤ u a)
       -> (forall a x. x ≤ u a -> f x ⊑ a)
       -> (forall x y. x ≤ y -> f x ⊑ f y, forall a b. a ⊑ b -> u a ≤ u b)
aLemma reflX transX reflA transA phi psi = (foo, bar) where
	foo p = psi(p `transX` phi reflA)
	bar p = phi(psi reflX `transA` p)

Diagramme

2-Zellen

${\begin{matrix}{\mathcal {C}}&{\xrightarrow {\quad \operatorname {Id} \quad }}&\!{\mathcal {C}}&{\xrightarrow {\quad \operatorname {Id} \quad }}&\!{\mathcal {C}}\\\!\!\!F{\Bigg \downarrow }&\Downarrow \eta &\ {\Bigg \uparrow }G&\Downarrow \varepsilon &\ {\Bigg \downarrow }F\\{\mathcal {D}}&{\xrightarrow {\quad \operatorname {Id} \quad }}&\!{\mathcal {D}}&{\xrightarrow {\quad \operatorname {Id} \quad }}&\!{\mathcal {D}}\end{matrix}}$

2 Adjunktionen

${\begin{array}{c}{\mathcal {O}}X\\U'{\Big \downarrow }\!{\dashv }\!{\Big \uparrow }\mathrm {int} \\{\mathcal {P}}X\\\mathrm {cl} {\Big \downarrow }\!{\dashv }\!{\Big \uparrow }U\\{\mathcal {C}}X\end{array}}$

Noch eins.

${\begin{array}{rcccl}1&{\xrightarrow {\ulcorner h\urcorner }}&N&{\xrightarrow {\ h\ }}&X\\\ulcorner h\urcorner {\Big \downarrow }&&\!\Delta {\Big \downarrow }&&{\Big \downarrow }\operatorname {id} \\N&&N^{2}&&X\\h{\Big \downarrow }&&e{\Big \downarrow }&&{\Big \downarrow }\operatorname {id} \\X&{\xrightarrow[{\ \operatorname {id} \ }]{}}&X&{\xrightarrow[{\ g\ }]{}}&X\end{array}}$

Bidirektionale ND-Regel u.ä.

${\begin{array}{c}X\times S\to Y\\\hline \hline X\to Y^{S}\end{array}}(\operatorname {curry} )$

Tabelle

Kat	Ord, a.k.a. Hälfte weggeworfen.
Kategorie ${\mathcal {C}}$	Menge $C$ mit Quasiordnung $\leq$
Objekt	Element
Morphismus	$\leq$ -"Zeuge" -- mit proof-irrelevance
Funktor ${\mathcal {C}}\to {\mathcal {D}}$	monotone Funktion $C\to D$
nat. Trans $F\to G$ , jeweils ${\mathcal {C}}\to {\mathcal {D}}$	Zeuge für $F\leq _{D^{C}}G:\Longleftrightarrow \forall x\in C.\ Fx\leq _{D}Gx$
Funktorkategorie ${\mathcal {D}}^{\mathcal {C}}$	Elemente: mon. Funktionen $C\to D$ , Ordnung: $\leq _{D^{C}}$
Monade	Hüllen-Op; d.h. $T\colon C\to C$ monoton, $\eta :\operatorname {id} _{C}\leq _{C^{C}}T$ , $\mu \colon T^{2}\leq _{C^{C}}T$
Set	$\Sigma :=\{0\leq 1\}$ scheint für die Zwecke hier zu reichen.
Hom-Funktor	$C(-,-)\colon C^{\text{op}}\times C\to \Sigma ;C(x,y):={\begin{cases}1&x\leq _{C}y\\0&{\text{sonst}}\end{cases}}$
Yoneda-Lemma	$F\colon C\to \Sigma$ monoton, $x\in C$ . Dann: $Fx=\Sigma ^{C}(C(x,-),F)$

Damit zum Beispiel $|\Sigma ^{\Sigma ^{0}}|=2,|\Sigma ^{\Sigma ^{1}}|=3,|\Sigma ^{\Sigma ^{2}}|=6,|\Sigma ^{\Sigma ^{3}}|=20,|\Sigma ^{\Sigma ^{4}}|=168$ (Siehe auch en:Dedekind number) und
$|\Sigma |=2,|\Sigma ^{\Sigma }|=3,|\Sigma ^{\Sigma ^{\Sigma }}|=4,|\Sigma ^{\Sigma ^{\Sigma ^{\Sigma }}}|=5$ usw.

Baz

$\bullet \colon \forall A,B,C\in {\mathcal {C}}.\ {\mathcal {C}}(B,TC)\times {\mathcal {C}}(A,TB)\to {\mathcal {C}}(A,TC)$ ,
$f\circ (g\circ h)=(f\circ g)\circ h,\mathrm {id} \circ f=f=f\circ \mathrm {id}$ ,
$f\bullet (g\bullet h)=(f\bullet g)\bullet h,\eta \bullet f=f=f\bullet \eta$ ,
$f\circ g=f\bullet (\eta \circ g)$ , (und damit auch $(f\bullet g)\circ h=f\bullet (g\circ h)$ ).

$Tf:=(\eta \circ f)\bullet \mathrm {id}$ ,
$\mu :=\mathrm {id} \bullet \mathrm {id}$ .

$Tf\circ \eta =((\eta \circ f)\bullet \mathrm {id} )\circ \eta =\eta \circ f$ ,
$T\mathrm {id} =(\eta \circ \mathrm {id} )\bullet \mathrm {id} =\eta \bullet \mathrm {id} =\mathrm {id}$ ,
$T(f\circ g)=(\eta \circ f\circ g)\bullet \mathrm {id} =(Tf\circ \eta \circ g)\bullet \mathrm {id} =(\eta \circ f)\bullet (\eta \circ g)\bullet \mathrm {id} =((\eta \circ f)\bullet \mathrm {id} )\circ ((\eta \circ g)\bullet \mathrm {id} )=Tf\circ Tg,$
( $\mu \circ Tf=(\mathrm {id} \bullet \mathrm {id} )\circ ((\eta \circ f)\bullet \mathrm {id} )=\mathrm {id} \bullet (\eta \circ f)\bullet \mathrm {id} =f\bullet \mathrm {id}$ )
$\mu \circ T^{2}f=Tf\bullet \mathrm {id} =(\eta \circ f)\bullet \mathrm {id} \bullet \mathrm {id} =((\eta \circ f)\bullet \mathrm {id} )\circ (\mathrm {id} \bullet \mathrm {id} )=Tf\circ \mu$ ,
$\mu \circ \eta =(\mathrm {id} \bullet \mathrm {id} )\circ \eta =\mathrm {id}$ ,
$\mu \circ T\eta =\eta \bullet \mathrm {id} =\mathrm {id}$ ,
$\mu \circ T\mu =\mu \bullet \mathrm {id} =\mathrm {id} \bullet \mathrm {id} \bullet \mathrm {id} =(\mathrm {id} \bullet \mathrm {id} )\circ (\mathrm {id} \bullet \mathrm {id} )=\mu \circ \mu$ .

ohne mathpartir

${\begin{array}{c}{\begin{array}{c}\Gamma \vdash M\colon \Pi x\colon A.\ B\\\hline \Gamma ,x\colon A\vdash M\colon \Pi x\colon A.\ B\end{array}}\ ({\text{Weak}})\qquad {\begin{array}{c}~\\\hline \Gamma ,x\colon A\vdash x\colon A\end{array}}\ ({\text{Ax}})\\\hline {\begin{array}{c}\Gamma ,x\colon A\vdash Mx\colon B\\\hline \Gamma \vdash (\lambda x\colon A.\ Mx)\colon \Pi x\colon A.\ B\end{array}}\ (\Pi {\text{-Intro}})\end{array}}\ (\Pi {\text{-Elim}})$

Merke:

texvc kann Kapitälchen nicht, jedenfalls nicht mit \textsc

Beschriftungs-Hack 🤔

${\begin{array}{c}{\begin{array}{c}{\begin{array}{c}\\\hline A\vdash A\\\hline \vdash \lnot A,A\\\hline \lnot \lnot A\vdash A\end{array}}{\begin{array}{c}{\text{Ax.}}\\\lnot {\text{R}}\\\lnot {\text{L}}\end{array}}\quad {\begin{array}{c}\\\\\\A\vdash B\end{array}}\end{array}}\\\hline \lnot \lnot A\vdash B\end{array}}{\begin{array}{c}\\\\\\{\text{cut}}\end{array}}$

Fazit: Kann man wohl immer noch nehmen. Zumindest, was die Optik angeht.