tchncs

Latest articles

This is the local timeline where you can see the latest articles from this instance. You can control the visibility of each of your blogs. New blogs are currently set to unlisted by default. You can change this in each blogs settings.

from Hannes

19.2.2025 Nachdenklich Heute vor einem Jahr war Margret noch bei mir, trotz der Schmerztabletten quälte sie sich herum. Uschi kam schon mittags zu uns und half Margret zur Toilette und wusch ihre Haare, mir tat Margret sehr Leid. Ich verstehe nicht, warum Margret nicht vorher im ersten Krankenhaus operieren können. Das Krankenhaus hatte doch eine Gynäkologieabteilung. Am 21.2. wusste Margret noch nicht, das sie den letzten Tag in unserer Wohnung war, sie ist nicht mehr wiedergekommen, ich musste selbst sehen, wie ich ohne sie auskomme. Neben dem Haushalt, den ich von ab übernehmen musste, hatte ich auch Luna bei mir, dieses war eine Karthäuser Katze. Als Margret nicht mehr wieder kam, suchte sie nach ihr, sie fraß kaum etwas, aber das war dann nur vorübergehend. Abends nahm ich Luna mit ins Bett und schlief bei mir aufs Margrets Bett. Heute schien die Sonne, dabei waren meine Gedanken bei Margret: “Guck mal Margret, die Sonne scheint auf dein Portait, du hattes doch die Sonne so gern gehabt.” Was nützt das Bild an der Wand, wenn man keine Antwort mehr erhält. Uschi kam heute, sie brachte Katzengras und Futter mit. Danach machte sie für uns einen Kaffee fertig. Anschließend fuhren wir zum Futterhaus nach Witten. Es war ein reichliches Angebot für Katzen vorhanden. Danach fuhren wir zur Innenstadt von Witten und gönnten uns ein Mittagessen. Dann war Zeit nach Hause zu fahren. Unterwegs sprachen wir viel über Margret, das sie nicht mehr bei uns ist. Wir hätten uns zu dritt einen schönen Tag machen können. Die Entzündung am großen Zeh ist zurück gegangen und habe keine Schmerzen mehr, sie ist verheilt. Tschüss

 
Weiterlesen...

from forza4galicia

Hablemos... del fediverso

Introducción

En un mundo tan convulso y cambiante como el nuestro, las redes sociales se han convertido en el mentidero preferido de mucha clase de gente lo que ha deteriorado el ambiente de las redes comerciales comerciales (esas en las que las personas que las poblamos somos el producto).

Aunque esas mismas redes hacen ver que son las únicas, esto no es cierto en absoluto. Aparte de que la propia tecnología nos puede brindar otras formas de relacionarnos, desde hace más de un lustro han crecido diversas plataformas que se intercomunican entre sí, y en las cuales (salvo que la cuenta o el servidor completo estén vetados en tu servidor, o por tí mism@) todas ven los artículos o mensajes de todas las otras redes.

Para ello, todas las redes federadas deben compartir un protocolo de comunicación,es decir, deben comunicarse de la misma manera entre ellas...

El protocolo principal de estas redes se llamó, originalmente, StatusNet. Años después, evolucionó y cambió su nombre por el que tiene actualmente: ActivityPub .

Dado que estas plataformas están formadas por una cantidad enorme de servidores (virtualmente ilimitada) y que todas las instancias (que así se llama cada plataforma alojada en un servidor) tienen la posibilidad de verse entre ellas, es decir que era una Federación i estaba formada por una universo de servidores, el nombre para llamar a toda esta miríada de diferentes redes sociales fue obvio: Fediverso.

Es decir, ¿El fediverso en una red social? ¿Un conjunto de ellas? ¿Que es?

