FLP_partial Cheat Sheet (DRAFT) by andreea2823

Deși lambda calculul constă doar în λ-termeni, putem reprezenta și manipula tipuri de date comune.

•T ≜ λxy.x (dintre cele doua altern­ative o alege pe prima)
•F ≜ λxy.y (dintre cele doua altern­ative o alege pe a doua)
if = λbtf.t , if b = true
        λbtf.f, if b = false
altfel spus, if ≜ λbtf.b t f
and ≜ λb1b2.if b1 b2 (sau λb1b2.b2 b1 b2 sau λb1b2.b1 b2 F)
or ≜ λb1b2.if b1 T b2
not ≜ λb1.if b1 F T F
Operațiile lucrează corect doar dacă primesc ca argumente valori booleene. Folosind lambda calcul fară tipuri, avem garbage in, garbage out.

Numeralul Church pentru numărul n ∈ N este notat n(bar).
Numeralul Church n(bar) este λ-termenul λfx.fⁿx, unde fⁿ reprezintă compunerea lui f cu ea însăși de n ori. Avem deci n ≜ λfx.fⁿx.
Definim Succ ≜ λnfx.f (n f x)
       add ≜ λmnfx.m f (n f x)
       add′ ≜ λmn.m Succ n
       mul ≜ λmn.m (add n) 0(bar)
       exp ≜ λmn.m (mul n) 1(bar)
       isZero ≜ λnxy.n (λz.y) x

Dacă F și M sunt λ-termeni, spunem că M este un punct fix al lui F dacă F M =β M.
Thm: În lambda calculul fără tipuri, orice termen are un punct fix.

= termeni închiși care „const­ruiesc” un punct fix pentru un termen arbitrar.
Exemple:
Combin­atorul de punct fix al lui Curry: Y ≜ λy.(λx.y (x x)) (λx.y (x x)) (YF punct fix al lui F, pt orice teremn F, deoarece YF ↠β F (Y F))
Combin­atorul de punct fix al lui Turing: Θ ≜ (λxy.y (x x y)) (λxy.y (x x y)) (ΘF punct fix al lui F, pt orice termen F, deoareceΘF ↠β F (Θ F))

fact n = if(isZero n) (1) (mul n (fact(pred n)) )
fact = λn.if(­isZero n) (1) (mul n (fact(pred n)) )
fact = (λfn.i­f(i­sZero n) (1) (mul n (f(pred n)) ))fact
Notăm F = λfn.if­(isZero n) (1) (mul n (f(pred n)) )
Ultima ecuat, ie devine fact = F fact, o ecuație de punct fix.
Luăm deci fact ≜ Y F, adică fact ≜ Y (λfn.i­f(i­sZero n) (1) (mul n (f(pred n)) ))

extens­ional: „funcții prin grafice”, clasă mai largă de funcții, cuprinde și funcții care nu pot fi definite prin formule
   (domeniu și codomeniu fixate, funcția e o mulțime de perechi -> duce intrări în ieșiri)
  funcții extens­ional egale = pentru aceeași intrare obțin aceeași ieșire (f(x) = g(x), ∀x∈ X)
intens­ional: „funcții ca formule” (nu e mereu necesar să știm domeniul și codome­niul; paradigmă utilă în inform­ati­că-­>un program = o fcț de la intrări la ieșiri)
 ­  funcții intens­ional egale: definite prin acceași formulă (eventual prelucrată)

lambda calcul = teorie a funcțiilor ca formule
Exemplu: λx.x² = x->x² (e expresie, nu instrucțiune/declarație)
 ­ ­ ­Var­iabila x este locală­/legată în termenul λx.x²
Exemplu: f◦f = λx.f(f(x))
               f→f◦f = λf.λx.f­(f(x))
              ((λf.λx.f(f(x)))(λy.y²))(5) = 625
Funcția identitate f = λx.x are tipul X->X, unde X poate să fie orice mulțime
Funcția g = λf.λx.f­(f(x)) are tipul (X->X)->(X->X)
f(f) ≃ (λx.x)­(λx.x) ≃ λx.x ≃ f
Combin­atorul ω = λx.xx care reprezintă funcția care aplică x lui x
 ­ ­ω(λy.y) ≃ (λx.xx­)(λy.y) ≃ (λy.y)­(λy.y) ≃ (λy.y)
