В этой статье я попробую показать соотвествие между между математическими доказательствами и программами, а так же попытаюсь ненавязчиво ввести читателя в синтаксис 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

Эта статья будет публичной, но в статусе 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

Die beiden tragischen Anschläge in Magdeburg und Aschaffenburg werden derzeit auf perfide Weise von den rechtsaußen Parteien emotionalisiert und instrumentalisiert, obwohl die Eltern der Opfer darum gebeten haben, dies nicht zu tun. Dabei werden die Rechten mit Nachdruck von diversen Medien unterstützt, die bereits eine lange Tradition der Brandstiftung pflegen. Mittlerweile gesellt sich auch der ÖRR immer mehr dazu. Ob aus vorauseilendem Gehorsam, oder weil die rechtsextremen Parolen in den Redaktionen auch immer mehr verfangen, lässt sich nur noch schwer unterscheiden. Das Narrativ, das Migration gerade unser allergrößtes Problem sei und der Untergang des Abendlandes drohe, plättet gerade sämtliche anderen Themen und Probleme in der Berichterstattung. Wahlkampf sei Dank. Wohnungsnot, Klimakrise, Inflation und Armut, Ukraine-Krieg usw., spielt gerade alles keine Rolle. Die Angst frisst den Verstand auf.

Es sollte jedem klar sein, dass es den Rechten nicht vorrangig um die Begrenzung der Migration geht, sondern sie wissen, dass sie bei der Wahl der “illegalen Migranten” als Feindbild sehr wahrscheinlich eine große Zustimmung in der Bevölkerung bekommen. Sicherheit ist ein menschliches Grundbedürfnis, und die Angst diese zu verlieren ist so tief verankert, dass sie sich extrem leicht von Populisten nutzen lässt, um viele Menschen zu manipulieren. Der Wunsch nach einfachen Lösungen in einer immer komplexer werdenden Welt, bietet den Haudrauf-Maulhelden in der Politik zusätzlich eine Klaviatur, die sie gerne bespielen.

Wenn ihnen dieser Schritt der Migrationsbegrenzung gelingt, inklusive der weiteren Normalisierung rechtsextremer Positionen, können sie das als Sprungbrett nutzen,um ihre Macht weiter auszubauen. Und dann sind sehr bald die bereits hier legal lebenden Menschen mit Migrationshintergrund dran. Danach vielleicht Kranke, Behinderte, Homosexuelle, und irgendwann auch Journalisten, Lehrer, Wissenschaftler, Intellektuelle und andere Gruppen, die nicht in die völkisch-nationale Ideologie hineinpassen.

Die Idee, dass Freiheit immer die Freiheit der Andersdenkenden ist, ist mit faschistischer Ideologie nicht vereinbar.

In was für einer Gesellschaft wollen wir leben?

Einer Gesellschaft, die das Grundgesetz, die Menschenrechte und ein solidarisches Miteinander wertschätzt? Oder einer Gesellschaft, in der das Recht des Stärkeren gilt?

In einer Gesellschaft, die sich durch die Einflüsse anderer Kulturen bereichert und beschenken lässt und über den Tellerrand hinausschaut? Oder in einer Gesellschaft, die sich abschottet und alles Fremde als minderwertig ansieht?

Das Problem heißt Rassismus, und dieser zieht sich systematisch durch die Strukturen im Land. Alle Regierungen der letzten Jahrzehnte haben nicht die nötigen Schritte unternommen, um Migration und Integration menschenwürdig zu gestalten. Stattdessen wurde das Asylrecht immer weiter verschärft, aus Angst vor zunehmender Gewalt von rechts. Der latente Rassismus in unserer Gesellschaft hat dafür gesorgt, dass wir unzureichende Strukturen haben, die letztlich die Probleme verursachen, die wiederum Wasser auf die Mühlen der Menschenfeinde sind. 2015 wäre eine Chance gewesen, grundlegende und nachhaltigere Struktur-Änderungen zu schaffen. Frau Merkels “Wir schaffen das” war damals ein wichtiger Impuls, aber nicht nachhaltig. Die meiste Arbeit wurde vor Ort von Freiwilligen in den Kommunen aufgefangen.

