# Vero-Funkcia Logiko por Hakistoj - Parto Unu

Published: February 26, 2025

 
Bob kaj Alice estas du hakistoj laborantaj sur enŝovita sistemo kun severa komputila limigo - estas miso en ilia malkostaj mikrokontrolilo igante OR-operaciojn signife pli malrapidaj ol ajnan alian operacion sur la ĉiparo.

Kiam ili profiladis sian micropython-kodon, ili trovis ke OR-operacioj estis ĝis 5-oble pli malrapidaj ol ajna alia operacio.

{{< dialog character1="Alice" character2="Bob" avatar1="https://images.lagomor.ph/alice.png" avatar2="https://images.lagomor.ph/bob.png" >}}
Alice: Ĉi tio estas granda problemo! Ni povus anstataŭigi la defektajn ĉipojn per pli bonaj, se ili alvenos antaŭ la templimo.

Bob: Mi ne pensas ke ni povas permesi atendi - la templimo estas en 3 tagoj. Pli bona elekto estas reskribita la kodon por eviti la OR-operacion.

Alice: Kiel ni povus fari tion? Ni uzas la OR-operacion en multaj kritikaj lokoj. Rigardu:
{{< /dialog >}}

```python
def authorize_access(request):
    # Uzanto estas rifuzita se ili estas sur nigrlistio AŬ 
    # ilia konto estas eksvalidiĝinta
    if (user_is_blacklisted(request.user_id) or 
        account_is_expired(request.account)
        return "Access denied"
    return "Access granted"
```

Ni prenu momenton por kompreni la problemon. La `authorize_access` funkcio estas uzata por kontroli ĉu uzanto estas rajtigita aliri risurcον. La `or` operacio estas uzata por kombini la kondiĉojn. Kiel ni povus reskribita ĉi tiun funkcion por eviti la OR-operacion?

Por komenci, ni rigardu la OR-operacion mem. OR estas iu ajn kazo kie aŭ A aŭ B estas vera (eble evidente).
La nura fojo kiam OR estas FALSA estas kiam ambaŭ enigoj estas mem falsaj.

Ni povas esprimi ĉi tion en io nomata ver-tabelo.

Ver-tabelo estas logika tabelo uzata por determini la ver-valorojn de logikaj esprimoj bazitaj sur iliaj enigoj. Ĝi sisteme listigas ĉiujn eblajn kombinaĵojn de enig-valoroj kaj la respondan eligon por ĉiu kombinaĵo, permesante al ni vidigi kiel logikaj operacioj funkcias.

Plenigu ĉi tiun por montri kiuj kazoj OR estus veraj:

(Vi povas klaki sur la tabelo por ŝalti la nekonatajn valorojn)
{{< truth-table 
    id="unique-id"
    columns="P,or,Q"
    rows="t,t,t|t,t,f|f,t,t|f,f,f" 
    editable="1" 
>}}

Ni prenu la tempon ankaŭ por diskuti iujn aliajn bazajn operatorojn kiujn Bob kaj Alice havas disponeblaj al ili - AND kaj NOT.

AND postulas AMBAŬ enigojn esti veraj por ke ĝi redonu veron.

{{< truth-table 
    id="unique-id"
    columns="P,and,Q"
    rows="t,t,t|t,f,f|f,f,t|f,f,f" 
    editable="1" 
>}}

NOT simple "renversas" la ver-valoron de la enigo asignita al ĝi.

{{< truth-table 
    id="unique-id"
    columns="P,not P"
    rows="t,f|f,t" 
    editable="1" 
>}}

{{< dialog character1="Alice" character2="Bob" avatar1="https://images.lagomor.ph/alice.png" avatar2="https://images.lagomor.ph/bob.png" >}}
Alice: Kompreneble. Ĉi tiuj estas la plej bazaj operatoroj en programado.