ω =λx.x(x), ω(ω) = ?
ω(f) = f(f), for any f that belongs to its domain. So ω(ω) = ω(ω) and cannot be further evaluated

-- nu specificăm tipul niciunei expresii
-- nu specificăm domeni­ul/­cod­omeniul funcțiilor
-- flexib­ilitate maximă, dar riscant deoarece putem ajunge în situații în care încercăm să aplicăm o funcție unui argument pe care nu îl poate procesa

-- specificăm mereu tipul oricărei expersii
-- nu putem aplica funcții unui argument care are alt tip față de denumirea funcției
-- expresii de forma f(f) sunt eliminate, chiar dacă f e funția identitate

-- o situație interm­ediară între cele două de mai sus
-- putem specifica că o expresie are tipul X->X, dar fără a specifica cine este X

informal: o funcție este calcul­abilă dacă există o metodă „pen-a­nd-­paper” care permite calcularea lui f(n), pentru orice n
Turing - a definit un calculator ideal numit mașina Turing și a postulat că o funcție este calcul­abilă ddacă poate fi calculată de o astfel de mașină
Godel - a definit clasa funcțiilor recursive și a postualt că o funcție este calcul­abilă ddacă este o funcție recursivă
Church - a definit un limbaj de programare ideal numit lambda calcul și a postulat că o funcție este calcul­abilă ddacă poate fi scrisă ca un labda termen
Teza Church­-Turing - cele 3 metode sunt echiva­lente și coincid cu noțiunea intuitivă de calcul­abi­litate

Logica clasică: plecând de la niște presup­uneri, este suficient să ajungi la o contra­dicție
Logica constr­uctivă: pentru a arăta că un obiect există, trebuie să îl construim explicit
- legătura dintre lambda calcul și logica constr­uctivă este dată de paradigma „proof­-as­-pr­ograms” (o demons­trație trebuie să fie o constr­ucție, un program; lambda calculul este o notație pentru un astfel de program)

•Un model de calcul­abi­litate
•Limbajele de programare funcți­onală sunt extensii ale sale
•Un limbaj formal
•Expre­siile din acest limbaj se numesc lambda termeni

Fie V o mulțime infinită de variabile, notate x, y, z,....
Mulțimea lambda termenilor este dată de următoarea formă BNF:
    lambda termen = variabilă | aplicare | abstra­ctizare
   M, N ::= x | (M N) | (λx.M)
Definiție altern­ativă:
Fie V o mulțime infinită de variabile, notate x, y, z, ....
Fie A un alfabet format din elementele din V și simboluri speciale (, ), λ, ..
Fie A mulțimea tuturor cuvintelor finite pentru alfabetul A.
Mulțimea lambda termenilor este cea mai mică submulțime Λ ⊆ A astfel încât:
    [Varia­bila] V ⊆ Λ
    [Aplicare] dacă M, N ∈ Λ atunci (M N) ∈ Λ
    [Abstr­act­izare] dacă x ∈ V și M ∈ Λ atunci (λx.M) ∈ Λ

•Se elimină parant­ezele exteri­oare.
• Aplicarea este asociativa la stânga (M N P = (M N P), f x y z = ((f x) y) z)
• Corpul abstra­cti­zării (partea de după punct) se extinde la dreapta cât se poate (λx.M N = λx.(M N), nu (λx.M) N)
• Mai mulți λ pot fi comprimați (λxyz.M = λx.λy.λz.M)
Exemple:
    (λx.(λ­y.(­λz.((x z)(y z))))) = λxyz.x z (y z)
    (((a b) (c d)) ((e f) (g h))) = a b (c d) (e f (g h))
    x x x x = (((x x) x) x)
    λx.x λy.y = (λx.(x (λy.y)))

λx.N, unde
    λ_._ = operator de legare (binder)
    x (din λx._) = variabilă de legare (binding)
    N = domeniul (scope) de legare a lui x