Natürlich schafft Migration auch Probleme und sorgt für Konflikte, sei es bei der Wohnungssuche oder anderweitig. Und das sind Probleme, die es zu lösen gilt. Aber Migration an sich ist nicht das Problem.

Dieses Narrativ gilt es zu durchbrechen, wenn wir nicht sehr bald in einem Land aufwachen wollen, in dem auch die Nicht-Migranten nicht mehr in Würde und Freiheit leben können.

---

Diskussion ist in diesem Thread möglich: https://social.tchncs.de/@marcr/113925349963168208

Wie holen wir uns die Zukunft zurück?

Der seltsame Retro-Fetischismus des Trumpismus/Elonismus – und was wir dem entgegensetzen können

Vom allgemeinen Zukunftsoptimismus der 1950er und 1960er Jahren sind wir in der westlichen Welt heute weit entfernt. Mein Eindruck ist, dass es viele Menschen in den westlichen Ländern gibt, die das Gefühl haben, dass wir in einem Jahrzehnt des Übergangs leben: Das Alte, die etablierte Wohlstandsordnung nach dem Zweiten Weltkrieg, ist vorüber – aber das Neue ist noch nicht da.

Auch die politische Weltlage passt in dieses Bild: Der aktuelle US-Präsident Donald Trump ist 1946 geboren und damit im selben Jahr wie Bill Clinton, der 1993 zum Präsidenten gewählt wurde.

Mit ihm ist ein eigentümliches Programm gewählt worden: Unterstützt von Milliardären wie Elon Musk und Peter Thiel, der 2009 ausführte, dass er nicht mehr daran glaube, dass Freiheit und Demokratie kompatibel seien. Damals forderte Thiel, Libertäre wie er sollten sich von Staaten abwenden und ihre eigenen Strukturen auf den Weltmeere, im Weltraum oder Cyberspace aufbauen. Inzwischen scheint er einen anderen Plan zu verfolgen: Statt neue libertäre Anti-Staaten zu gründen, in denen Superreiche ungestört von Steuern und Solidarität leben können, sollen die USA nach seinen Vorstellungen umgeformt werden.

Stilistisch und Ästhetisch fällt auf, dass das Trump-Lager nicht einmal den Versuch unternommen hat, eine Zukunftsvision zu kommunizieren. „Make America Great Again” bezieht sich auf die Vergangenheit – und daraus wurde auch ästhetisch kein Hehl gemacht. Der Wählerschaft wird Trump als ein zurück in die USA der 1950er bis 1980er verkauft, wie nostalgische Wahlkampfvideos des Trump-Lagers zeigen.

Trump-Wahlkampfvideo „National Revival”, unter anderem von Elon Musk verbreitet

Was also hatten die 1950er bis 1980er, das sie als Sehnsuchtsort so attraktiv macht? Vielleicht auch eine Vision einer besseren Zukunft, eines besseren Lebens für alle. Nicht nur die politische Rechte scheitert daran, eine Vision für die Zukunft anzubieten, weshalb sie uns eine Reise in die Vergangenheit als nationales Wiederaufblühen verkauft. Auch Liberale und Linke haben es seit Jahrzehnten nicht geschafft, eine Vision zu zeichnen, hinter der sich Menschen versammeln, die zusammenschweißt und Menschen das Gefühl gibt, mit ihrem Einsatz zu einem besseren Morgen beizutragen.

Seit Helmut Schmidts berühmten Satz „Wer Visionen hat soll zum Arzt gehen“ hat ihn niemand so sehr mit Leben gefüllt wie Ex-Kanzlerin Angela Merkel. Sie hat nicht geführt, sondern verwaltet. Und Olaf Scholz hat es geschafft, dieses Erbe noch einmal zu übertrumpfen. Merkel und Scholz waren Anti-Kennedys, dessen wohl berühmteste Sätze neben „Ich bin ein Berliner“ die folgenden waren:

„We choose to go to the Moon in this decade and do the other things, not because they are easy, but because they are hard; because that goal will serve to organize and measure the best of our energies and skills, because that challenge is one that we are willing to accept, one we are unwilling to postpone, and one we intend to win, and the others, too.“ John F. Kennedy

