Text jag skriver

Tankar och saker som jag skriver om med text

0022_lambdakalkyl_notation.md

Fann alltid det skumt att notationen för abstraktion i lambdakalkylen såg ut såhär:

λx. f(x)

...men jag insåg nu att denna notation följer mönstret med andra variabelintroducerande "operatorer" som t.ex.

∀x. f(x)

∃x. f(x)

Så ser kvantifikationer ut i logik, och det är alla variabelintroducerande operatorer jag hittills har stött på (λ, och ).

Jag har dock blivit van vid att använda notationen

x ↦ f(x)

för funktioner (och variabelintroducerande uttryck). Finner det så praktiskt så att jag försöker se allt som funktioner och genom att använda funktionsnotationen till allt:

Uttryck Kort form Lång form Typ
Derivata 𝐷f(p) 𝐷(x ↦ f(x))(p) 𝐷: (ℝ→ℝ) → (ℝ→ℝ)
Integral ∫(a..b)f ∫(a..b)(x ↦ f(x)) ∫: ℝ² → ((ℝ→ℝ) → ℝ)
Summa ∑(a..b)f ∑(a..b)(x ↦ f(x)) ∑: ℕ² → ((ℕ→ℝ) → ℝ)
Produkt ∏(a..b)f ∏(a..b)(x ↦ f(x)) ∏: ℕ² → ((ℕ→ℝ) → ℝ)
Gränsvärde lim f(L) lim(x ↦ f(x))(L) lim: (ℝ→ℝ) → (ℝ→ℝ)

Med funktioner som har funktioner i sin domän (alltså (A→B) → (C→D)) och vänsterassociativ funktionsapplicering (alltså f g x=f(g(x)))) funkar det finfint. Man kan se allt som funktioner!

Det kan vara praktiskt att se det på detta viset i många sammanhang, men problemet är bara den att ingen skriver på detta vis, och därför skulle ingen förstå vad jag menade.

Nåväl, så länge det är mina egna anteckningar så är det ju lugnt!

Grejen är då att man kanske till och med hade kunnat dra det längre:

Uttryck Kort form Lång form Typ
Allkvantifikation ∀f ∀(x ↦ f(x)) ∀(X): (X→P) → P
Existentialkvantifikation ∃f ∃(x ↦ f(x)) ∃(X): (X→P) → P

P är typen för påståenden (t.ex. är 1≠2 ett påstående).

Men att även se kvantifikatorerna som funktioner är väl lite.. Det känns lite skumt. Men det kanske bara är en vanesak?