Bob: Vi pravas, ili estas bazaj. Sed kio estas interesa estas kiel ni povas kombini ilin por krei ekvivalentajn esprimojn. Ekzemple, ni povas reskribita OR uzante AND kaj NOT.

Alice: Kiel tio funkcius precize?
{{< /dialog >}}

Bob estas studento de ver-funkcia logiko, kio signifas ke li komprenas ke multaj logikaj deklardiroj estas ekvivalentaj. Estas multaj, multaj manieroj reskribita la `authorize_access` funkcion sen devi uzi la OR-operacion entute.

En ver-funkcia logiko (TFL), logikaj operatoroj kiel AND, OR, kaj NOT povas esti espritaj laŭ unu la alia uzante logikajn ekvivalentecojn. Ĉi tiuj ekvivalentecoj estas deklaroj kiuj havas la saman ver-valoron en ĉiuj eblaj interpretoj.

Ekzemple, unu el la plej utilaj ekvivalentecoj estas la Leĝo de De Morgan, kiu diras:

 - ¬(p ∨ q) ≡ (¬p ∧ ¬q)
 - ¬(p ∧ q) ≡ (¬p ∨ ¬q)

{{< dialog character1="Alice" character2="Bob" avatar1="https://images.lagomor.ph/alice.png" avatar2="https://images.lagomor.ph/bob.png" >}}
Alice: Kio estas tiuj simboloj? Ili aspektas similaj al la operatoroj kiujn mi konas kiel & kaj ! en programado.

Bob: Bona observo! En ver-funkcia logiko, ni uzas specialajn simbolojn por reprezenti logikajn operaciojn. La '¬' simbolo repreznetas negacion aŭ NOT, simile al la '!' en programado. La '∧' estas por AND, kiel '&' en kodo, kaj '∨' estas por OR, simile al la '|' operatoro. La '≡' signifas "estas ekvivalenta al."

Alice: Mi vidas. Sed kial uzi malsamajn simbolojn anstataŭ nur uzi la programadajn?

Bob: TFL uzas ĉi tiujn simbolojn ĉar ili estas pli precizaj kaj universalaj trans malsamaj kampoj de logiko kaj matematiko. Ili helpas logikistojn esprimi kompleksajn ideojn klare sen esti ligitaj al ajna specifa programad-lingva sintakso. Aldone, ili faciligas vidi la strukturon de logikaj formuloj unurigarde.

Alice: Tio havas sencon. Do kiel ni uzus ĉi tiujn por reskribita OR-operacion?
{{< /dialog >}}

La Leĝo de De Morgan, artikulita en ordinara Esperanto, asertas ke ne estas la kazo ke aŭ P aŭ Q estas ekvivalenta al la aserto ke ambaŭ P kaj Q ne estas veraj.

Ni esploru tion per ver-tabelo! Ĉi tio estos iom pli komplikita ol la antaŭaj, ĉar ni administras pli da operatoroj samtempe.

Por solvi ĉi tiun tabelon, ni laboros tra ĉiu kolumno paŝe:

1. Komencu kun la bazaj ver-valoroj por P kaj Q (kolumnoj 1 kaj 2)
2. Kalkulu ¬P per renversado de la ver-valoro de P (kolumno 3)
3. Kalkulu ¬Q per renversado de la ver-valoro de Q (kolumno 4)
4. Trovu P∨Q (OR) (kolumno 5)
    - Memoru, (OR) estas vera se aŭ P aŭ Q estas Vera.
5. Kalkulu ¬(P∨Q) per renversado de la valoroj en kolumno 5 (kolumno 6)
    - Ĉar ni trovas NOT P aŭ Q
6. Kalkulu ¬P∧¬Q (AND) - vera nur kiam ambaŭ ¬P kaj ¬Q estas veraj (kolumno 7)
    - Memoru, (AND) estas vera nur se P aŭ Q estas AMBAŬ veraj.

