Substituce

V matematice a informatice , substituce je operace syntaktického nahrazení subterms daného termínu jinými termíny, podle určitých pravidel. Obvykle mluvíme o nahrazení termínu místo proměnné .

Definice a zápis

Neexistuje žádný univerzální, konzistentní zápis pro substituci, ani neexistuje standardní definice. Pojem substituce se liší nejen v rámci sekcí, ale i na úrovni jednotlivých publikací. Obecně můžeme rozlišit substituci kontextu a substituci „místo“ . V prvním případě je místo v termínu, kde k záměně dochází, dáno kontextem , tedy částí termínu, která toto místo „obklopuje“. Zejména se takový pojem substituce používá při přepisování . Druhá možnost je běžnější. V tomto případě je substituce obvykle dána nějakou funkcí z množiny proměnných do množiny termů. K označení akce substituce zpravidla používejte postfixovou notaci . Například znamená výsledek substituční akce na termínu . $\sigma :X\to T$ $t\sigma$ $\sigma$ $t$

V drtivé většině případů se požaduje, aby substituce měla konečnou podporu, tedy aby množina byla konečná. V tomto případě ji lze specifikovat jednoduchým výčtem párů proměnná-hodnota . Protože každá taková substituce může být redukována na sekvenci substitucí nahrazujících každou pouze jednu proměnnou, aniž by došlo ke ztrátě obecnosti, můžeme předpokládat, že substituce je dána jedním párem proměnná-hodnota , což se obvykle provádí. $\{x\mid x\neq \sigma x\}$

Poslední definice substituce je pravděpodobně nejtypičtější a nejčastěji používaná. Ani pro to však neexistuje jediný obecně uznávaný zápis. Nejběžnější zápis pro dosazení a za x v t je t [ a / x ], t [ x := a ] nebo t [ x ← a ].

Substituce proměnných v λ-kalkulu

V λ-kalkulu je substituce definována strukturální indukcí. Pro libovolné objekty a libovolnou proměnnou se výsledek nahrazení libovolného volného výskytu v považuje za substituci a je určen indukcí konstrukce : $P$ $Q$ $X$ $X$ $Q$ $Q$

(i) základ: : objekt je stejný jako proměnná . Potom ;

Q\equiv x

Q

X

[P/x]x\equiv P

(ii) základ: : objekt je stejný jako konstanta . Pak pro libovolný atomový ;

Q\equiv c

Q

C

[P/x]c\equiv c

c\not \equiv x

(iii) krok: : objekt je neatomový a má formu aplikace . Potom ;

Q\equiv (Q_{1}\,Q_{2})

Q

(Q_{1}\,Q_{2})

[P/x](Q_{1}\,Q_{2})\equiv ([P/x]Q_{1})([P/x]Q_{2})

(iv) krok: : objekt je neatomární a je abstrakce . Poté [ ;

Q\equiv \lambda xM

Q

X

\lambda xM

P/x](\lambda xM)\ekviv \lambda xM

(v) krok: : objekt je neatomární a je -abstrakce , s . Pak:

Q\equiv \lambda yM

Q

y

\lambda yM

y\not \equiv x

[P/x](\lambda yM)\equiv (\lambda y.[P/x]M)

pro a nebo ;

y\not \equiv x

y\notin P

x\notin M

(\lambda z.[P/x][z/y]M)

pro a a .

y\not \equiv x

y\in P

x \v M

Viz také

Odkazy

Logika

Filosofie • Sémantika • Syntaxe • Historie

Logické skupiny

klasická logika	Aristotelská logika výroková logika Logika prvního řádu Logika druhého řádu logika vyššího řádu
matematická logika	teorie množin Teorie modelu Teorie vyčíslitelnosti Důkazová teorie a konstruktivní matematika Lineární logika formální systém přirozený závěr Sekvenční počet Algebra logiky Relevantní logika Deontická logika intuicionistická logika Lambekův počet
Neklasická logika	intuicionismus fuzzy logika Substrukturální logika logika Popisná logika Vícehodnotová logika Logická syntéza Závazná logika Časová logika Modální logika ( Hybrid logic ) epistemická logika
Filosofická logika	Kritické myšlení neformální logika deduktivní uvažování

Komponenty

Seznam booleovských symbolů