Was also könnte ein Bild einer lebenswerten Zukunft und Vision sein? „Eine Zukunft, in der man nur etwas später stirbt und bis dahin mehr Fahrrad fährt, ist keine“ zitiert DIE ZEIT den deutsch-österreichischen Journalisten und Autor Wolf Lotter. Die Vision, die der Autor des Artikels, Ulrich Machold, uns anbietet, klingt sehr bescheiden. „Ein Land, das wieder funktioniert, von Zügen bis zu Bürgerämtern, und das zumindest in der Nähe des technisch neuesten Stands der Dinge. Ein Land, das keine Panikattacke bekommt, wenn der Verbrennungsmotor vom Fortschritt überholt wird, weil es auch andere Stärken hat.“

Vielleicht ist eine bescheidene Vision auch besser als gar keine.

Hier wird gemeinsam die Predigt von Bischöfin Mariann ins Deutsche übertragen. https://pad.gwdg.de/50UqgfbOQaCbU4ArQqnPXA

#fedikirche

2 Tassen Mehl ¾ Tasse Wasser 2 El Olivenöl 1 Tl Salz Kneten, teilen in 12 kleine Bällchen, sehr dünn ausrollen, auf Backpapier oder Backfolie bei 240° ca. 5-7min backen.  Zum Teilen mit anderen

Ulrike Leininger

Gottes Segen komme zu uns Frauen, dass wir stark sind in unserer schöpferischen Kraft, dass wir mutig sind in unserem Recht. dass wir Nein sagen, wo es nötig ist, dass wir Ja sagen, wo es gut ist. Gottes Segen komme zu uns Frauen, dass wir schreien, wo Unrecht ist, dass wir schweigen, wo Entsetzen ist. Gottes Segen komme zu uns Frauen, dass wir Weisheit suchen und finden, dass wir Klugheit zeigen und geben. Gottes Segen komme zu uns Frauen, dass wir die Wirklichkeit verändern, dass wir das Lebendige fördern. Dass wir Gottes Mitstreiterinnen sind auf Erden.

(Hanna Strack)

Chaos ist gut

Chaos macht Angst aber Chaos ist auch eine Chance.

Der brennende, sehnende, fühlende Mensch will an den Rand des inneren Chaos geführt werden, um die Chance zu bekommen – abseits der ausgetretene Pfade der „Normalen“ – es zu ordnen. Nicht nach den Normen des Außens, sondern nach dem Kompass des Inneren – dem Grundgefühl, dem schon immer geahnten Schicksal.

Diejenigen, die den Rand des inneren Chaos nie erreichen fühlen sich nicht selten als hätten sie ihr Leben schon gelebt, bevor es ganz vorbei ist.

For those who are doubting themselves: Sing, let your heart soar, sing forever Sad and so happy, feelings flow over, now Our world is full of all kinds of colors Closing my eyes, I still can see the stars …. Flowers are blooming, oh, it’s beautiful Sing, sing, sing! — Belle, Million Miles Away

TEMA Golf ist Ihr Experte für individuelle und Gruppen-Golfreisen weltweit. Unser erfahrenes Team bietet maßgeschneiderte Lösungen, um unvergessliche Erlebnisse auf den schönsten Golfplätzen dieser Welt zu garantieren. Mit unserem Fokus auf Qualität und Flexibilität sorgen wir für einzigartige Golfreisen. Entdecken Sie mit uns die Welt des Golfsports!

Einzigartiges Abenteuer: Golfreise Südafrika

Südafrika ist eine außergewöhnliche Golfdestination, die durch ihre atemberaubenden Landschaften, erstklassigen Golfplätze und faszinierende Tierwelt begeistert. Von den Küsten des Westkaps bis hin zu den majestätischen Drakensbergen bietet das Land eine unvergleichliche Vielfalt an Golfplätzen, die Spieler aller Niveaus beeindrucken.

Berühmte Anlagen wie der Gary Player Country Club und Leopard Creek verbinden anspruchsvolle Spielbedingungen mit spektakulären Aussichten auf die afrikanische Wildnis. Neben dem Golfen haben Besucher die Möglichkeit, unvergessliche Safaris zu erleben, Weinproben in den besten Weingütern der Region zu genießen oder historische Städte wie Kapstadt zu erkunden.