•toate aparițiile lui x în N sunt legate.
• o apariție care nu este legată se numește liberă
•un termen fără variabile libere se numește închis (combi­nator).
Exemplu: M ≡ (λx.xy) (λy.yz)
    x este legată
    z este liberă,
    y are o apariție legată și una liberă
    mulțimea variab­ilelor libere ale lui M este {y, z}.

Mulțimea variab­ilelor libere dintr-un termen M este notată FV(M) și este definită prin:
    FV(x) = {x}
    FV(M N) = FV(M) ∪ FV(N),
   ­FV(­λx.M) = FV(M)\{x}

Dacă x, y sunt variabile și M este un termen, M<y­/x> este rezultatul obținut după redenu­mirea lui x cu y în M.
    x<y­/x>≡ y, z<y­/x>≡ z, dacă x != z
    (M N)<­y/x> ≡ (M<­y/x­>) (N<­y/x­>),
    (λx.M)­<y/­x> ≡ λy.(M<­y/x­>),
    (λz.M)­<y/­x> ≡ λz.(M<­y/x­>), dacă x != z

α-echi­valența = cea mai mică relație de congruenșă =α pe mulțimea lambda termen­ilor, aî pentru orice termen M și orice variabilă y care nu apare în M, avem λx.M =α λy.(M<­y/x­>)
-- cea mai mică relație pe lambda termeni care satisface regulile:
  &nbsp vezi poza din cardul 2.1
Convenția Barend­regt: variab­ilele legate sunt redenumite pt a fi distincte.

M[N/x] este rezultatul obținut dupa înlocuirea lui x cu N în M.
Cazuri speciale:
1. Înlocuim doar variabile libere: x (λxy.x­)[N/x] = N (λxy.x), nu N (λxy.N) sau N (λNy.N).
2.Nu vrem sa legăm variabile libere neinte­nți­onat:M ≡ λx.y x, N ≡ λz.x z (x legată în M și lilberă în N). Redenumim variab­ilele legate înainte de substi­tuție!
 ­M[N/y] = (λx'.y x')[N/y] = λx'.N x'= λx'.(λz.x z) x'

(λz.x)­[y/x] = λz.y
(λy.x)­[y/x] = λy'.y, nu λy.y,
(λy.x)[(λz.z w)/x] = λyz.zw

Convenție: M=N (2 termeni egali) dacă sunt α-echi­val­enți.
β-reducție = procesul de a evalua lambda termeni prin „pasarea de argumente funcți­ilo­r"
β-redex = un termen de forma (λx.M) N
redusul unui redex (λx.M) N este M[N/x]
Reducem lambda termeni prin găsirea unui subtermen care este redex și apoi înlocuirea acelui redex cu redusul său; repetăm acest proces până nu mai sunt redexuri
forma normală = un lambda termen fără redexuri
Observ­ații:
   ­•re­ducerea unui redex poate crea noi redex-­uri­/șterge alte redex-uri
    • numărul de pași necesari pâna a atinge o fn poate varia, în funcție de ordinea în care sunt reduse redex-­urile, iar rezultatul final nu depinde de alegerea redex-­urilor
    •lungimea unui termen nu trebuie să scadă în procesul de β-redu­cție; poate crește sau rămâne neschi­mbat.

(λx.x x) (λx.x x) nu poate fi redus la o β-formă normală (evaluarea nu se termină)
Există lambda termeni care deși pot fi reduși la o formă norală, pot să nu o atingă niciodată (contează strategia de evaluare).
Notăm cu M -»β M' faptul că M poate fi β-redus până în M' în 0 sau mai mulți pași (închiderea reflexivă și tranzitivă a relației →β)
Notăm cu M =β M′ faptul că M poate fi transf­ormat în M′ în 0 sau mai mulți pași de β-redu­cție, transf­ormare în care pașii de reducție pot fi și întorși.
=β este închiderea reflexivă, simetrică și tranzitivă a relației →β.
M este slab normal­izabil (weakly normal­ising) dacă există N în forma normală aî M -»β N.
M este puternic normal­izabil (strong normal­ising) dacă nu există reduceri infinite care încep din M.
puternic normal­izabil => slab normal­izabil
Exemple:
    (λx.y) ((λz.zz ) (λw.w)) - puternic normalizabil.
   ­(λxy.y) ((λx.x x) (λx.x x)) (λz.z) - slab normal­izabil, dar nu puternic normal­izabil.