{{< truth-table 
    id="demorgan-or"
    columns="P,Q,¬P,¬Q,P∨Q,¬(P∨Q),¬P∧¬Q"
    rows="t,t,f,f,t,f,f|t,f,f,t,t,f,f|f,t,t,f,t,f,f|f,f,t,t,f,t,t" 
    editable="2,3,4,5,6" 
>}}

Rimarku kiel kolumnoj 6 kaj 7 havas identajn valorojn? Ĉi tio signifas ke ili estas ekvivalentaj, montrante la Leĝon de De Morgan: ¬(P∨Q) ≡ ¬P∧¬Q

{{< dialog character1="Alice" character2="Bob" avatar1="https://images.lagomor.ph/alice.png" avatar2="https://images.lagomor.ph/bob.png" >}}
Alice: Tio estas lerta! Do en nia kodo, ni povus diri: "ne estas la kazo ke ambaŭ kazoj estas falsaj" anstataŭ "aŭ kazo estas vera."

Bob: Precize! Fakte, ni ankaŭ povus esprimi ĉion uzante nur NAND-operatorojn. La NAND-operacio estas tre potenca ĉar ĝi povas esti uzata por krei ajnan logikan esprimon. Ekzemple, ni povas reskribita niajn antaŭajn esprimojn uzante nur NAND.

Alice: Vere? Kiel tio funkcius?

Bob: Nu, ni povas esprimi AND, OR, kaj NOT uzante NAND. Ekzemple, NOT A povas esti reprezentita kiel A NAND A, kaj A AND B povas esti esprimita kiel (A NAND B) NAND (A NAND B). Ĉi tio signifas ke ni povas konstrui ajnan logikan operacion, inkluzive nian originan funkcion, uzante nur NAND-operaciojn. Kun iom da kreemeco, ni povas derivi ĉiujn necesajn esprimojn sen iam devi uzi OR rekte.
{{< /dialog >}}

Uzante ĉi tiujn ekvivalentecojn, Bob kaj Alice reskribis sian funkcion:

```python
def authorize_access(request):
    # Logike ekvivalenta sed uzante nur NOT kaj AND operaciojn
    if not (not user_is_blacklisted(request.user_id) and 
            not account_is_expired(request.account):
        return "Access denied"
    return "Access granted"
```
La reskribjita funkcio estas logike identa, kaj ni pruvis ĝin! Aldone ĝi rulaĵos signife pli rapide sur ilia aparataroj. Bob kaj Alice savis la tagon, kun via helpo.

# Preter Aparataraj Limigoj: Aliaj Praktikaj Aplikoj

SQL-demandoj ofte implikas tre kompleksajn logikajn kondiĉojn. Kompreni ekvivalentecon povas kelkfoje fari demandojn pli optimumigitajn en kazoj kie certaj logikaj strukturoj prenas pli longajn demand-tempojn ol aliaj. Ekzemple:

```sql
SELECT * FROM transactions
WHERE NOT (customer_id = 101 AND transaction_date > '2023-01-01')
```

estas ekvivalenta al:

```sql
SELECT * FROM transactions
WHERE customer_id != 101 OR transaction_date <= '2023-01-01'
```
## Kriptografio 

Kriptografio ankaŭ estas kazo kie fortaj fundamentoj en logiko povas fari aŭ rompi realigon. En homomorfisma ĉifrado (kiu permesas komputadon sur ĉifrita datumaro), certaj operacioj estas pli efikaj ol aliaj pro la subkuŝantaj kriptografiaj strukturoj.