Ihre Golfreise Südafrika wird zu einer perfekten Mischung aus sportlicher Herausforderung, kulturellen Entdeckungen und luxuriöser Entspannung. Südafrika bietet Golfern ein einzigartiges Erlebnis, das Natur, Abenteuer und Golfgenuss auf höchstem Niveau vereint.

Lassen Sie sich von der Magie dieses Landes verzaubern und erleben Sie eine Golfreise, die Sie nie vergessen werden. Von der spektakulären Tierwelt bis zu erstklassigen Golfplätzen ist Südafrika eine Destination, die jeden Golfliebhaber begeistern wird.

Einzigartiges Abenteuer: Golfreise Südafrika

Südafrika ist eine außergewöhnliche Golfdestination, die durch ihre atemberaubenden Landschaften, erstklassigen Golfplätze und faszinierende Tierwelt begeistert. Von den Küsten des Westkaps bis hin zu den majestätischen Drakensbergen bietet das Land eine unvergleichliche Vielfalt an Golfplätzen, die Spieler aller Niveaus beeindrucken.

Berühmte Anlagen wie der Gary Player Country Club und Leopard Creek verbinden anspruchsvolle Spielbedingungen mit spektakulären Aussichten auf die afrikanische Wildnis. Neben dem Golfen haben Besucher die Möglichkeit, unvergessliche Safaris zu erleben, Weinproben in den besten Weingütern der Region zu genießen oder historische Städte wie Kapstadt zu erkunden.

Ihre Golfreise Südafrika wird zu einer perfekten Mischung aus sportlicher Herausforderung, kulturellen Entdeckungen und luxuriöser Entspannung. Südafrika bietet Golfern ein einzigartiges Erlebnis, das Natur, Abenteuer und Golfgenuss auf höchstem Niveau vereint.

Lassen Sie sich von der Magie dieses Landes verzaubern und erleben Sie eine Golfreise, die Sie nie vergessen werden. Von der spektakulären Tierwelt bis zu erstklassigen Golfplätzen ist Südafrika eine Destination, die jeden Golfliebhaber begeistern wird.

Bei den Sprachtreffen, die ich regelmäßig organisiert hatte, kam immer wieder die Frage auf, wo eins in Heidelberg deutsche Küche bekäme. Um nicht immer neu darüber nachzudenken und eine findbare Liste zu haben, schreibe ich hier eine Liste.

Wer nach einer deutschen Küche sucht, wird meist fündig. Alternativ kannst Du auch nach Restaurants gutbürgerlich suchen, um weitere deutsche Restaurants zu finden.

Wenn Du einen Tipp für weitere Restaurants hast, freue ich mich über einen Hinweis.

Heidelberg

Altstadt

Backmulde Die Kurfürstenstube Essighaus Gasthaus zum weißen Schwanen Restaurant Hackteufel Herrenmühle Kulturbrauerei Löwenbräu Palmbräu Gasse Weinstube Schnitzelbank Schnitzelhaus Alte Münz Sudpfanne Vetters Alt Heidelberg Brauhaus Wirtshaus zum Spreisel Wirtshaus zum Nepomuk Zum Güldenen Schaf Zum Roten Ochsen Zum Seppl

Bahnstadt

Bergheim

uban Kitchen

Handschuhsheim

Alt Hendesse Gilberts Goldener Adler Hendsemer Löb Weißer Stein Züchterklause Handschuhsheim

Kirchheim

Dufke Stettiner Klause

Neuenheim

BräuStadl Kyffhäuser Marktstübel Dorfschänke

Pfaffengrund

Gasthaus zur Kupferlampe

Rohrbach

Roter Ochsen, Rathausstraße 55 Traube Linde

Schlierbach

Restaurant Wolfsbrunnen

Weststadt

Krokodil Schwarzer Peter

Wieblingen

Zum Hirsch

Ziegelhausen

Über den Tellerrand

Bammental

Dossenheim

Edingen-Neckarhausen