Pues podríamos decir que el fediverso es un conjunto de plataformas de red social, dónde cada plataforma esta formada por un conjunto de servidores (de equipos que tienen instalado el sistema que permite poner en el aire a la red social, y dónde este sistema está activo y funcionando.

Y, ¿cuáles son las diferencias de esta red social con otras? digo...¿de este conjunto de plataforma de red social?

Lo primero, es que es descentralizada y federada.

Descentralizada, significa que no dependen de un servidor o estructura centralizada. Por ejemplo, las redes sociales de meta (empresa matriz de facebook, instagram o whatsapp) pueden estar dispersas entre diversos servidores (sistema distribuído) pero, con todo, presentan una interfaz y un funcionamiento como si fuese un sistema único. Es decir, si bien, al ser un sistema distribuído, el procesamiento, el almacenamiento y demás, pueden estar repartidos entre decenas, centenas o miles de ordenadores o equipos semejantes, sin embargo, no se ven diferencias entre el tratamiento de un artículo almacenado en uno de esos equipos informáticos o en otro.

Sin embargo, en un sistema descentralizado, cada equipo informático que da ese servicio (o cada equipo informático virtual -ya explicaremos esto en otro momento-) presenta una instancia diferente de red social.

Pongamos un ejemplo: si un servidor de una de estas plataformas sociales, digamos https://masto.es , tiene unos ciertos usuarios, estos no sólo verán lo que se publica en su servidor, sino de todos los servidores de mastodon y otras redes sociales con el mismo protocolo que usa mastodon (ActivityPub) . De la misma manera, https://social.ferrocarril.net/ (que, como cualquiera se puede imaginar es para personas aficionadas o apasionadas por el mundo del ferrocarril), también podrá hacer lo mismo.

De otra parte, si no te gusta algún contenido, puedes proponer a los administradores de la instancia que la bloqueen o puedes hacer algo tú al respecto (en bastantes instancias). Al menos, en lo que respecta a mastodon, puedes buscar cuentas de una instancia específica, por ejemplo (y recuerda que este nombre de instancia es ficticio): instanciaQueQuieroBloquear.xxx y, mirando en las opciones de cualquier cuenta de esa instancia, buscas en el menú la opción: “Bloquear instancia” y, una vez que le des, ya no te aparecerán más artículos de cuentas que estén alojadas en esa instancia.

De este modo, en una gran proporción de instancias, se han bloqueado instancias de spam, pornográficas, con mensajes de odio, de corte fascista, etnicista (“racista”) o elitista.

Si quisiera hacerme una cuenta en el fediverso, ¿qué he de tener en cuenta previamente?

En este caso, al ser muchas instancias, has de elegir una, pero, para ello, has de tener en cuenta que cada instancia tiene sus propias reglas y puede que algunas no te convenzan, así que cuando intentes el alta, léete bien las reglas para decidir si te convence esa instancia, o ir a otra u otras.

Por otra parte, podrías encontrarte instancias operadas por empresas o instituciones, y otras (probablemente, la mayoría) operadas por particulares. Ten en cuenta, que cada administrador o grupo de administradores puede tener una idea distinta de lo que se permite o no en el servidor y que, sí, en ocasiones puedes ser censurad@ o echad@ de forma tan arbitraria como en las redes sociales comerciales, con varias diferencias notables:

  1. En estas redes, puedes bajarte tu contenido, hacerte la cuenta en otra instancia, y subir ese contenido a esa misma instancia.

  2. Como ya he dicho en el punto número 1, te lleves o no el contenido, puedes irte a otra instancia.

  3. La gente que hayas conocido en esa otra instancia puedes seguirla desde la nueva e, incluso, puedes subir los contactos de la otra instancia y poder tenerlos añadidos desde ese momento sin tener que hacer esa añadidura manualmente.

Teniendo en cuenta, el punto número 1, esto es totalmente diferente de otras redes (tú no podrías subir a instagram el contenido de tu twitter/X, ni a twitter/X el contenido de tu facebook o linkedin. Pero sí puedes subir el contenido de tu mastodon a otro mastodon, o incluso puede que a misskey (no lo he probado nunca, cuando lo pruebe os comento).

¿Cómo hago una cuenta en alguna instancia del fediverso?

Lo ideal sería leer sobre los tipos de instancias que hay, y hacerse varias cuentas (a poder ser, sólo una en cada tipo de instancia). Por ejemplo, una en mastodon, otra es misskey, otra en hubzilla.

Empiezas a usarlas y decides cual te gusta más,

Para ello, hay distintas webs dónde puedes encontrar instancias del fediverso.

Por cierto, puedo hacerme una cuenta en cualquier instancia, ¿no?

Esto es una buena pregunta, y la respuesta es no. En el fediverso, tanto hay instancias públicas (cualquiera se puede hacer una cuenta), instancias de grupos (no se hacen cuentas, únicamente la persona fundadora o creadora de la instancia, o sus administradores, añaden únicamente a la instancia a las personas de su grupo) e, incluso, instancias individuales (las que hace una persona para añadirse al fediverso, que esa persona gestiona y en la que la única cuenta, aparte de la de administración, es la suya persona (es importante separar la cuenta de administración de la que se va a usar para publicar, tanto por organización como para mayor seguridad).

Y, ¿cómo hago una instancia en el fediverso? Continúa, por favor.

Pues lo primero es buscar la instancia.

Si lo que quieres es una instancia únicamente de mastodon, puedes ir aqui:

https://joinmastodon.org/es/servers

Dónde podrás encontrar una lista en castellano de instancias de mastodon. También encontrarás herramientas de búsqueda dónde puedes buscar por idioma, por “región” ( aquí llaman región al continente), o incluso por temática (sí, hay instancias temáticas también, como vimos en el caso de la instancia dedicada al ferrocarril).

Por otra parte, si quieres un directorio de más tipos de instancias, una de las opciones a tener en cuenta sería:

https://fediverse.observer/

Siendo esta una de las opciones más potentes en la búsqueda, puedes buscar por cierto dato en las columnas (por ejemplo, “Yes” en la columna donde dice si está abierta a nuevas altas de cuentas) o “es” para el idioma (“español”), etc. También es posible buscar por el software, es decir, por el tipo de plataforma: mastodon, friendica, akkoma, pleroma, misskey, y muchas otras más.

Por cierto, esas plataformas son tipo twitter, ¿no?

Bueno, se puede identificar casi (aunque no es tan semejante) a mastodon con twitter -de hecho sus twitts, se llaman toots –. Friendica, por ejemplo, tiene un estilo que algunas personas creen semejante a facebook. Igualmente, hay plataformas que no tienen nada que ver con las comerciales.

Por ejemplo, este artículo lo estás leyendo en una plataforma del fediverso para blogs textuales (no he encontrado ninguna forma de añadirle imágenes (aunque posiblemente pueda tenerla), pero se centra más bien en el texto. También hay plataforma sobre música. Hay otra (en formación) de videos cortos (tipo tiktok) que viene del mismo equipo que pixelfed, la plataforma de fotos del fediverso.

Incluso hay otra plataforma dedicada a los libros (bookwyrm), e incluso otra a los podcasts -en especial de audio- llamada castopod.

Después, para artículos largos pero con imágenes estaría Socialhome en la cual suelo escribir artículos largos sobre política y economía (en breve, voy a poner artículos de otros tipos de contenido).

Incluso hay una plataforma muy prometedora llamada bonfire donde quieren hacer instancias que promuevan cosas como el intercambio científico libre, el cuidado del medio ambiente, y muchas cosas más.

Es enorme esto, ¿No?

Como se puede ver, el nombre de fediverso no es casualidad. De hecho, hay un enorme universo de opciones de federarse al fediverso, incluso en otros protocolos distintos a ActivityPub, y algunas plataformas tienen varios protocolos (como Friendica que utiliza Zot y ActivityPub).

Por lo tanto, aquí tenéis una gran cantidad de opciones para hacer bitácoras (blogs) de sólo texto o también con elementos multimedia, para tener plataforma de microblogs (tipo twitter) o incluso de blogs (como esta en la que estamos (writefreely), podcasts o, casi, lo que se te ocurra.

Y, ¿algo que yo conozca, también puede estar federado?

Pues Wordpress, el conocido sistema de blogs, también se puede federar, pero esto da problemas con algunas instancias que podrían no querer contenido venido o de esa plataforma o de ciertas bitácoras (blogs) de la misma, como pasa con cualquier otro contenido federado.

Como se puede ver aquí, hay muchísimas opciones para habitar el fediverso, incluso más de una vez, según el tipo de artículos o cortes audiovisuales que quieras compartir.

¿Elegirás el tuyo?

forza4galicia

 
Leer más...

from Hannes

18.2.2025 Nichsts Besonderes Vor einigen Tagen tat mir der große Zeh vom rechten Fuß weh. Beim Schneiden des Nagels spürte ich, das eine Ecke in das Hautgewebe eingewachsen war. Nun versuchte ich die Ecke heraus zu schneiden. Den Zeh tauchte ich ins warmes Wasser ein, damit der Nagel etwas weicher wird. Ich schnitt von dem übrigen Teil des Nagels herunter, wahrscheinlich muss ich ihn zu tief abgeschnitten haben. Es fing etwas zu bluten an. Außerdem war der Zeh entzündet und rieb ihn mit Pferdesalbe ein. Spät in der Nacht holte ich aus der Küche nebem Radio eine Schmerztablette.. Es dauerte eine Weile, bis das die Schmerzen nachließen. Am Tage darauf war meinZeh schmerzfrei. Nun steckte die Nagelecke trotzdem noch drin, Ich wachte davon auf und die Entzündung war stärker geworden.. Es zog am ganzen Zeh, besonders wenn man an der Ecke drückte, tat es sehr weh. Heute ungefähr 10 Uhr 30 fuhr ich zum Arzt, weil es nicht besser wurde. Sie gab mir eine Überweisung zum Podologen und bekam noch einen Termin für heute. Um 12 Uhr 30 war ich dort. Die Ärztin besah sich den Nagel und bereitete warmes Wasser zu und musste meine Füße eintauchen, sie wurden gewaschen. Als nächstes stocherte sie am Nagel herum und holte die eingewachsene Ecke hervor und schnit sie ab. Die Ärztin bastele eine Spange, der dazu dienen sollte, das dann der Zehennagel nicht wieder ins Fleisch einwächst. Nun sollte ich die Klammer bis zu den nächsten Termin in 5 Wochen tragen. Jetzt spüre ich keine Schmerzen mehr. Heute wurden Schilder an der Grundschötteler Straße montiert. Da muss Tempo 30 kmh gefahren werden, ist auch besser so, dann gibt so nicht viele Unfälle.

 
Weiterlesen...

from BeiZero

В этой статье мы определим тип списков, введем несколько базовых операций над ними и докажем для них пару утверждений(например, что reverse (reverse list) ≡ list).

Модуль List

Определим модуль и импортируем тип равенства типов ≡ (пишется как \==) вместе с удобным синтаксисом для ведения доказательств, а так же натуральные числа и их свойства

module List where

-- Импорт модулей необходимых для ведения доказательства
import Relation.Binary.PropositionalEquality as Eq
open Eq 
open Eq.≡-Reasoning

-- Импорт натуральных чисел и их свойств
open import Data.Nat
open import Data.Nat.Properties

List

Индуктивно определим тип списка с помощью конструктора пустого списка и конструктора добавляющего элемент в начало списка

infixr 4 _::_

data List(A : Set) : Set where
  [] : List A
  _::_ : A → List A → List A -- → пишется как `\to`

Длина списка

Определим функцию возвращающую длину списка. Длина пустого списка равна нулю, а длина непустого списка 1 + длина его хвоста

length : {A : Set} → List A → ℕ
length [] = 0
length (_ :: xs) = 1 + (length xs) 

Интерактив

В компиляторе Agda присутствует интерактивный режим, которым можно пользоваться для проверки написанного кода

% agda -I src/List.lagda.md 
                 _ 
   ____         | |
  / __ \        | |
 | |__| |___  __| | ___
 |  __  / _ \/ _  |/ __\     Agda Interactive
 | |  |/ /_\ \/_| / /_| \
 |_|  |\___  /____\_____/    Type :? for help.
        __/ /
        \__/

The interactive mode is no longer under active development. Use at your own risk.
Main> 1 :: 2 :: []
1 :: 2 :: []
Main> length (1 :: 2 :: [])
2

HEAD и TAIL

Определим функции head и tail

  • head это функция возвращающая голову списка, т.е. первый элемент списка
  • tail это функция возвращающая хвост списка, т.е. список без первого элемента

но обе функции определены не для всех списков, а только для не пустых

Определение в Haskell

В Haskell, например, определение выглядит так

head                    :: HasCallStack => [a] -> a
head (x:_)              =  x
head []                 =  errorEmptyList "head"

tail                    :: HasCallStack => [a] -> [a]
tail (_:xs)             =  xs
tail []                 =  errorEmptyList "tail"

т.е. в случае пустого списка обе функции выкидывают ошибки

Определение в Haskell (через Maybe)

Есть довольно неплохой вариант вместо ошибки возвращать ответ завернутый в тип Maybe, например, в Haskell можно определить эти функции так

safeHead                    :: [a] -> Maybe a
safeHead (x:_)              =  Just x
safeHead []                 =  Nothing

safeTail                    :: [a] -> Maybe [a]
safeTail (_:xs)             =  Just xs
safeTail []                 =  Nothing

Определение в Agda

В Agda, с помощью зависимых типов, мы просто можем не определять head и tail на пустых списках, и их нельзя будет на них вызвать

head : {A : Set} → (a : List A) → {length a > 0} → A 
head (x :: _) = x

tail : {A : Set} → (a : List A) → {length a > 0} → List A 
tail (_ :: xs) = xs 
ex1 = head (1 :: 2 :: []) 

ex2 = head [] -- не может найти доказательство, что length a > 0 и просит его предъявить, при компиляции будет ошибка

ex3 = tail (1 :: 2 :: []) 

ex4 = tail [] -- не может найти доказательство, что length a > 0 и просит его предъявить, при компиляции будет ошибка

Ошибка компиляции

Не смотря на то, что непосредственно в редакторе отображается не ошибка, а подсказка, что нужно предоставить доказетельство не нулевой длины, во время компиляции действительно будет ошибка

% agda src/List.lagda.md   
Checking List (/Users/igorfedorov/Github/agda-pfds/src/List.lagda.md).
Unsolved metas at the following locations:
  /Users/igorfedorov/Github/agda-pfds/src/List.lagda.md:96,7-11
  /Users/igorfedorov/Github/agda-pfds/src/List.lagda.md:103,7-11

Цепочка преобразований

Для удобства ведения доказательств можно использовать операторы

  • a ≡⟨⟩ ba и b равны по определению
  • a ≡⟨ l ⟩ ba и b равны по утверждению l
  • – конец доказательства

Написание символов:

  • ∎ – \qed
  • ≡ – \==
  • ⟨ – \<
  • ⟩ – \>

Полезные функции

  • (f a) ≡⟨ cong f l ⟩ (f b)cong конгруэтность, если аргументы f равны по l, т.е. a ≡⟨ l ⟩ b, то (f a) ≡⟨ cong f l ⟩ (f b)
  • b ≡⟨ sym l ⟩ asym симметричность, если a ≡⟨ l ⟩ b, то b ≡⟨ sym l ⟩ a

Добавление в конец

Определим функцию добавления элемента в конец списка. Добавление a в конец пустого списка это список из состоящий из одного элемента a, а добавление в конец непустого списка это добавление в конец его хвоста.

Обратите внимание, что операция добавления в конец имеет алгоритмическую сложность O(n), где n – длина списка.

append : {A : Set} → List A → A → List A 
append [] a = a :: []
append (x :: xs) a = x :: (append xs a)

Длина append

Докажем с помощью индукции, что длинна списка после применения append увеличивается на единицу

append-length-lemma : {A : Set} → (l : List A) → (a : A) → 
                      length (append l a) ≡ 1 + (length l)
-- База
append-length-lemma {A} [] a = 
    length (append [] a) ≡⟨⟩ 
    length (a :: []) ≡⟨⟩
    1 + (length {A} []) ∎ --необходимо явно указать тип т.к. [] может не быть типа List A
-- Шаг индукции
append-length-lemma (x :: xs) a = 
    length (append (x :: xs) a) ≡⟨⟩ 
    length (x :: (append xs a)) ≡⟨⟩ 
    1 + (length (append xs a)) ≡⟨ cong suc (append-length-lemma xs a) ⟩ 
    -- Для (length (append xs a) лемма уже доказана, поэтому используем cong suc 
    1 + (1 + (length xs)) ∎ 

Цепочку преобразований в которой есть ≡⟨⟩ можно заменить на refl, но для наглядности иногда удобнее не сокращать.

Определение конкатенации

Определим конкатенацию двух списков

infixr 5 _++_

_++_ : {A : Set} → List A → List A → List A 
[] ++ ys = ys 
(x :: xs) ++ ys = x :: (xs ++ ys)

Правый ноль

Покажем, что [] является правым нулем относительно конкатенации

[]-rightUnit : {A : Set} → (a : List A) → a ++ [] ≡ a 
[]-rightUnit [] = refl
[]-rightUnit (x :: xs) = 
  (x :: xs) ++ [] ≡⟨⟩ 
  x :: (xs ++ []) ≡⟨ cong (λ l → x :: l) ([]-rightUnit xs) ⟩
  x :: xs ∎

Ассоциативность конкатенации

Докажем ассоциативность конкатенации

++-assoc : {A : Set} → (a b c : List A) → (a ++ b) ++ c ≡ a ++ (b ++ c)
++-assoc [] b c = 
    ([] ++ b) ++ c ≡⟨⟩ 
    b ++ c ≡⟨⟩ 
    [] ++ (b ++ c) ∎ 
++-assoc (x :: a) b c = 
    ((x :: a) ++ b) ++ c ≡⟨⟩ 
    (x :: (a ++ b)) ++ c ≡⟨⟩ 
    x :: ((a ++ b) ++ c) ≡⟨ cong (λ y → (x :: y)) (++-assoc a b c ) ⟩ 
    -- для (a ++ b) ++ c ассоциативность доказана, поэтому используем cong 
    x :: (a ++ (b ++ c)) ≡⟨⟩ 
    (x :: a) ++ (b ++ c) ∎

Длина конкатенации

Докажем, что длина конкатенации двух строк равна сумме длин этих строк

length-concat-sum : {A : Set} → (a b : List A) → 
                    length (a ++ b) ≡ length a + length b 
length-concat-sum {A} [] b = 
    length ([] ++ b) ≡⟨⟩ 
    length b ≡⟨⟩ 
    0 + length b ≡⟨⟩
    length {A} [] + length b ∎
length-concat-sum (x :: xs) b = 
    length (x :: xs ++ b) ≡⟨⟩ 
    length (x :: (xs ++ b)) ≡⟨⟩
    suc (length (xs ++ b)) ≡⟨ cong suc (length-concat-sum xs b) ⟩
    suc (length xs + length b) ∎ 

Определение foldLeft

Определим левую свертку

foldLeft : {A B : Set} → List A → B → (B → A → B) → B
foldLeft [] b _ = b
foldLeft (x :: xs) b f = foldLeft xs (f b x) f

Определения reverse

Определим функцию reverse, т.к. существует несколько вариантов имплементации определим их все и сможем подоказывать их эквивалентность(с точки зрения возвращаемого результата)

Через append

reverse можно определить, например, через append

reverse-by-append :  {A : Set} -> List A -> List A
reverse-by-append [] = []
reverse-by-append (x :: v) = append (reverse-by-append v) x

проблема этой реализации в сложности, которая будет O(n²)

Через concat

Можно так же использовать concat

reverse-by-concat : {A : Set} → List A → List A 
reverse-by-concat [] = []
reverse-by-concat (x :: xs) = (reverse-by-concat xs) ++ (x :: [])

сложность этой реализации так же O(n²)

Через аккумулятор

Более “хитрое” решение можно написать используя аккумулятор

reverse-by-acc : {A : Set} → List A → List A → List A 
reverse-by-acc acc [] = acc 
reverse-by-acc acc (x :: xs) = reverse-by-acc (x :: acc) xs

reverse : {A : Set} → List A → List A 
reverse = reverse-by-acc []

сложность этой реализации уже O(n), эту реализацию и будем считать каноничной

Через foldLeft

Аналогичная реализация, но аккумулятор мы перенесем в foldLeft

reverse-by-foldLeft : {A : Set} → List A → List A 
reverse-by-foldLeft l = foldLeft l [] (λ b a → a :: b)

так же за O(n)

Доказательство эквивалентности реализаций reverse

Рассмотрим несколько доказательств эквивалентности реализаций reverse(остальные можно подоказывать самостоятельно)

Через foldLeft и аккумулятор в аргументе

Докажем эквивалентность reverse через foldLeft и через аккумулятор в аргументе. Для этого представим, что мы находимся в процессе выполнения reverse'а и аккумулятор уже не пуст

reverses-eq-1' : {A : Set} → (acc : List A) → (a : List A) → 
                 reverse-by-acc acc a ≡ foldLeft a acc (λ b a → a :: b)
reverses-eq-1' _ [] = refl
reverses-eq-1' acc (y :: ys) = 
    reverse-by-acc  acc (y :: ys) ≡⟨⟩ 
    reverse-by-acc  (y :: acc) ys ≡⟨ reverses-eq-1' (y :: acc) ys ⟩ 
    foldLeft ys (y :: acc) (λ b a → a :: b) ∎

Через foldLeft и аккумулятор в аргументе, но “честно”

Предыдущее доказетельство не совсем честное т.к. доказывает эквивалентность на определенном шаге рекурсии, чтобы сделать его “честным” просто подставим вместо аккумулятора пустой список

reverses-eq-1 : {A : Set} → (a : List A) → 
                reverse-by-acc [] a ≡ reverse-by-foldLeft a
reverses-eq-1 = reverses-eq-1' []

Через acc и ++ (лемма)

Для доказательства сначала представим, что мы уже находимся на каком-то шаге рекурсии и аккумулятор не пуст, и покажем, что элемент в начале списка переносится в конец

reverses-eq-2' : {A : Set} → (acc : List A) → (l : List A) → (a : A) → 
                 reverse-by-acc acc (a :: l) ≡ reverse-by-acc [] l ++ (a :: acc)
reverses-eq-2' _ [] _ = refl
reverses-eq-2' acc (x :: []) a = refl
reverses-eq-2' acc (x₁ :: x₂ :: xs) a =
    reverse-by-acc acc (a :: x₁ :: x₂ :: xs) ≡⟨⟩ 
    reverse-by-acc (a :: acc) (x₁ :: x₂ :: xs) ≡⟨⟩
    reverse-by-acc (x₁ :: a :: acc) (x₂ :: xs) ≡⟨⟩
    reverse-by-acc (x₁ :: a :: acc) (x₂ :: xs) ≡⟨ reverses-eq-2' (x₁ :: a :: acc) xs x₂ ⟩ 
    reverse-by-acc [] xs ++ (x₂ :: x₁ :: a :: acc) ≡⟨⟩
    reverse-by-acc [] xs ++ ((x₂ :: x₁ :: []) ++ (a :: acc)) 
      ≡⟨ sym (++-assoc (reverse-by-acc [] xs) (x₂ :: x₁ :: []) (a :: acc))⟩ 
    (reverse-by-acc [] xs ++ (x₂ :: x₁ :: [])) ++ (a :: acc) 
      ≡⟨ cong (λ x → x ++ (a :: acc)) (sym(reverses-eq-2' (x₁ :: []) xs x₂ )) ⟩
    (reverse-by-acc (x₁ :: []) (x₂ :: xs)) ++ (a :: acc) ≡⟨⟩
    (reverse-by-acc [] (x₁ :: x₂ :: xs)) ++ (a :: acc) ∎ 

Через acc и ++

Теперь можем подставить вместо аккумулятора пустой список и завершить доказательство

reverses-eq-2 : {A : Set} → (l : List A) → 
                reverse-by-acc [] l ≡ reverse-by-concat l
reverses-eq-2 [] = refl
reverses-eq-2 (x :: xs) = 
    reverse-by-acc [] (x :: xs) ≡⟨ reverses-eq-2' [] xs x ⟩
    reverse-by-acc [] xs ++ (x :: []) 
      ≡⟨ cong (λ l → l ++ (x :: [])) (reverses-eq-2 xs) ⟩
    reverse-by-concat xs ++ (x :: []) ∎

Длина reverse

reverse-length : {A : Set} → (a : List A) → length (reverse a) ≡ length a
reverse-length [] = refl
reverse-length (x :: xs) = 
  length (reverse (x :: xs))  ≡⟨ cong length (reverses-eq-2' [] xs x) ⟩
  length (reverse xs ++ (x :: [])) ≡⟨ length-concat-sum (reverse xs) (x :: []) ⟩
  length (reverse xs) + length (x :: [])
    ≡⟨ cong (λ a → a + length (x :: [])) (reverse-length xs) ⟩ 
  length xs + length (x :: []) ≡⟨⟩ 
  length xs + 1 ≡⟨ +-suc (length xs) 0 ⟩ 
  1 + (length xs) + 0 ≡⟨ +-comm ( 1 + (length xs)) 0 ⟩ 
  1 + (length xs) ∎

reverse инвертирует конкатенацию

reverse-inversion : {A : Set} → (a b : List A) → 
                    reverse (a ++ b) ≡ reverse b ++ reverse a

База

reverse-inversion [] b = 
  reverse b ≡⟨ sym ([]-rightUnit (reverse b)) ⟩ 
  reverse b ++ [] ≡⟨⟩ 
  reverse b ++ reverse-by-concat [] 
    ≡⟨ cong (λ x → reverse b ++ x) (sym(reverses-eq-2 []))⟩
  reverse b ++ reverse [] ∎

Шаг

reverse-inversion (x :: xs) b = 
  reverse ((x :: xs) ++ b) ≡⟨⟩ 
  reverse (x :: (xs ++ b))  ≡⟨ reverses-eq-2' [] (xs ++ b) x ⟩ 
  reverse (xs ++ b) ++ (x :: []) 
    ≡⟨ cong (λ l → l ++ (x :: [])) (reverse-inversion xs b) ⟩ 
  (reverse b ++ reverse xs) ++ (x :: []) 
    ≡⟨ ++-assoc (reverse b) (reverse xs) (x :: []) ⟩ 
  reverse b ++ (reverse xs ++ (x :: [])) 
    ≡⟨ cong (λ l → reverse b ++ l)(sym (reverses-eq-2' [] xs x)) ⟩
  reverse b ++ reverse (x :: xs) ∎

Инволюция reverse

reverse-involution : {A : Set} → (a : List A) → reverse (reverse a) ≡ a
reverse-involution [] = refl
reverse-involution (x :: xs) = 
  reverse (reverse (x :: xs)) ≡⟨ cong reverse (reverses-eq-2' [] xs x) ⟩
  reverse (reverse xs ++ (x :: [])) ≡⟨⟩ 
  reverse (reverse xs ++ (x :: []))  ≡⟨ reverse-inversion (reverse xs) (x :: []) ⟩
  reverse (x :: []) ++ reverse (reverse xs) ≡⟨⟩ 
  (x :: []) ++ reverse (reverse xs) 
    ≡⟨ cong (λ l → (x :: []) ++ l) (reverse-involution xs) ⟩ 
  (x :: []) ++ xs ≡⟨⟩
  x :: ([] ++ xs) ≡⟨⟩ 
  x :: xs ∎
 
Read more...

from Erdrandbewohner

Ein Bericht – Tag 1 und Tag 2

Eine Reise zweier neurodivergenter Menschen mit sehr kaputten Reizfiltern nach Paris. Im Februar. Kann das gut gehen? Macht das Spaß? Oder floss Blut? Steht Paris noch?

Bevor ich diese Fragen beantworte, erst einmal die Vorgeschichte:

Vor etwa zwei Monaten sagte meine Liebste: „Schau mal, wir müssen nur noch eine Hotelübernachtung bis Februar auf der Plattform „hotelbuchungen.com“ (die Plattform heißt in Wirklichkeit anders) buchen, dann bekommen wir den Supergast-Status Level 3! Wie wäre es, wenn wir für ein paar Tage nach Köln fahren? Museen und so, das wird sicher toll!“

Nun, Köln im Spätwinter entpuppte sich beim nähren Nachdenken als eher unsexy. Aber hey, wir waren schon lange nicht mehr in Paris gewesen! Außerdem ist Paris viel größer, schöner und hat viel tollere Museen! Und es ist schneller und sicherer zu erreichen als Köln, weil wir mit dem TVG fahren. Der ist immer pünktlich. Im Gegensatz zur Deutschen Katastrophenbahn, wo wir wegen Feuchtigkeit auf den Gleisen (nicht wirklich, aber ähnlich albern) schon mal fast sechs Stunden von Köln nach Trier unterwegs waren.

Wie wir in diversen Reiseblogs lasen, wurde eine Reise nach Paris im Februar als super toll angepriesen, denn das sei der Monat mit den wenigsten Touristen, was kaum Warteschlangen vor den touristischen Hotspots bedeute und eine viel entspanntere Atmosphäre garantiere. (Haha. Aber dazu später...)

Meine Liebste ist bei uns die Reiseplanungsbeauftragte, das ist eines ihrer Spezialinteressen und wohl mit ihre überragendste Superkraft. Ich hingegen fuchse mich in die Stadtstruktur ein, finde so verborgene Juwelen, erarbeite die geschichtlichen Hintergründe und bin ansonsten ein angenehmer Reisegenosse. Meine Liebste fand heraus, dass das von uns ausgesuchte Hotel auf dieser Buchungsplattform sehr viel teurer als bei der Direktbuchung, womit sich unser Supergast-Status Level 3 erledigt hatte. Egal, wir waren angefixt und wollten raus, was erleben.

Reisevorbereitungen sind bei uns eine komplizierte Sache. Es gibt zweierlei Reisevorbereitungen: Zum einen die Organisation, also die Reservierungen, das Herausfinden von Öffnungszeiten und die Buchungen von Zeitfenstern zum Besuch von Museen, Denkmälern usw.

Und es gibt die innere Reisevorbereitung. Das beinhaltet das Schwanken zwischen „Das wird alles ganz toll, oh was freue ich mich!“ und „OMG, wir sind doch völlig bescheuert! Wie kamen wir bloß darauf, wegfahren zu wollen! Und das auch noch im Februar! Was ist, wenn das Wetter scheiße ist? Oder wenn irgendwas schief läuft?“. Außerdem ertrage ich es nicht, wenn ich von einer Reise nach Hause komme und das Haus ist unordentlich. Also steht vor dem Abfahrtstermin eine gigantische Putzorgie auf dem Plan. Ja, ich weiß, es klingt vermutlich sehr bescheuert, aber ich brauche die Gewissheit, dass alles in Ordnung ist, wenn ich zurück komme. Je näher der Termin rückt, desto intensiver wird die Anspannung und das Wechselbad der Gefühle – bis... bis wir endlich unterwegs sind und keine Überraschungen mehr befürchten müssen.

Wir haben uns im TGV die erste Klasse gegönnt. Der Aufpreis dafür ist im Vergleich zur Deutschen Katastrophenbahn lächerlich gering, der zusätzliche Komfort aber unbezahlbar. Es ist recht ruhig, man hat Platz und man kann sich zwischen den ganzen Geschäftsfuzzis hinter ihren Laptops wichtig fühlen. Mit 315 km/h durch die Champagne zu donnern ist schon ein tolles Erlebnis!

Als Unterkunft in Paris haben wir uns für ein einfaches Hotel im Zentrum des Stadtteils Belleville entschieden. In Belleville hatten wir in einem früheren Urlaub schon mal gewohnt und wir haben uns in diesen Ort verliebt. Die Gentrifizierung ist noch nicht weit fortgeschritten, hier wohnen also noch „echte“, alteingesessene Menschen, es gibt zwei große Parks, viele kleine tolle Geschäfte, Streetart, Kneipen, Restaurants, Cafés und vor allem: Es gibt hier kaum etwas, was Standard-Touris interessiert. Nur ein paar Meter von unserem Hotel befinden sich eine Bushaltestelle und eine Metrostation. Prima!

Das Hotel war dann wirklich ganz okay, es war wie gesagt einfach, aber sauber, die Matratzen waren perfekt und das Bad war frisch renoviert. Die Heizung funktionierte und ein simples Frühstück mit so viel Kaffee wie man wollte gab es auch. Unser Zimmer ging raus auf die Kirche, ein etwas heruntergekommenes, schmutzig-graues, neogotisches Ding mit zwei Kirchtürmen und einer schepprig klingenden Glocke, die gottseidank die meiste Zeit nicht bimmelte.

Nach dem Einchecken sind wir dann als aller erstes zur frisch sanierten Kathedrale Notre Dame gefahren. Meine Liebste ist Kunsthistorikerin, sie sabberte bereits vor freudiger Erwartung. Bei unseren bisherigen Paris-Aufenthalten hatte wir die Kathedrale nicht besucht, aber nach dem Brand und der Sanierung gab es diesmal keinen Weg daran vorbei.

Also ab in die U-Bahn-Linie 11. War die beim letzten mal auch so höllisch voll? Selbst zu Zeiten außerhalb des Berufsverkehrs? Wie stressig. Ich liebe das Fahren in einer U-Bahn, aber ich konnte mich nicht daran erinnern, dass es sooo laut war, die Menschen soooo hektisch und die Wägen soooo gerammelt voll waren!

Gestresst kamen wir auf der Ile de la Cité an und hier erlebten wir die ach so ruhige und entspannte Atmosphäre von Paris mit wenigen Touristen im Februar. Polizei. Überall Polizei. Teils schwer bewaffnet, teils die öffentliche Ordnung alleinig durch einen besonders grimmigen Gesichtsausdruck sichernd. Polizist*innen patroullierten in Gruppen, fuhren auf Motorrädern umher, saßen in Mannschaftsbussen oder blockierten die Straßen. Großes Tatütata (auf französisch klingt das Tatütata wie Düddledü-Düddledü). Später wurde klar, warum da so ein Geschiss gemacht wurde. Ein Staatsbesuch.

Die „wenigen“ Februar-Touristen entdeckten wir dann auf dem Kathedralenvorplatz. Eine zig hundert Meter lange Schlange mit zig hunderten, wenn nicht sogar tausenden Menschen wand sich quer über den Platz und wuchs dabei in rasanter Geschwindigkeit. Alle warteten auf ihren Einlass in Notre Dame. Daneben gab es eine deutlich kleinere Schlange. Die war für die Leute, die ein Zeitfenster im Internet ergattern konnten. Also für so Leute wie wir, denn meine Liebste hat in einem heroischen Akt tatsächlich ein üblicherweise ausverkauftes Zeitfenster geschossen. Yippie! Trotzdem mussten wir erst einmal an der Sicherheitskontrolle vorbei. Taschenkontrolle, Schnellabfertigung, in die Kathedrale hineingetrieben, eng an eng mit Menschen aus allen Herren Ländern, als Teil einer amorphen, sich durch die Kirche schiebenden Walze bestehend aus tausenden von Leibern. Habe ich das Wort Stress eigentlich schon geschrieben? Ja? Zurecht. Trotz Ohrenstöpsel, die uns vor dem schlimmsten Lärm abschirmten.

Ich ertrage keine Enge, mit zufälligen Berührungen durch fremde Leute habe ich ein großes Problem. Vor allem, wenn ich eh schon gestresst und überreizt bin. Nach wenigen Minuten, in denen ich einen Blick auf das nun wundervoll in fast weißem Kalkstein erstrahlendem Gebäude werfen konnte, wollte ich nur noch schreien und um mich schlagen. Mein Sichtfeld verengte sich, jeder Muskel in meinem Körper war angespannt und mir wurde schwindelig vor Wut. Ich musste da raus – sofort! Ein beginnender Meltdown. Höllehöllehölle!

Draußen atmete ich erstmal durch, versuchte herunter zu kommen und wartete auf meine Liebste, die dann auch bald eben so gestresst (ja, schon wieder dieses Wort!) aber auch sehr glücklich aus der Kirche kam. Wir beratschlagten kurz, wie es nun weiter ginge und wir beschlossen, so schnell wie möglich dem stressigen Gewusel und der immer noch herumlärmenden Polizei zu entfliehen... (Das wars jetzt erstmal mit dem Wort „gestresst“, versprochen!)

Hunger. Wir entdeckten unseren Hunger. Er war sehr groß. Außerdem begann es zu dämmern und zu schiffen. Wir kamen an einem ruhigen, winzigen asiatischen Restaurant vorbei, in dem ein kleines Buffet aufgebaut war, von dem man so viel essen konnte, wie man wollte. Die Speisen waren nicht warm, dafür standen mehrere Mikrowellengeräte bereit. Sowas habe ich noch nie gesehen, aber ich fand es lustig und das Essen war sogar sehr lecker und günstig.

Etwas im Bauch zu haben und die Ruhe halfen mir, ich fühlte mich bereit noch etwas zu erleben. Wie zufällig stand da das Centre Pompidou in der Nähe herum, dieses auf links gedrehte Museumsgebäude für moderne und zeitgenössische Kunst. Darin war ich erst ein mal in meinem Leben, als Kind, vermutlich etwa 1980. Damals hat mich nicht nur das Gebäude beeindruckt, sondern auch die dadaistischen Kunstwerke, die ich als kopfchaotisches Kind mit eingebauter assoziativer Denkweise offenbar intuitiv verstand und sofort liebte.

Und hier hatten wir den ersten Paris-Moment für diesen Urlaub. Eine Mischung aus Begeisterung, aus Staunen und einem dauerhaften Grinsen im Gesicht. Es begann bereits auf der außerhalb der Fassade entlangführenden Rolltreppe. Je höher wir kamen, desto fantastischer der Blick über die Stadt. In der Ferne, nebelverhangen, strahlte der illumierte Eiffelturm sein Leuchtturmleuchten in die tiefhängenden Wolken, und ganz rechts ragte der Hügel Montmatre mit seiner kitschigen Zuckerbäckerkirche aus der Dunkelheit hervor. Zusammen mit den retrofuturistisch rot beleuchteten Rolltreppenröhren des Kunstmuseums löste dieser Ausblick bei uns eine fast schon surrealistische Stimmung aus. Apropos Surrealismus. Leider haben wir die große Surrealismus-Sonderausstellung um wenige Tage verpasst. Schade. Aber wir hatten trotzdem großen Spaß, sowohl mit den hochkarätigen Kunstwerken (die wir genossen, aber einfach nicht ernst genommen haben) als auch mit dem Beobachten der kulturbegeisterten Besucher*innen (die die Kunstwerke mit sehr gewichtigem Gesichtsausdruck und unangemessenen Ernst betrachteten). Übrigens waren viele Besuchende ihr eigenes (dadaistisches) Kunstwerk. Ich schätze, das waren Angehörige der örtlichen Modeindustrie oder solche, die sich ihr streng verpflichtet fühlen…

Sehr glücklich, aber physisch und psychisch völlig am Ende und bereits wieder mit einem Tunnelblick gings per Metro zurück zum Hotel nach Belleville. Sowohl in der Metro als auch in Belleville pulsierte trotz vorgerückter Stunde noch das Leben. Gehörschutz – so wichtig! Gegen zu viele optische Reize hilft nur Augen zu. Was aber nicht immer machbar oder sinnvoll ist, wenn man sich in einer Großstadt bewegt… Die mitgebrachten CBD-Fruchtgummis sorgten dafür, dass wir innerlich herunterfahren und schlafen konnten.

Fazit Tag 1: Bereits das frühe Aufstehen, die Aufregung, die Anreise kosteten uns einige Löffel. Der Besuch von Notre Dame und mein beginnender Meltdown saugte mir meinen Akku komplett leer. Die Energie für den tollen Museumsbesuch haben meine Liebste und ich uns vom folgenden Tag geliehen. Das geht. Und vor allem geht es grandios in die Hose, wenn man am nächsten Tag was vor hat und nicht ausreichend regenerieren kann oder will.

Tag 2.

Der Tag begann viel zu früh mit dem betörenden Duft von frisch gebackenem Brot und heißen Crossaints. Ganz in der Nähe gibt es eine Bäckerei, die das gesamte Viertel allmorgendlich beduftet. Natürlich konnte ich nicht mehr schlafen (mein Schlaf ist natürlich dann gestört, wenn ich ihn am meisten brauche) und beobachtete und lauschte statt dessen, wie das Viertel langsam erwachte. Das kleine Café hatte bereits vor 6:00 Uhr in der Früh geöffnet und in der Dunkelheit saßen die ersten Gäste an den Tischen an der Straße und tranken ihren Kaffee und rauchten dazu sehr klischeehaft eine Zigarette, bevor sie von dem Loch im Gehweg mit dem Schild „Metro“, verschluckt wurden. Ja, in Frankreich wird immer noch viel geraucht. Lastenradfahrer*innen fuhren Waren aus oder ihre Kinder in die jeweiligen Lehr- oder Verwahranstalten, die Stadtreinigung tat ihr Bestes, und das sogar mehrmals.

So ganz fit war ich nicht, das merkte ich ziemlich schnell. Denn auch die drei Tassen Kaffee beim einfachen Frühstück im eher schlicht und sachlich gehaltenen Frühstücksraum vertrieb nicht die Müdigkeit und auch nicht die Schwere in den Gliedern. Ja, kein Wunder, denn gestern war alles zu viel und der Schlaf war zu wenig.

Auf dem Plan für den Tag stand die Sainte-Chapelle, ein hochgotisches Wunderwerk das vor allem aus bunten Fenstern besteht. Früher war sie die Kapelle der königlichen Residenz auf der Ile de la Cité Aus der königlichen Residenz wurde später nach vielen Umbauten der Justizpalast, ein heute schwer gesicherter, aber auch ein traurig abgeranzt-vergammelter Ort. Doch wir hatten noch Zeit, meine Liebste ergatterte eine Eintrittskarte für um 12:00 Uhr.

Wir beschlossen, durch Belleville zu schweifen, bewunderten die Käseläden, sabberten vor den Fischläden, bestaunten die wirklich schönen Wandmalereien (aka Streetart) und fanden eine Kreuzung, an der man von der Rue de Belleville den Hügel herab über die Stadt bis zum Eifelturm schauen kann, der hinter dem Dunst und dem Morgennebel der Stadt wie eine unwirkliche, fremdartige Landmarke über der Dachlandschaft hervorragte.

Durch kleine Wohnstraßen schlendernd strebten wir zum Parc de Belleville. Bevor die Stadt Paris zu ihrer heutigen Größe explodierte, wurde an den Hängen des Hügels, der heute teilweise bebaut, teilweise der Park ist, Wein und Obst angebaut. Später lebte hier die aufsässige Arbeiterklasse, vom Bürgertum und der reaktionären Regierung argwöhnisch beobachtet, und hier wie im Parc des Buttes Chaumont fand die unvergessene Pariser Kommune, der erste Versuch einer sozialistischen Gemeinschaft, in einem gnadenlosen Gemetzel ihr trauriges Ende. Daran erinnert heute nichts mehr.

Der Park ist hübsch angelegt, wir hatten von der obersten Terrasse eine phantastische Aussicht über die Stadt – und auf eine Gruppe von etwa zehn älteren Damen aus Asien, die zu asiatischen Popsongs eine nur für sie einen Sinn ergebende Choreographie tanzten und uns ein Lächeln ins Gesicht zauberten. Nicht nur die tanzenden Damen bevölkerten den kahlen, winterschlafenden Park, sondern auch ein paar Grüppchen Jugendliche. Ich vermute, sie repräsentieren die inoffiziellen französischen Freiluft-Coffeeshops, wo man dubiose Kräuter erwerben und gleichzeitig konsumieren kann…

Bis hier hin liest es sich, als hätten wir einen sehr erholsamen und entspannten Vormittag gehabt, nicht wahr? Stimmt. Aber das ändert sich genau jetzt. Achtung, mit sehr hoher Wahrscheinlichkeit werde ich wieder sehr oft das Wort „Stress“ in all seinen Formen und Ableitungen benutzen.

Nachdem wir den Park von oben nach unten durchschlendert hatten, trafen wir auf den Boulevard de Belleville, und dort fand gerade der wöchentliche Straßenmarkt statt. Ich liebe Märkte! Laute, bunte, wuselige Märkte, mit Menschen aus allen möglichen Kulturen, die ihre Waren anpreisen, feilschen, oder kaufen. Märkte, auf denen ich Obst, Gemüse oder auch tote Tiere sehe, deren Existenz mir bisher unbekannt war und über deren Eignung als Nahrung ich sehr skeptisch bin. Hier schieben sich alte Männer mit rot gefärbtem Bart aus Bangladesch durch die Menge, neben den in traditionelle Gewänder gehüllten Menschen aus Zentralafrika. Elegant für den Markt herausgeputzte ältere Pariserinnen beratschlagen sich mit jungen Frauen mit Kopftuch über die Qualität der Fische, während am Stand nebendran ein Verkäufer mit lautem Sprech-Singsang für seine Waren wirbt. Herrlich!

Bevor ihr euch nun fragt, wie ich als Mensch ohne nennenswerten Reizfilter eine solche Atombombe an Reizen „herrlich“ finden kann: nun, ich weiß was auf mich zukommt, daher weiß ich, wie ich in diesem Tsunami an Reizen schwimmen muss und ich weiß (meistens), wann ich da raus muss. Ich will es und ich entscheide mich dafür. Das genau macht den Unterschied zu Situationen, die ich nicht will und auch nicht beeinflussen kann. Aber mir ist bewusst, dass mich so ein Markt am Ende enorme Energie kostet. Ein hoffentlich treffendes Gleichnis: Ein Mensch kann unter Wasser nicht lange überleben. Aber man kann mit angehaltener Luft tauchen und die Fische im Wasser beobachten. Wenn die Luft verbraucht ist und die Lunge schmerzt, ist man gezwungen zum Atmen aufzutauchen...

Also habe ich meine Liebste angeschaut, sie nickte. Gehörschutz in die Ohren und los, sich treiben lassen, gucken, riechen und staunen. Mittendrin drehte ich mich nach ihr um. Oh je, sie sah bereits enorm angestrengt und gestresst aus und bald darauf machte sie Zeichen, dass es ihr zu viel wird. Gut, dass wir eh schon fast am Ende des Marktes angekommen waren. Als wir uns etwas abseits ohne Gehörschutz unterhalten konnten, spürte auch ich, dass das auch mir schon fast zu viel war. Ich habe mich überschätzt, vergessen, dass ich mit zu wenig Schlaf und einem Energiedefizit in den Tag gestartet bin. Mist.

Nirgends gab es eine wirklich ruhige Ecke, der Verkehr auf dem Boulevard toste, Presslufthämmer, hupende Autos, Motorräder, überall Menschen. Außerdem meinte meine Liebste, dass wir nun langsam los zur Sainte-Chapelle müssten. Also eine Bushaltestelle finden. Wieder Stress. Wo sind wir überhaupt, und warum funktioniert das scheiß GPS nicht ordentlich? Ah. Hier sind wir. Jetzt links rein in eine belebte Seitenstraße, dort sollte eine Bushaltestelle sein, sagte die Pariser ÖPNV-App. Menschenmassen, blinkende Lichter, Läden, Gesprächsfetzen und laute Musik, und nach hunderten Metern Slalomlauf endlich die Bushaltestelle. Meine Liebste sah inzwischen zutiefst verzweifelt aus, ergatterte einen Sitzplatz im Wartehäuschen und versuchte sich herunterzuregulieren. Ich spürte, wie verspannt meine Schultern waren, atmete bewusst und versuchte meinen Stress und die Anspannung fallen zu lassen. Erfolglos.

Das wäre nun der Punkt, an dem wir dringend einen Park, ein ruhiges Cafe, notfalls eine stille Kirche gebraucht hätten. Statt dessen saßen wir im Bus zur Ile de la Cité. Im Stau. Um uns hupten genervte Menschen in ihren Autos, fest davon überzeugt, dass sich der Stau durch ihre Huperei in Wohlgefallen auflöst.

Auf die Sainte-Chapelle hatte ich mich mit am meisten gefreut. Dummerweise liegt sie unweit der Kathedrale Notre Dame, also im Epizentrum des touristischen Paris. Wie am Tag zuvor war alles voll mit schwerbewaffneter Polizei, Straßenzüge waren abgesperrt, Taschen wurden anlasslos kontrolliert. Blaulicht und „Düddledü-Düddledü, Düddledü-Düddledü, Düddledü-Düddledü“. Wieder ein Staatsbesuch? Kurz vor 12:00 Uhr fanden wir die Schlangen mit Menschen, die ebenfalls in die Saint-Chapelle oder in die Conciergerie wollten. Eine Reihe für Leute ohne gebuchten Timeslot, die andere Reihe für Leute, die wie wir ein Ticket gebucht hatten. Beide Schlangen etwa gleich groß. 12:00 Uhr. Es tat sich nichts. Um 12:15 Uhr standen wir immer noch in der selben Position draußen in der Kälte rum. Genau wie um 12:30 Uhr. Wir waren beide maximal genervt, niemand wusste, was oder ob etwas passiert. Dann endlich wurde die Absperrung für unsere Schlange geöffnet und wir durften zur Sicherheitskontrolle in einen hässlichen, kahlen Raum. Teils unfreundliches, teils gelangweiltes Sicherheitspersonal durchleuchtete unsere Taschen, ein Flughafen-Nacktscanner durchleuchtete uns.

Dann standen wir in einem der Innenhöfe des abgeranzten Justizpalastes und durften uns nun zur Ticketkontrolle anstellen. Das dauerte gottseidank nicht zu lange, und schließlich befanden wir uns im Untergeschoss der Kapelle, stiegen eine enge, steinerne Wendeltreppe hinauf und landeten inmitten einer lärmenden Menschenmasse. Glaubt mir, das war der Moment, an dem ich erneut kurz davor war auszurasten. Ich war eh schon sehr drüber, und nun wieder eingekeilt zwischen fremden Menschen, ohne Ruhe, ohne die Möglichkeit, sich hinzusetzen und die gigantischen Fenster und die Architektur auf sich wirken zu lassen. Ich konnte mich auf nichts mehr fokusieren, mein Sichtfeld verengte sich, mein Puls raste, ein beginnender Meltdown. Ich musste raus. So schnell wie möglich. 13 Euro Eintrittsgeld fürn Arsch. Draußen hätte ich fast angefangen zu heulen. Teils, weil mein Nervensystem komplett dereguliert war, teils aus Enttäuschung über die gesamte Situation.

Ich musste nicht lange auf meine Liebste warten. Auch sie war enttäuscht und völlig drüber, gemeinsam flüchteten wir aus dem Justizpalast, irgendwo hin, wo wir uns weniger Leute und weniger Lärm erhofften. An einen Ort, wo wir uns hinsetzen und runterkommen, vielleicht sogar was trinken und essen können.

Wenn wir beide unterwegs sind und nur eine Person drüber ist oder bereits schon im Meltdown, dann kann die andere Person die Führung und die Verantwortung übernehmen. Das hilft ungemein, so retten wir uns regelmäßig gegenseitig den Arsch. Wenn wir allerdings beide durch sind, kurz vor dem Meltdown stehen oder schon drin sind, dann ist das eine gefährliche Situation, weil niemand mehr einen klaren Kopf hat. Gefährlich, weil es sein kann, dass wir dann einen üblen Krach bekommen, der uns dann noch mehr in den Meltdown hinein reitet. Nicht selten bis zum Shutdown. Aber so weit kam es gottlob nicht. Im Quartier Latin, auf der „Schäl Sick“ von Paris, fanden wir ein nett aussehendes Café, in dem nicht viel los war. Ein sehr freundlicher Kellner begrüßte uns und auf der Sitzbank am Tisch neben uns schlummerte eine wuschelige Katze. Ein guter Ort. Durchatmen. Kaffee trinken. Was essen. Die übrig gebliebenen, verstreuten Lebensgeister zusammenrufen.

Normalerweise wäre das jetzt der Punkt, an dem vernünftige Leute merken, dass es genug ist und herausfinden, wie man am besten zurück zum Hotel kommt. Vernünftige Leute. Also nicht wir.

Denn ich hatte auf dem Weg zum Café eine Ruine gesehen. Aufsteigendes Mauerwerk, das ich als römisch identifizierte. Meine Liebste meinte lapidar, sie vermute, dass es sich um das Musée de Cluny handelt. Dieses ist in einem Palast im Stil der Renaissance, das an die erhaltenen römischen Thermen von Paris angebaut wurde, untergebracht. Das Musée de Cluny ist das nationale Mittelaltermuseum.

Römische Thermen. Renaissancepalast. Mittelalter. Jetzt ratet mal, wie wir uns entschieden haben? Richtig!

Nein, diesmal keine Schlangen. Die Sicherheitskontrolle bestand aus einem Blick in die Taschen. Das Museum war sehr gut besucht, aber nicht überlaufen.

Gute Museen machen uns glücklich. Fast so glücklich wie guter Sex. In diesem Fall strahlten wir vor Glück und hachten ohne Unterlass. Im Frigidarium, dem vollständig erhaltenen Kaltbadesaal der römischen Thermenanlage wurden die bei der Sanierung der Kathedrale Notre Dame aufgefundenen Figurenreste des mittelalterlichen Lettners ausgestellt. Wir hatten eine Doku darüber gesehen und waren äußerst entzückt, diese noch farbig gefassten Architekturreste live bewundern zu dürfen. Damit hatten wir nicht gerechnet. Wunderschöne Kapitelle nicht mehr existierender Kirchen wurden zur Bewunderung präsentiert, so wie frühmittelalterliche Elfenbeinschnitzereien, überlebensgroße, romanische und frühgotische Jesuse aus Holz, die einst an einem Kreuz in Kirchen hingen. Eine Ursula-Reliquienbüste aus Köln. Berühmte, spätmittelalterliche Wandteppiche mit Einhörnern drauf (fragt meine Liebste, sie kennt sich damit aus), Gemälde, wunderschöne Buchmalereien, prächtige Buchdeckel, verziert mit Gold und Edelsteinen. Geht hin, wenn es euch interessiert und ihr in Paris seid! Dieses Museum ist eine großartige Schatzkammer!

Und wer sich jetzt freut und denkt „Ende gut, alles gut“, der hat die Rechnung ohne die Metrostation Chatelet gemacht. Chatelet ist ein Verkehrsknotenpunkt, ein irres Gewirr aus unterirdischen Gängem, aus Laufbändern und plötzlichen Abzweigungen. Hier mussten wir umsteigen. Das Licht ist extrem grell, die Ansagen brutal laut, die Menschenmassen hetzen teilweise im Dauerlauf, als ginge es um ihr Leben. Meine Liebste, bereits am Ende ihrer Kräfte, fing an zu zittern, blieb stehen, war kurz vorm weinen, konnte nicht weiter. Gottseidank, ich weiß nicht woher, hatte ich noch ein Notlöffelchen übrig und konnte sie sanft zur Linie 11 bugsieren, wo direkt ein leerer Zug einfuhr und uns bis kurz vor unser Hotel brachte.

Achja. Abendessen. Wir hatten gehofft, in das kleine, nette Bistro im Erdgeschoss des Hotels gehen zu können. Die Energie dafür hatten wir nicht mehr. Statt dessen habe ich meine Liebste aufs Zimmer geschickt und habe ihr ein hochdosiertes CBD-Fruchtgummi verschrieben. Ich Wahnsinniger bin dann noch in den Supermarkt um die Ecke und habe uns mit letzter Kraft Kleinkram zur Notversorgung organisiert. Ich muss sehr langsam gewesen sein und der Einkauf war skurril, ich kann mich kaum noch daran erinnern. Danach fiel auch ich ins Bett.

Fazit Tag 2: Als ich mir eben meine Sätze durchlas, dachte ich spontan, dass wir eigentlich unglaublich bescheuert sind. Sind wir aber nicht, denn wir pendeln ständig zwischen dem wunderbaren Rausch des intensiven Erlebens und der Hölle der kompletten sensorischen Überreizung. Im Urlaub natürlich mehr als im Alltag. Aber auch Zuhause am Erdrand beschreibt das unser Leben...

 
Weiterlesen...

from Hannes

17.2.2025 Wie ging es weiter mit Margret, Besorgungen Es ist ein Jahr her, um diese Zeit im Februar 2024. Ich muss immer noch an sie denken. Ich bestellte von einer Versandfirma einen Bettgalgen und einen elektrischen Kissenheber. Uschi brachte für die Toilette eine Erhöhung für die Klobrille mit. Auch der Rollator kam vor der damaligen Woche ins Hinterzimmer, neben dem Kartoffeleimer. Uschi kam sehr oft nach mir, um ihrer Schwester zu helfen. Dafür kann ich ihr nicht genug danken. Sie pendelte zwischen vom Wohnort und mir hin und her. Als Margret aus Krankenhaus entlassen wurde, das war am 11.2. 2024 bekam sie von der Klinik Schmerztabletten, gut und schön. Aber trotzdem wuchs ihr Krebs an den Ovarien weiter. Die Schmerzen waren nicht mehr so stark, sie musste nach Anordnung des Arztes die Tabletten einehmen. Sie musste raus aus dem Krankenhaus, weil keine Betten mehr frei waren. Aber ich kann es nicht verstehen, das man eine krebskranke Frau aus dem Krankenhaus entlässt. Sie musste zusehen, wie sie zu Hause klarkommt. Am 18.2. 2024 bestellte ich einen Krankenfahrdienst für den 21.2.2024. Margret hatte dort einen erneuten Vorstellungstermin in der Klinik. Das Auto kam pünktlich, mit Hilfe des Rollstuhles wurde Margret in den Wagen eingeladen. Ich bekam einige Papiere, die ausgefüllt werden mussten, das tat Uschi für sie. Margret schrieb ihre Vollmacht an Uschi. Auf der Hinfahrt zur Klinik war sehr viel Verkehr und mussten über innerstädtische Straßen ausweichen. Aber wir waren pünktlich da. Um 10 Uhr wurden wir empfangen und die Ärztin nahm Margret sofort mit zur Untersuchung. Uschi und ich gingen zum hinteren Eingang des Flures und verweilten dort, wir mussten sehr lange warten bis sie aus dem Untersuchungsraum heraus kam. Sie bekam ein Bett und kam 2 Stockwerke höher in eine Abteilung für Brustkrebskranke. Dort war es heller als im Erdgeschoss und der Service besser. Margret hatte eine Nachbarin, sie verschenkte ihr ein herzförmiges Kissen als Trost. Die Dame war auch von vervierfachverschiedenen Krebsarten befallen. Sie wollte von sich aus in ein Hospiz gehen. Uschi sprach mit einer Sozialabeiterin, die ein Pflegeheim für uns aussuchen sollte, um nicht andauernd zum Krankenhaus zu fahren und in der Nähe wäre. Um zu operieren wäre es ein Risiko gewesen, Margret noch zu behandeln. Wir besuchten das Pflegeheim, es war sehr modern eingerichtet mit allem Pi-Pa- Po. Margret hatte die Pflegestufe 4. Als wir heraus kamen, bekam Uschi eine niederschmetternde Nachricht über ihr Handy, das man Margret nicht operieren könne, wegen ihres Herzschrittmachers und der Epilepsie, Es war zu spät, leider war es die Endstadion des Krebses eingetreten und Margret in ein Hospiz überwiesen, wo sie die 3 Wochen bis zu ihrem Lebensende ihrem Tode verbrachte. Bald jährt sich der Todestag vor einem Jahr. Mir kommt es so vor, als wäre es erst gestern gewesen. Auch in dieser Zeit war sie glücklich und zufrieden und hatte stehts ein Lächeln im Gesicht. Sie bekam täglich Besuch von ihren Freunden und Bekannten und von den Geschwistern und mir. Noch im Tode konnte man ein zufriedenes Gesicht von ihr erkennen. Sie hatte im christlichen Glauben an Gott von uns Abschied genommen. Warum ist meine Frau gestorben? Sie war mein rechtes Standbein und ist ist 42 Jahre mit mir durch das Leben gegangen und war froh, einen Mann kennengelernt zu haben und mit ihm durch dick und dünn gegangen. ist. Aber was soll es, ich sehe sie nicht mehr wieder als lebendige Person. Vor einigen Tagen, vieleicht vor einer Woche, erzählte mir Uschi einen wunderbaren Traum: Sie begegnete Margret, sie erzählten irgend etwas. Sie hatte angerufen und deutlich konnte Uschi die Stimme von Margret hören. Sie sagte es mir stolz in der Küche, auch sie schwärmte für Margret und war glücklich gewesen, im Traum Margret gesehen zu haben, denn es war ihre Schwester gewesen. Als die Wirklicheit wieder kam, standen Uschi und ich ohne Margret in der Küche herum.
Heute brauchte ich nicht viel zu besorgen, weil ich an einem Samstag mir alles kaufte, was ich brauchte. Lediglich Katzenfutter und Streu, 2 Tüten Milch, einige Brezeln für abends und Brotbelag. Als ich den Futternapf füllte, kam Felix heran und fraß etwas davon. Ich lag mit dem Bauch auf dem Teppich. Er kam dicht an meinen Kopf heran ohne mich zu beißen und schleckerte weiter. Kaum das ich auf dem Sofa war, kam Luna angerannt, sie brauchte ihre Streicheleinheiten. Tschüss

 
Weiterlesen...

from Hannes

16.2.2025 Endlich, Heute Morgen war Sonntag, trotzdem stand ich wieder früh auf, weil ich zu der Zeit Tabletten einnehmen musste. Sofort bereitete ich den Kaffee zu und aß die Dinkelbrötchen auf, die ich gestern noch zubereitet hatte. Sie sind weg, Ha- Ha-Ha. Bevor ich zur Kirche fuhr, wusch ich mir die Füße, versorgte die Katzen und streichelte Luna. Dann wurde es Zeit zur Kirche zu fahren. In der Einfahrt kam mir ein Großraumtaxi entgegen und musste zurück fahren, damit das Taxi zur Straße fahren konnte. Ich berührte mit einem Seitenspiegel sanft eine Hecke. Es war nichts passiert. Es waren draußen nur 0,5 Grad. Etwas wärmer war es in der Kirche. Mich beeindruckte das Lied aus dem GL 388 ein schönes Lied von Franz Schubert. Nach der Kirche fuhr ich nach Hause. Am Nachmittag ließ mir die Kommode keine Ruhe. Ich nahm die Schubladen heraus und wechselte die anderen Leisten von der alten Kommode, die im Hinterzimmer steht, aus. Mit dem Akkuschrauber ging es sehr schnell.. Nun probierte ich die Schubladen aus und es passte wunderbar an der neuen Kommode im Wohnzimmer. Dann hatte die Kommode ein vernünftiges Erscheinungsbild. Nun schob ich das kleine Sofa zur Tür hin, nahm das Kabel von Stehlampe und führte es in die Steckdose. So kann sagen, das das Wohnzimmer mit der neuen Kommode ordentlich eingerichtet ist. Das Sofa schob ich zur Wand hin. Dadurch konnte ich die Tür verschließen.

 
Weiterlesen...

from Der Emil

Es wird in meinem Leben einen zweiten Umbruch geben, dessen bin ich mir sicher. Der erste ließ sich für viele Menschen noch schönreden, ich konnte mich irgendwann mit den Verlusten abfinden.

Der jetzt drohende allerdings …

Selbst, wenn die Bundestagswahlen glimpflich ausgehen und weiterhin Demokraten (ohne C oder F, und die Nicht-Demokraten sowieso nicht) das Land regieren werden: Die internationale Lage gerät wegen eines Hamsters gerade aus den Fugen. Jetzt fehlen die Fachleute zur Überwachung, Kontrolle und Wartung von Kernwaffen in diesem einen Land. Die Kommunikation, auch unsere, ist tatsächlich zu einem Teil abhängig von Sympathiesanten faschistoider Politiker bzw. faschistischer Politiker. Es ist unerheblich, ob diese ihr Faschistsein verleugnen; ihre Taten zeigen deutlich, wes Geistes Kind sie sind.

Ich gestehe: Ich habe Angst vor den nächsten fünf Jahren …

 
Read more...

from Hannes

15.2.2025 kaum was getan, Andacht Heute Morgen stand ich schon sehr früh auf, es war 6 Uhr 15 und machte mich frisch. Ich zog mir eine andere Hose an, da die beigefarbene Hose Löcher hatte. Dann machte ich eine Kerze an und begann zu essen. Die Katzen warteten auf ihr Futter. Nun hatte ich wieder mal Flurdienst und ging mit dem Wischer über die Treppenstufen. Einige Zeit blieb mir noch und streichelte Luna. In der Küche stand auf dem Kalender eine Spalte, auf der man seine Gedanken schreiben konnte.—– Ich hoffe, das Wunder geschehen, das Margret und Luna als Engel erscheinen und mit ihnen einige schöne Stunden verbringen können. Ach wäre es schön, Margret zu knuddeln und Luna zu streicheln. —— Das waren meine Gedanken im Kalender und gucke jeden Morgen darauf. Ich nahm den blauen Beutel aus dem Schrank und tat die Lebensmittel für die Andacht hinein. Im Pfarrsaal in der Küche schnitt ich mit einem Messer die Brötchen auf und belegte sie mit Wurst ,Ei und Käse und stellte sie auf den Tisch im Pfarrsaal. Dorothee ging zur Kirche und bereitete alles für die Andacht vor und ließ die Glocken läuten. Andere Mitglieder kamen an und gingen zur Kirche hinein. Dort wurde eine Andacht gehalten, was uns zu denken gab. Nach der Andacht gingen wir hinüber zum Pfarrsaal und aßen die belegten Brötchen. Dazu gab es Kaffee. Wir kamen in der Übereinstimmung die Andachtzeiten auf einen Sonntagnachmittag ab 14 Uhr zu verlegen. Ich fegte mit einem Besen die Krümel weg und ein Mitglied wusch das Geschirr ab und verließen gemeinsam den Pfarrsaal. Heute Abend aß ich ein Teil der Brötchen, die bei der Vesper übergeblieben sind.

 
Weiterlesen...

from Michael Gisiger

Waterhouse: Echo and Narcissus

Ich kenne das Gefühl nur zu gut: Ein neues Projekt, eine knifflige Herausforderung, eine wichtige Entscheidung – und sofort denke ich, dass meine Situation einzigartig ist. Keine Erfahrungswerte, keine Vergleiche, keine Vorbilder. Doch genau dieses Denken kann zu gravierenden Fehlentscheidungen führen. Im aktuellen Harvard Business Review findet sich ein aufschlussreicher Artikel (Paywall) zum Uniqueness Bias, einer kognitiven Verzerrung, die uns glauben lässt, dass unsere Probleme oder Projekte einmalig sind. Die Autoren zeigen: Wer sich für einzigartig hält, trifft oft schlechtere Entscheidungen, unterschätzt Risiken und ignoriert wertvolle Erfahrungen anderer. [1]

Was ist der Uniqueness Bias?

Der Uniqueness Bias beschreibt die menschliche Tendenz, die eigene Situation für aussergewöhnlicher zu halten, als sie tatsächlich ist. Die Psychologie sieht darin eine weitverbreitete Verzerrung unserer Wahrnehmung: Wer glaubt, sich in einer beispiellosen Lage zu befinden, sieht keine Parallelen zu vergangenen Ereignissen und lernt weniger aus der Vergangenheit.

Diese Denkweise wird durch verschiedene Faktoren begünstigt:

  • Der „Inside View“: Wir betrachten unsere Probleme aus der Ich-Perspektive und neigen dazu, externe Vergleiche zu ignorieren.
  • Mangel an Erfahrung: Wenn wir noch nie mit einer bestimmten Situation konfrontiert waren, empfinden wir sie als neu und einmalig.
  • Das Bedürfnis nach Einzigartigkeit: Wer sein Projekt als unvergleichlich darstellt, erhält oft mehr Aufmerksamkeit und Unterstützung – ein starker Anreiz, die Einzigartigkeit zu betonen.

Der Uniqueness Bias ist auch eng mit „schnellem Denken“ (System 1 in Daniel Kahnemans Theorie) verbunden. Unser Gehirn neigt dazu, Entscheidungen ohne tiefgehende Analyse zu treffen, um Energie zu sparen.

Die Folgen: Warum der Uniqueness Bias uns schadet

Die Annahme, in einer einzigartigen Lage zu sein, hat oft erhebliche Konsequenzen. Der Artikel zeigt, dass sich dieser Bias in mehreren Bereichen negativ auswirkt:

1. Schlechtere Entscheidungen im Beruf Viele Führungskräfte oder Unternehmerinnen glauben, dass ihre Herausforderungen ohne Beispiel sind. Das kann dazu führen, dass sie bestehende Erfahrungen ausblenden und stattdessen Entscheidungen auf Basis von Annahmen oder Intuition treffen.

Ein Beispiel aus der Studie: In einer Analyse von 1'300 IT-Projekten zeigte sich, dass Managerinnen und Manager, die ihre Projekte als „einzigartig“ einstuften, wesentlich höhere Kostenüberschreitungen hatten. Die Konsequenz: Wer sich für etwas Besonderes hält, plant schlechter und kalkuliert Risiken falsch.

2. Fehlentscheidungen im Privatleben Der Uniqueness Bias betrifft nicht nur Unternehmen, sondern auch unser tägliches Leben. Menschen neigen dazu, ihren eigenen Weg zu gehen, anstatt auf bewährte Strategien zurückzugreifen.

Denken wir an jemanden, der sich auf einen neuen Job bewirbt. Statt sich mit Personen auszutauschen, die bereits erfolgreiche Bewerbungsprozesse durchlaufen haben, verlässt sich die Person ausschliesslich auf ihre eigenen Vorstellungen. Sie schreibt ein Motivationsschreiben, ohne bewährte Strategien zu recherchieren, und geht unvorbereitet ins Vorstellungsgespräch. Das kann dazu führen, dass sie Chancen verpasst, typische Fehler macht oder unrealistische Gehaltsvorstellungen hat – schlicht, weil sie denkt, dass ihr Bewerbungsprozess einzigartig ist.

3. Verpasste Lernchancen Wer glaubt, dass seine Herausforderung beispiellos ist, sucht nicht nach Analogien und entgeht damit wertvollen Erkenntnissen. In Wirklichkeit hat fast jede Problemstellung eine Entsprechung. Wer beispielsweise eine neue Sprache lernen möchte, könnte von den bewährten Methoden anderer Sprachlernender profitieren – etwa durch den Einsatz von Eselsbrücken, gezielte Immersion oder Sprachtandems. Doch wer denkt, dass sein eigener Lernprozess völlig individuell ist, läuft Gefahr, ineffiziente Wege zu wählen und langsamer Fortschritte zu machen.

Wege aus der Einzigartigkeitsfalle: Die „Outside View“

Die gute Nachricht ist: Der Uniqueness Bias lässt sich überwinden. Der Schlüssel dazu ist die „Outside View“, also die bewusste Entscheidung, die eigene Situation von aussen zu betrachten.

1. Suche aktiv nach Analogien Frage dich: Gab es ähnliche Fälle in der Vergangenheit? Wer hatte schon einmal mit einem vergleichbaren Problem zu tun? Selbst wenn es keine 1:1-Entsprechung gibt, lassen sich oft Parallelen finden.

2. Zerlege das Problem in Module Falls keine offensichtlichen Vergleichsfälle existieren, kann es helfen, eine Situation in kleinere Bestandteile zu zerlegen. Einzelne Aspekte lassen sich dann mit anderen Erfahrungen abgleichen.

3. Nutze bewährte Methoden zur Entscheidungsfindung Um den Uniqueness Bias zu umgehen, bieten sich verschiedene Techniken an:

  • Die 10-10-10-Methode: Betrachte eine Entscheidung aus drei Zeithorizonten – Wie wirst du in 10 Minuten, 10 Monaten und 10 Jahren darüber denken? [2]
  • Szenario-Denken: Entwickle mehrere mögliche Zukünfte: Was ist das beste, das schlechteste und das wahrscheinlichste Szenario?
  • Der Perspektivwechsel („Inversion“): Frage dich nicht nur, wie du Erfolg haben kannst, sondern auch, wie du scheitern würdest – und vermeide diese Fehler. [3]
  • Die Feynman-Methode: Erkläre dein Problem so, als würdest du es einem Kind erklären. Wenn du Schwierigkeiten hast, es klar zu formulieren, hast du es wahrscheinlich noch nicht vollständig durchdacht.

Fazit: Niemand ist so einzigartig, wie er denkt

Der Uniqueness Bias ist eine tückische kognitive Verzerrung, die uns daran hindert, aus bestehenden Erfahrungen zu lernen. Besonders im Beruf und im Privatleben kann die Annahme, dass eine Situation beispiellos sei, zu gravierenden Fehlentscheidungen führen. Doch wer bewusst nach Analogien sucht, die eigene Perspektive erweitert und erprobte Methoden anwendet, kann fundiertere und bessere Entscheidungen treffen.

Die wichtigste Erkenntnis ist simpel: Fast nichts ist wirklich einzigartig. Und das ist eine gute Nachricht, denn es bedeutet, dass wir nicht bei null anfangen müssen.


Fussnoten [1] Der Artikel im HBR basiert auf der Studie Uniqueness Bias: Why It Matters, How to Curb It (2024) von Flyvbjerg et al., die auch den Artikel verfasst haben: https://dx.doi.org/10.2139/ssrn.4924942.

[2] Die 10-10-10-Methode wurde von der Autorin und Journalistin Suzy Welch entwickelt. Sie beschreibt diese Entscheidungsfindungstechnik ausführlich in ihrem Buch 10-10-10: A Life-Transforming Idea (deutschsprachige Ausgabe: 10 Minuten, 10 Monate, 10 Jahre: Die neue Zauberformel für intelligente Lebensentscheidungen).

[3] Charlie Munger, der verstorbene, langjährige Geschäftspartner von Warren Buffett, beschreibt Inversion ausführlich in seinem Buch Poor Charlie's Almanack.

Bildquelle John William Waterhouse (1849–1917): Echo and Narcissus, Walker Art Gallery, Liverpool, Public Domain.

Disclaimer Teile dieses Texts wurden mit Deepl Write (Korrektorat und Lektorat) überarbeitet. Für die Recherche in den erwähnten Werken/Quellen und in meinen Notizen wurde NotebookLM von Google verwendet.

Topic #ProductivityPorn

 
Weiterlesen...

from BeiZero

В этой статье я попробую показать соотвествие между между математическими доказательствами и программами, а так же попытаюсь ненавязчиво ввести читателя в синтаксис Agda.

#agda

И да, эта статья тоже будет типо DRAFT и я ее буду дополнять.

Соответствие Карри-Ховарда устанавливает соответствие между типизированным лямбда исчислением и интуиционистской логикой. Типы соответствуют высказываниям. Если мы построим значение определённого типа, то мы так же докажем высказываение соответствующее этому типу. Поскольку типы являются высказываниями, а значения являются доказательствами, конструкторы для типа соответствуют правилам вывода для соответствующего предположения.

В таблице ниже соответствие представлено более наглядно:

Логические системы Языки программирования
Высказывание Тип
Доказательство высказывания P Терм(выражение) типа P
Утверждение P доказуемо Тип P обитаем(∃ p ∈ P)
Импликация P ⇒ Q Функциональный тип P → Q
Конъюнкция P ∧ Q Тип произведения(пары) P × Q
Дизъюнкция P ∨ Q Тип суммы (размеченного объединения) P + Q
Истинная формула Единичный тип (⊤)
Ложная формула Пустой тип (⊥)
Квантор всеобщности ∀ Тип зависимого произведения (Π-тип)
Квантор существования ∃ Тип зависимой суммы (Σ-тип)

Модули

Определим модуль:

{-# OPTIONS --safe #-}
module CurryHoward where

Имя модуля на верхнем уровне должно соответствовать названию файла, а вложенные модули могут называться как угодно или даже не иметь названия. Тут так же могут быть указаны опции компилятора, например, очень частая опция —safe заставляет компилятор убедиться, что выключены другие опции, которые могут вызывать противоречия и отключает возможность делать постулаты, а так же проверяет, что все импорты тоже “безопасны”.

Единичный тип

Определим единичный тип как тип с одним конструктом:

data ⊤ : Set where 
    tt : ⊤ 

(подробнее про объявление типов)

Пустой тип

Определим пустой тип как тип без конструкторов:

data ⊥ : Set where 

Здесь же определим элиминатор пустоты

⊥-elim : ∀ {A : Set}  → ⊥ → A  
⊥-elim () -- это так называемый absurd pattern, который можно использовать когда нет ни одного значения которое можно было бы передать в эту функцию

(подробнее про Absurd Pattern)

Определим отрицание, отрицание для типа A будет означать функцию которая A в пустой тип ⊥

¬_ : Set → Set 
¬ A = ⊥

Функциональный тип как импликация

Определим функциональный тип и покажем, что он соотвествует импликации:

-- true ⇒ true 
f₁ : ⊤ → ⊤ 
f₁ tt = tt 

-- false ⇒ true 
f₂ : ⊥ → ⊤ 
f₂ _ = tt 

-- false ⇒ true можно так же доказать через элиминатор пустоты
f₂' : ⊥ → ⊤ 
f₂' x = ⊥-elim x 

-- false ⇒ false 
f₃ : ⊥ → ⊥ 
f₃ x = x 

-- true ⇒ false невозможно определить т.к. нет способа сконструировать пустой тип
-- f₄ : ⊤ → ⊥ 
-- f₄ = ? 

-- ¬ true тоже невозможно определить т.к. нет способа сконструировать пустой тип
-- f₄' : ¬ ⊤ 
-- f₄' = ? 

Ну и давайте на пример тавтологии A ⇒ (B ⇒ A) покажем как можно использовать явный и не явный полиморфизм

-- Явным образом
taut : (A B : Set) → A → (B → A) 
taut T₁ T₂ t₁ t₂ = t₁ 

-- Вызывать придется с явным указанием типов 
taut-ex : ⊥ → (⊥ → ⊥)
taut-ex = taut ⊥ ⊥ 

-- Эквивалентная запись 
taut₂ : (A : Set)(B : Set) → A → (B → A) 
taut₂ T₁ T₂ t₁ t₂ = t₁ 

-- Эквивалентная запись 
taut₃ : (A : Set) → (B : Set) → A → (B → A) 
taut₃ T₁ T₂ t₁ t₂ = t₁ 

-- Так же можно добавлять квантор всеобщности 
taut₄ : ∀ (A : Set) → (B : Set) → A → (B → A) 
taut₄ T₁ T₂ t₁ t₂ = t₁ 

-- Эквивалентная запись 
taut₅ : ∀ (A B : Set) → A → (B → A) 
taut₅ T₁ T₂ t₁ t₂ = t₁ 

-- Неявный образом
taut' : {A B : Set} → A → (B → A) 
taut' t₁ t₂ = t₁ 

-- Тогда типы можно передать или не передавать
taut'-ex₁ : ⊥ → (⊥ → ⊥)
taut'-ex₁ = taut' {⊥} {⊥} -- передаются неявные параметры в фигурных скобках, если нужно

-- Или передать один, причем можно указать какой
taut'-ex₂ : {A : Set} → A → (⊥ → A)
taut'-ex₂ = taut' {B = ⊥}

-- В целом можно делать все тоже самое, что и с круглыми скобками -- добавлять стрелочки и квантор всеобщности, и даже получать неявные параметры и использовать их в функции
taut'₂ : {A : Set} → ∀ {B : Set} → A → (B → A) 
taut'₂ {B = T₂} t₁ t₂ = t₁ --тут можно использовать T₂

-- Если совсем безумствовать, то с ума можно сходить очень по разному
taut'₃ : ∀ (A : Set) → {B : Set} → A → (B → A) 
taut'₃ T₁ t₁ t₂ = t₁ 

-- Вообще-то даже Set можно не писать, если писать ∀, но в таком общем коде лучше писать(можно смело писать, где из контекста понятен конкретный тип) 
-- т.к. там есть нюансы с вложенностью типов в типы
taut'₄ : ∀ A → ∀ {B} → A → (B → A) 
taut'₄ T₁ = λ t₁ t₂ → t₁ --а еще лямбды можно писать

(еще подробнее про объвление функций)

Тип произведения (пары)

Определим тип пары, который соотвествует коньюнкции

data _×_ (P : Set) (Q : Set) : Set where
    pair : P → Q → (P × Q)

И тогда можно показать, что

-- P ∧ Q ⇒ P
×-elim₁ : {P Q : Set} → (P × Q) → P
×-elim₁  (pair p _) = p

-- P ∧ Q ⇒ Q
×-elim₂ : {P Q : Set} → (P × Q) → Q
×-elim₂  (pair _ q) = q

Тип суммы

Определим тип суммы, который соотвествует дизъюнкции

data _+_ (P Q : Set) : Set where
   Left : P → P + Q
   Right : Q → P + Q

И тогда можно показать, что

+-elim : {A B C : Set} → (A → C) → (B → C) → (A + B) → C
+-elim ac bc (Left a) = ac a
+-elim ac bc (Right b) = bc b

Сигма тип(зависимая сумма)

А вот сейчас будет сложно. Во первых, потому что зависимые типы, во вторых, мы незаметно введем уровни для типов Set(в целом все что нужно знать это Set i имеет тип Set (i + 1), сделано так, чтобы обойти парадокс Рассела), а в третьих, сумма это теперь пара, т.е. фактически зависимая сумма это обобщение произведения, и понимайте это как хотите(если я сам это когда-нибудь осознаю обязательно расскажу).

open import Agda.Primitive

record Σ {i j} (A : Set i) (P : A → Set j) : Set (i ⊔ j) where 
  constructor _,_
  field
    fst : A    
    snd : P fst 

(подробнее про record'ы и про уровни)

В стандартной билиотеке есть еще несколько удобных синтаксисов для Σ-типа

Σ-syntax : ∀ {a}{b} (A : Set a) → (A → Set b) → Set (a ⊔ b)
Σ-syntax = Σ

syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B

∃ : ∀ {a}{b}{A : Set a} → (A → Set b) → Set (a ⊔ b)
∃ = Σ _

∃-syntax : ∀{a}{b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
∃-syntax = ∃

syntax ∃-syntax (λ x → B) = ∃[ x ] B

Фактически Σ-тип можно воспринимать как значение типа A и зависящий от этого значения предикат P. Например

-- Для любого типа B существует тип A такой, что существует функция B → A
Σ-ex : ∀ {B} → Σ Set (λ A → B → A)
Σ-ex = ⊤ , λ _ → tt

-- Или тоже самое используя синтаксис Σ
Σ-ex' : ∀ {B} → Σ[ A ∈ Set ] (B → A)
Σ-ex' = ⊤ , λ _ → tt

-- Или тоже самое используя синтаксис ∃
Σ-ex'' : ∀ {B} → ∃[ A ] (B → A)
Σ-ex'' = ⊤ , λ _ → tt

Пи тип(зависимое произведение)

Пи-тип, он же тип зависимой функции, он же тип зависимого произведения, можно использовать и без дополнительных определений т.к. фактически он зашит в Agda, но чисто формально его можно представить так:

Π : ∀ { n m }(A : Set n)(P : A → Set m) → Set(m ⊔ n)
Π A P = (x : A) → P x

Тип Π можно воспринимать как квантор всеобщности где для любого элемента типа A истинен предикат P. Например:

--Для любого типа существует функция из него в непустое множество
Π-ex : Π Set (λ A → A → ⊤)
Π-ex = λ _ _ → tt

Зависимые типы

Зависимые типы это одна из ключевых фишек Agda позволяющая конструировать функции в которых типы зависят от термов или даже типы от типов, данные типы можно воспринимать в том числе как предикаты или отношения, а их обитаемость как доказательства свойств термов.

Например, можно определить равенство Лейбница, когда x = y, если для любого предиката P: P x = P y.

_==_ : ∀ {A : Set} (x y : A) → Set₁
_==_ {A} x y = Π (A → Set) (λ p → (p x → p y))
-- определение эквивалентно ∀ (P : A → Set) → P x → P y

и тогда можно показать рефлексивность ==

refl-== : ∀ {A : Set}{x : A} → x == x
refl-== P Px = Px

На самом деле в Agda равенство термов и типов обычно определяется иначе, но кажется это хороший пример, чтобы показать как работают зависимые типы.

Вместо послесловия

Надеюсь было не слишком абстрактно, специально не хотелось вводить дополнительные типы, чтобы сконцентрироваться именно на соответствии логических операций и типов. Далее, возможно, хотелось бы разобрать такую штуку как Decidability т.к. иногда нужно с уровня типов опуститься на уровень термов, чтобы, например, факт обитаемости того или иного типа сопоставить с true и false, как это было в статье про лямбда исчисление в if_then_else

Используемые символы и их коды:

Символ Код
\to
\and
\or
λ \lambda
∣ ∈ \in
\exists
× \x
∣ ⊤ \top
\bot
\forall
Π \Pi
Σ \Sigma
\=>
\_n
 
Read more...

from Cedaras Couch

Kurze Rezension zu : "Der Katze ist es ganz egal" von Franz Organdl

Ein bezauberndes Buch über ein transgender Kid, das eines morgens aufwachte, und wußte, dass sie jetzt Jennifer heißt.

Ich habe es als Hörbuch via Libby ausgeliehen gehabt, was gut 90min lang ist. Im Text finden sich ein paar österreichische Worte, die allerdings im Kontext nicht erklärt werden müssen.

Man bekommt gut mit, welche Probleme Jennifer zuerst mit ihrer Entscheidung gegenüber ihrer Umwelt hat, aber glücklicherweise stehen ihre Freunde zu ihr, und die Klassenkameraden verhalten sich nicht ablehnend. Von Stella, dem Mädchen aus dem anderen Zweig der Schule, erhält Jennifer ein wenig Hilfe in der Art, wie sich ein Mädchen kleidet.

Jennifers Vater hat zuerst etwas Probleme mit der Entscheidung seines Kindes, aber die Mutter ist da offener und akzeptiert es schneller. Das drolligste sind die Großeltern. Zuerst dachte ich, sie seien ablehnend, was aber nicht der Fall war.

Das Ende ist positiv und hinterläßt ein warmes „Awww“ im Leser.

Es ist sehr verständlich, dass das Buch 2021 einige Preise bekommen hat. Der Verlag empfiehlt das Buch ab 9 Jahre. Es ist aber auch sehr gut für Erwachsene geeignet.

Erschienen bei Klett: https://www.klett-kinderbuch.de/buecher/details/der-katze-ist-es-ganz-egal.html

 
Weiterlesen...

from BeiZero

Эта статья будет публичной, но в статусе DRAFT, скорее всего я буду ее дополнять и пересматривать, пока тут какие-то базовые определения и доказательство того, что у (λx.xx)(λx.xx) нет нормальной формы. Скорее всего тут есть некоторые неточности и даже ошибки, буду исправлять в процессе.

#agda #lambdacalculus

Определим модуль и импортируем необходимые модули

module LambdaCalc where

open import Data.Nat
open import Data.Bool hiding (_≟_)
import Relation.Binary.PropositionalEquality as Eq
open Eq hiding (subst)
open Eq.≡-Reasoning
open import Relation.Nullary.Decidable 
open import Data.Empty using (⊥; ⊥-elim) 
open import Data.Unit using (⊤; tt) 
open import Data.Product

Начнем с определения термов лямбда-исчисления. Для простоты будем использовать индексы де Брауна для переменных, это когда переменные не именуются, а нумеруются (индексируются), индекс показывает, сколько лямбд назад переменная была связана:

λx. (λy. x y) ↔ λ (λ 1 0) λx. x (λy. x y y) ↔ λ 0 (λ 1 0 0)

-- Определение термов лямбда-исчисления
data Λ : Set where     
  _`  : ℕ → Λ          -- Переменная
  λ'_  : Λ → Λ         -- Лямбда-абстракция 
  _∘_  : Λ → Λ → Λ     -- Применение 

Подстановка нужна для реализации бета-редукции:

-- Подстановка терма вместо переменной
subst : Λ → ℕ → Λ → Λ 
--Если переменная равна той же вместо которой мы подставляем, то подставляем, иначе не подставляем
--Как работают ⌊_⌋ и ≟ надо будет как-нибудь объяснить, но пока поверьте, что это такое хитрое сравнение на равенство
subst (x `) y s = if ⌊ x ≟ y ⌋ then s else (x `)
--Внутрь лямбда абстрации тоже можем подставить(увеличиваем на единицу значение искомого индекса т.к. погружаемся глубже)
subst (λ' t) y s = λ' (subst t (suc y) s)
--Можем подставить с обеих сторон применения
subst (t ∘ u) y s = (subst t y s) ∘ (subst u y s)

Теперь определим одношаговую бета-редукцию:

-- Одношаговая бета-редукция
data _→β_ : Λ → Λ → Set where
  --Если есть абстракция и применение, то можем применить подстановку
  beta : ∀ {t u} → ((λ' t) ∘ u) →β (subst t 0 u)
  --Можно редуцировать левую часть применения
  app₁ : ∀ {t t' u} → t →β t' → (t ∘ u) →β (t' ∘ u)
  --Можно редуцировать правую часть применения
  app₂ : ∀ {t u u'} → u →β u' → (t ∘ u) →β (t ∘ u')
  --Можно редуцировать под лямбда абстракцией
  lam  : ∀ {t t'} → t →β t' → (λ' t) →β (λ' t')

Определяем многошаговую редукцию:

-- Многошаговая редукция (→β*)
data _→β*_ : Λ → Λ → Set where
  refl : ∀ {M} → M →β* M
  step : ∀ {M N P} → M →β N → N →β* P → M →β* P

Определяем нормальную форму:

Normal : Λ → Set
--Переменная уже в нормальной форме
Normal (x `)    = ⊤
--Если есть лямбда абстракция и применение к ней, то это редекс т.е. можно использовать подстановку
Normal ((λ' _) ∘ _) = ⊥
--Применение имеет нормальную форму, если оба аргумента имеют нормальную форму
Normal (M ∘ N)  = Normal M × Normal N
--Лямбда абстракция имеет нормальную форму, если терм внутри имеет нормальную форму
Normal (λ' M)    = Normal M
-- Определение Ω = (λx.xx)(λx.xx)
Ω : Λ
Ω = (λ' ((0 `) ∘ (0 `))) ∘ (λ' ((0 `) ∘ (0 `)))

--xx не редуцируется
l1 : ∀ {x t} → ((x `) ∘ (x `)) →β t → ⊥ 
l1 (app₁ ())  --интересно, кстати, почему этого кейса достаточно и Agda не требует еще разобрать app₂
--() это так называемый absurd pattern, т.е. не существует такой β-редукции, которую мы могли бы применить к левой части применения

--λx.xx не редуцируется 
l2 : ∀ {x t} → (λ' ((x `) ∘ (x `))) →β t → ⊥ 
l2 (lam b) = l1 b

--(λx.xx)(λx.xx) редуцируется в себя
l3 : Ω →β Ω 
l3 = beta

--Ω всегда редуцируется в Ω
Ω→βΩ : ∀ T → Ω →β T → T ≡ Ω
--Если использовать применение, то Ω переходит в себя по определению
Ω→βΩ t beta = refl
--Если мы редуцировали левую часть применения, то это могла быть только λx.xx, что невозможно
Ω→βΩ _ (app₁ b) = ⊥-elim (l2 b)
-- А вот тут почему-то требует app₂ проверить :) 
Ω→βΩ _ (app₂ b) = ⊥-elim (l2 b)

Ну и собственно доказываем, что у Ω нет нормальной формы

--У Ω нет нормальной формы
no-normal-form : ∀ {N} → Ω →β* N → Normal N → ⊥ 
--Тут это другой refl из многошаговой β-редукции
no-normal-form refl ()
--Если это была редукция, то Ω перешла в себя
no-normal-form (step beta steps) nf = no-normal-form steps nf
--Остальные варианты невозможны
no-normal-form (step (app₁ t) steps) nf = l2 t
no-normal-form (step (app₂ t) steps) nf = l2 t

Используемые символы и их коды:

Символ Код
\to
Λ \Lambda
λ \lambda
\top
\bot
\bN
\o
\forall
\clL
\clR
\?=
_1
_2
β \beta
Ω \Omega
 
Read more...