From f712321988dddc7972f36726866776f21dee1390 Mon Sep 17 00:00:00 2001 From: Boris Verkhovskiy Date: Sat, 6 Apr 2024 04:03:33 -0700 Subject: Remove Latino sine flexione --- lsf/lambda-calculus-lsf.html.markdown | 91 ----------------------------------- 1 file changed, 91 deletions(-) delete mode 100644 lsf/lambda-calculus-lsf.html.markdown (limited to 'lsf/lambda-calculus-lsf.html.markdown') diff --git a/lsf/lambda-calculus-lsf.html.markdown b/lsf/lambda-calculus-lsf.html.markdown deleted file mode 100644 index 88bb638f..00000000 --- a/lsf/lambda-calculus-lsf.html.markdown +++ /dev/null @@ -1,91 +0,0 @@ ---- -category: Algorithms & Data Structures -name: Lambda Calculus -contributors: - - ["Max Sun", "http://github.com/maxsun"] -translators: - - ["Victore Leve", "https://github.com/AcProIL"] -lang: lsf ---- - -# Calculo λ - -Calculo lambda, creato principto per Alonzo Church, es lingua de programmatura -computatro maximo parvo. Quamquam non habe numero, serie de charactere vel ullo -typo de data non functionale, id pote repraesenta omne machina de Turing. - -Tres elemento compone calculo lambda: **quantitate variabile** (q.v.), -**functione** et **applicatione**. - -| Elemento | Syntaxe | Exemplo | -|----------------------|-----------------------------------|-----------| -| Quantitate variabile | `` | `x` | -| Functione | `λ.` | `λx.x` | -| Applicatione | `` | `(λx.x)a` | - -Functione fundamentale es identitate: `λx.x` cum argumento primo `x` et cum -corpore secundo `x`. In mathematica, nos scribe `id: x↦x`. - -## Quantitate variabile libero et ligato - -* In functione praecedente, `x` es q.v. ligato nam id es et in copore et - argumento. -* In `λx.y`, `y` es q.v. libero nam non es declarato ante. - -## Valutatione - -Valutatione es facto per reductione beta (reductione β) que es essentialiter -substitutione lexicale. - -Dum valutatione de formula `(λx.x)a`, nos substitue omne evento de `x` in -corpore de functione pro `a`. - -* `(λx.x)a` vale `a` -* `(λx.y)a` vale `y` - -Pote etiam crea functione de ordine supero: `(λx.(λy.x))a` vale `λy.a`. - -Etsi calculo lambda solo tracta functione de uno parametro, nos pote crea -functione cum plure argumento utente methodo de Curry: `λx.(λy.(λz.xyz))` -es scriptura informatica de formula mathematico `f: x, y, z ↦ x(y(z)))`. - -Ergo, interdum, nos ute `λxy.` pro `λx.λy.`. - -## Arithmetica - -### Logica de Boole - -Es nec numero nec booleano in calculo lambda. - -* «vero» es `v = λx.λy.x` -* «falso» es `f = λx.λy.y` - -Primo, nos pote defini functione «si t tunc a alio b» per `si = λtab.tab`. -Si `t` es vero, valutatione da `(λxy.x) a b` id es `a`. Similiter si `t` es -falso, nos obtine `b`. - -Secundo, nos pote defini operatore de logica: - -* «a et b» es `et = λa.λb.si a b f` -* «a vel b» es `vel = λa.λb.si a t b` -* «non a» es `non = λa.si a f t` - -### Numeros - -Nos pone: - -* `0 = λf.λx.x` (`0: f↦id`) -* `1 = λf.λx.f x` (`1: f↦f`) -* `2 = λf.λx.f(f x)` (`2: f↦f⚬f`) - -Cum mente generale, successore de numero `n` es `S n = λf.λx.f((n f) x)` -(`n+1: f↦f⚬fⁿ`). Id es **`n` est functione que da `fⁿ` ex functione `f`**. - -Postremo additione es `λab.(a S)b` - -## Ut progrede - -### In lingua anglo - -1. [A Tutorial Introduction to the Lambda Calculus](http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf) per Raúl Roja -2. [The Lambda Calculus](http://www.cs.cornell.edu/courses/cs3110/2008fa/recitations/rec26.html), CS 312 Recitation 26 -- cgit v1.2.3