Eppelheim

Badisches Gasthaus zum Goldenen Löwen Gasthaus Adler

Ladenburg

Die Kartoffel Gasthaus zum Ochsen Gasthaus zum Schwanen

Leimen/St. Ilgen

Neckargemünd

Alte Scheune

Sandhausen

Schönhau

Schriesheim

Deutscher Hof

Walldorf

Weinheim

Wiesloch

Inspiriert durch einen Post von ElaWild (die wiederrum auch von einer anderen Person dazu inspiriert wurde) möchte auch ich versuchen einen Wochenrückblick in Textform abzufassen und hier zu veröffentlichen.

Ihr könnt euch schon mal Mental auf jede Menge unsinn vorbereiten. Ich bin auch sehr gut darin oft meine Tools zu wechseln (Joplin –> Obsidian –> Logseq –> Obsidian –> Joplin –> Obsidian) oder über Probleme nachzudenken, die ich eigentlich garnicht habe.

Jahreswechsel

Den Jahreswechsel habe ich im engsten Kreis mit meiner Frau und den zwei kleinen Hobbits verbracht. Seit langem habe ich es mal wieder geschafft bis Mitternacht wach zu bleiben. Meine Frau musste mich beim schauen von John Wick 5 nur öfter wecken (Wer den Film auch schon gesehen hat, kann sich denken weshalb...).

Nachdem wir dann zu zweit einen kleinen Piccolo getrunken haben, sind wir auch schon ins Bett gefallen.

Zimmergestaltung

Wie ich in dem einen oder anderen Beitrag im Fediverse bereits geschrieben hatte, haben wir unser Wohnzimmer umgestaltet. Dabei hat meine Frau den gestalterischen Part übernommen und ich den handwerklichen. Optik kann ich halt nicht.

So zogen diverse Zimmerpflanzen, neue Töpfe (Werden die auch so genannt, wenn sie eigentlich aus Bast mit einer Tüte drin sind?) und Gardinen mit Gardinenstangen ein.

In Summer gefällt mir alles sehr gut. Jetzt ist alles schön Boho und hyggelig.

Gerätewechsel

Wie ich in in diesem Beitrag bereits geschrieben hatte, bin ich jetzt im Besitz eines MacBook Pro (2024). Mein MacBook Air (mid 2017) bekommt leider keine Updates mehr und ich setze es gerade auf “Werkseinstellungen” zurück, um es weiterverkaufen zu können.

Ich habe dazu schon Kritik aus dem Fedi bekommen. Und ja, ihr habt recht! Nachhaltiger wäre es gewesen auf das Air ein Linux zu schmeißen und es weiter zu nutzen. Wenn ich mehr Zeit zur Verfügung hätte, hätte ich das auch getan. Bei der wenigen Zeit möchte ich mich aber einfach an ein Gerät setzen und es einfach nutzen. Da möchte ich nicht groß rumfrickeln bis der Drucker funktioniert oder ich die Software für den Tiptoi-Stift in Gang bekommen habe.

Ziele 2025

Natürlich habe ich mir Ziele für 2025 gesetzt. Um diese Ziele zu ermitteln habe ich ein “Lebensrad” oder “Rad des Lebens” erstellt bzw. gefüllt. Die Idee davon habe ich aus dem Buch “Feel Good Productifity” von Ali Abdaal. In diesem Video wird es aber auch erklärt (Kapitel “Wheel of Life” – Minute 3:57)

Aus den drei Bereichen mit den niedrigsten Werten bzw. den Bereichen, bei denen ich gerne einen höheren Wert hätte, haben sich meine Ziele abgeleitet. Welche das sind, bleibt aber mein Geheimnis (noch zumindest)

---

Das war es für KW1. Jetzt, wo ich den ersten Post verfasst habe, finde ich die Idee weiterhin gut. Schauen wir mal, wie lange ich durchhalte.

General Info

Country: The Autonomous Region of Madeira, Portugal | Language: Portuguese | Currency: EURO (EUR) | Flag: https://de.wikipedia.org/wiki/Flagge_Madeiras | When visited: December 2022 & 2024

____________________________________________________________________________