[TFHE (Rapida Plene Homomorfisma Ĉifrado super la Toro)](https://tfhe.github.io/tfhe/) estas vaste uzata homomorfisma ĉifrad-biblioteko kie NAND-pordegoj estas signife pli rapidaj ol aliaj operacioj. En Microsoft-a SEAL-bibliotekan realigon de FHE, NAND-operacioj povas esti pli efikaj ol rektaj OR-operacioj.

Konsideru privatec-konservan voĉdon-rajtigo-sistemon kie voĉdant-datumoj estas ĉifritaj:

**Originala Logiko:**
```python
def is_eligible_voter(encrypted_data):
    # Voĉdanto estas rajtigita se ili estas civitano AŬ 
    # (ili estas konstanta loĝanto KAJ vivis ĉi tie 5+ jarojn)
    eligibility = homomorphic_or(
        encrypted_data.is_citizen(),
        homomorphic_and(
            encrypted_data.is_permanent_resident(),
            encrypted_data.lived_here_5_plus_years()
        )
    )
    return eligibility
```

Ĉi tio enhavas ambaŭ AND kaj OR operaciojn. Uzante la leĝojn de De Morgan kaj la NAND-universalecon, ni povas reskribita ĝin por uzi nur NAND-operaciojn, kiujn TFHE prilaboras pli efike:

**Optimumigita por TFHE:**
```python
def is_eligible_voter(encrypted_data):
    # Paŝo 1: Konverti la OR uzante De Morgan: A OR B = NOT(NOT A AND NOT B)
    # Paŝo 2: Esprimi NOT laŭ NAND: NOT X = NAND(X, X)
    # Paŝo 3: Esprimi AND laŭ NAND: A AND B = NOT(NAND(A, B)) = NAND(NAND(A, B), NAND(A, B))
    
    citizen = encrypted_data.is_citizen()
    resident = encrypted_data.is_permanent_resident()
    years = encrypted_data.lived_here_5_plus_years()
    
    # NOT citizen uzante NAND
    not_citizen = homomorphic_nand(citizen, citizen)
    
    # resident AND years uzante NAND
    resident_and_years = homomorphic_nand(
        homomorphic_nand(resident, years),
        homomorphic_nand(resident, years)
    )
    
    # NOT (resident AND years) uzante NAND
    not_resident_and_years = homomorphic_nand(resident_and_years, resident_and_years)
    
    # NOT citizen AND NOT (resident AND years) uzante NAND
    not_both = homomorphic_nand(
        homomorphic_nand(not_citizen, not_resident_and_years),
        homomorphic_nand(not_citizen, not_resident_and_years)
    )
    
    # Fina NOT por akiri: citizen OR (resident AND years)
    eligibility = homomorphic_nand(not_both, not_both)
    
    return eligibility
```

En produktad-TFHE-realigoj, ĉi tiu transformo reduktis komputad-tempon de minutoj al sekundoj por kompleksaj rajtigo-kontroloj sur ĉifritaj voĉdant-datumoj, igante privatec-konservajn elekto-sistemojn praktikaj por realmond-uzo.

Vi povas lerni pli pri TFHE [ĉi tie](https://openmined.org/blog/introduction-to-thfe-and-its-applications/).

# Lerni Pli

La kapablo transformi logikajn esprimojn dum konservado de ilia signifo estas fundamenta lerteco kiu rajtigas programistojn superi limigojn en praktike ajna komputad-kunteksto. Ĝi ankaŭ estas nur iomete interesa.

La ekzemploj en ĉi tiu esplorado nur tuŝas la surfacon de kio estas ebla kiam vi profunde komprenas la principojn de ver-funkcia logiko.

Por tiuj interesitaj pri konstruado de pli forta fundamento en logiko, la [Malferma Logiko Projekto](https://openlogicproject.org/) provizas elstarajn senpagajn edukajn resursojn pri propozicia kaj predikato logiko, formalaj prud-sistemoj, kaj aliaj temoj kiel modala logiko kaj ar-teorio - ĉiuj celitaj al ne-matematika publiko.

{{< bookshelf >}}
    {{< book cover="https://forallx.openlogicproject.org/forallxyyc.png" alt="for all x" link="https://forallx.openlogicproject.org/" >}}
    {{< book cover="https://slc.openlogicproject.org/slc.png" alt="Sets, Logic, and Computation" link="https://slc.openlogicproject.org/" >}}
{{< /bookshelf >}}