Card 3.2

(λx.x) M -»β M
(λxy.x) M N -»β M
(λx.x x) (λy.y y y) -»β (λy.y y y) (λy.y y y) (λy.y y y). . .

Lambda calculul nu specifică o strategie de evaluare, fiind nedete­rminist
Strategia normală = leftmo­st-­out­ermost (alegem redex-ul cel mai din stânga și apoi cel mai din exterior)
  dacă M1 și M2 sunt redex-uri și M1 este un subtermen al lui M2, atunci M1 nu va fi um redex ales.
  printre redex-­urile care nu sunt subtermeni ai altor redex-uri (și sunt incomp­atibili față de relația de subter­men), îl alegem pe cel mai din stânga.
Dacă un termen are o formă normală, atunci strategia normală va converge la ea.
Strategia aplicativă = leftmo­st-­inn­ermost (alegem redex-ul cel mai din stânga și apoi cel mai din interior)
  dacă M1 și M2 sunt redex-uri și M1 este un subtermen al lui M2, atunci M2 nu va fi următorul redex ales
  printre redex-­urile care nu sunt subtermeni ai altor redex-uri (și sunt incomp­atibili față de relația de subter­men), îl alegem pe cel mai din stânga.

Call-b­y-Name (CBN) = strategia normală fără a face reduceri în corpul unei λ-abst­rac­tizări.
Call-b­y-Value (CBV) = strategia aplicativă fără a face reduceri în corpul unei λ-abst­rac­tizări (folosit în general de limbajele de progr funcți­onală, excepție Haskell, e o formă de evaluare leneșă).
O valoare este un λ-term pt care nu există β-reducții date de strategia de evaluare consid­erată.

Fie V = {α, β, γ, ...} o mulțime infinită de tipuri variabilă.
Mulțimea tuturor tipurilor simple T este definită prin:
   T = V | T → T
• (Tipul variabilă) Dacă α ∈ V, atunci α ∈ T.
• (Tipul săgeată) Dacă σ, τ ∈ T, atunci (σ → τ) ∈ T.
Tipurile săgeată reprezintă tipuri pentru funcții cum ar fi Nat->Real (fct de la nr nat la nr reale) sau (Nat ->I­nt)­->(­Int­->Nat) (fcț care au ca intrare o fcț de la nr nat la nr întregi li produce o fcț de la întregi la nat)
Parant­ezele în tipurile săgeată sunt asociative la dreapta.

M are tip σ: M :σ
Variabilă x :σ. Pp că orice var din M are tip unic (Dacă x :σ și x : τ, atunci σ ≡ τ)
Aplicare: Dacă M :σ → τ și N:σ, atunci M N : τ.
Abstra­ctizare Dacă x :σ și M : τ, atunci λx. M :σ → τ.
M are tip (este typeable) daca există un tip σ astfel încât M :σ.

Asocierea explicită (Churc­h-t­yping):
    •constă în prescierea unui unic tip pt fiecare variabilă, la introd­ucerea acesteia (tipuri stabilite explicit)
Asocierea implicită (Curry­-ty­ping):
    • constă în a nu prescrie un tip pt fiecare variabilă, ci în a le lăsa „deschise” (teremenii typeable sunt descop­eriți printr-un proces de căutare).

Mulțimea λ-term­enilor cu pre-tipuri ΛT este: ΛT = x | ΛT ΛT | λx : T. ΛT.
O afirmație este o expresie de forma M :σ, unde M ∈ ΛT și σ ∈ T (M = subiect, σ =tip).
O declarație este o afirmație în care subiectul e variabilă (x :σ*).
Un context este o listă de declarații cu subiecți diferiți.
O judecată este o expresie de forma Γ ⊢ M :σ, unde Γ este context și M :σ este o afirmație.