🗺️ Check out my new “Now and Then” travel account on Instagram: https://www.instagram.com/nowandthenjourney

🚗 How to commute

There are 3 ways to move around the island as well as to reach this small town: to hire a car, to get a taxi or to go by public transport, i.e. by bus. The cheapest way is, of course, the public transport, but if you go to Porto Moniz from the airport, you'll have to go to Funchal firstly (use the Aerobus #9, in Dec. 2024 a one way ride was 6,20 EUR) and then change to the bus #80 or #139 (for example, on the station “Avenida Do Mar”). Buses are operated by Rodoeste and depart just a few times per day, so make sure to check the timetable in advance. You can do it here: https://www.portomoniz.pt/de/besuch/verkehr/oeffentliche-verkehrsmittel or directly on the Rodoeste website.

🏨 Where to stay

Last time we have been renting an apartment “Sea and Sun 4 You”. A well-equipped and comfortable flat with a nice terrace and some sea view just in a minute from the ocean and the natural pool “Piscinas Naturais do Porto Moniz” (in the same building as the hotel “Salgueiro”). This time we have been staying in one of the best hotels in this town – “Aqua Natura Bay”: it has great modern rooms, amazing facilities (outdoor and indoor swimming pool, jacuzzi, 2 saunas, gym, rooftop terrace as well as further services), friendly stuff and generous and tasty breakfasts. The same hotel owns 2 more buildings in the town, and one can use all the facilities like, for example, a rooftop terrace with a jacuzzi, there too.

🍽️ What and where to eat

If you have an apartment and can cook there, you can go to one of 3 local supermarkets (the best prices are in the Meu Super though) and have an affordable though still high quality food. Otherwise, you'll have to go to one of the local cafés or restaurants for breakfasts, lunches, and dinners. Prices are almost the same in various places, but quality may vary. Though you can eat a fresh and tasty food including fish of the day almost everywhere. We have been to almost all places and our favourites are listed below: -Cafe Atlantico – a place, where many locals eat, and you can find one of the best Fish of the day or Octopus lagareiro in the town. You need to ask, what they have in the menu today, as it totally depends on the local fishermen.

-Snack-bar Ilhèu Mole – a place, where many locals eat as well, and you can have some quick but tasty snacks such as empanadas or toasts and also enjoy both the Portuguese & Venezuelan cuisine and tasty coffee just for 1,5 EUR for Americano.

-Cachalote an atmospheric place with great interior, incredible view as it's surrounded by the ocean, and good food. There is also an amazing small historical exhibition about the whale fishing industry on the 1st floor, which is freely accessible for everyone.

-Vila Baleia just a good place with a good menu and affordable prices.

-Sea View Restaurante where you can eat tasty dishes with a remarkable view over the ocean and the natural swimming pool. Though, variety of food is not that big here and prices are one of the highest in the town.

👀 What to do and what to see

• Swim in one of 2 natural swimming pools. There are 2 natural pools: — one – Piscinas Naturais do Porto Moniz – is paid and provides the full service and all the needed facilities. — another one – Piscinas Naturais do Aquário – is free and open for anyone to use anytime, though there is just an open-air shower and there is no changing rooms or toilet, though there is a really clean and cool toilet nearby under the Aquário da Madeira.

• Visit Forte de São and Aquário da Madeira.

• Walk around and visit multiple viewpoints nearby, our favourite is Miradouro do Cabo Calhau.

• Go to one of the neighbour cities. You can go for a day tour by bus or taxi to Seixal, Sao Vicente or Achadas da Cruz. There is also small town “Ribeira da Janela”, which you can visit even by foot going through the picturesque route along the ocean.

• Go to one of the day tours. There are multiple great and beautiful places to see around like Fanal Forest, multiple beautiful hiking routes (Levadas) and viewpoint in the mountain, boat trips to watch whales and dolphins and so on.

💡 Some highlights

• You can literally breathe the ocean and enjoy its beauty and power here! Walk around and enjoy views and smells.
• Try fresh seafood and fish – it's just so tasty here!
• Try the local sweets from passion fruit, which also grows here: a soft drink “Brisa Maracuja” and a dessert “Passion Fruit Pudding”.