Helyettesítés

A matematikában és az informatikában a helyettesítés egy adott kifejezés résztagjainak szintaktikai cseréje más kifejezésekkel, bizonyos szabályok szerint. Általában egy kifejezés helyettesítéséről beszélünk változó helyett .

Definíciók és jelölések

Nincs univerzális, konzisztens jelölés a helyettesítésre, és nincs szabványos definíció sem. A helyettesítés fogalma nemcsak a rovatokon belül változik, hanem az egyes kiadványok szintjén is. Általában megkülönböztethetünk kontextus-helyettesítést és „helyett” helyettesítést . Az első esetben azt a helyet a kifejezésben, ahol a helyettesítés megtörténik , a szövegkörnyezet adja meg , vagyis a kifejezés azon része, amely ezt a helyet „környékeli”. A helyettesítés ilyen fogalmát különösen az újraírásnál használják . A második lehetőség gyakoribb. Ebben az esetben a helyettesítést általában valamilyen függvény adja a változók halmazából a kifejezések halmazába. A helyettesítés műveletének jelölésére általában használjon postfix jelölést . Például egy kifejezésen végrehajtott helyettesítési művelet eredményét jelenti . $\sigma :X\to T$ $t\sigma$ $\sigma$ $t$

Az esetek túlnyomó többségében szükséges, hogy a helyettesítésnek véges támasza legyen, azaz véges halmazzal. Ebben az esetben a változó-érték párok egyszerű felsorolásával adható meg . Mivel minden ilyen helyettesítés egy-egy változót helyettesítő helyettesítések sorozatára redukálható az általánosság elvesztése nélkül, feltételezhetjük, hogy a helyettesítést egy változó-érték pár adja , ami általában meg is történik. $\{x\mid x\neq \sigma x\}$

A helyettesítés utolsó definíciója valószínűleg a legjellemzőbb és leggyakrabban használt. Nincs azonban rá egyetlen általánosan elfogadott jelölés sem. A leggyakoribb jelölés az x helyett a t [ a / x ] , t [ x : = a ] vagy t [ x ← a ] jelöléssel .

Változóhelyettesítés λ-számításban

A λ-számításban a helyettesítést a szerkezeti indukció határozza meg. Tetszőleges objektumok és tetszőleges változó esetén a tetszőleges szabad előfordulás lecserélésének eredménye helyettesítésnek minősül , és a konstrukciós indukció határozza meg : $P$ $K$ $x$ $x$ $K$ $K$

(i) alap: : az objektum megegyezik a változóval . Aztán ;

Q\equiv x

K

x

[P/x]x\equiv P

(ii) alap: : az objektum megegyezik a konstanssal . Aztán tetszőleges atomra ;

Q\equiv c

K

c

[P/x]c\equiv c

c\not \equiv x

(iii) lépés: : az objektum nem atomi, és alkalmazás formájú . Aztán ;

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

K

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

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

(iv) lépés: : az objektum nem atomi, és a -absztrakciója . Akkor [ ;

Q\equiv \lambda xM

K

x

\lambda xM

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

(v) lépés: : az objektum nem atomi, és a -absztrakciója , -val . Akkor:

Q\equiv \lambda yM

K

y

\lambda yM

y\not \equiv x

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

és vagy ; _

y\not \equiv x

y\notin P

x\notin M

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

és és . _

y\not \equiv x

y\in P

x \-ben M

Lásd még

Linkek

Logikák

Filozófia • Szemantika • Szintaxis • Történelem

Logikai csoportok

klasszikus logika	Arisztotelészi logika propozíciós logika Elsőrendű logika Másodrendű logika magasabb rendű logika
matematikai logika	halmazelmélet Modellelmélet Kiszámíthatóság elmélet Bizonyításelmélet és konstruktív matematika Lineáris logika formális rendszer természetes következtetés Sorozatszámítás Logikai algebra Releváns logika Deontikus logika intuicionista logika Lambek kalkulus
Nem klasszikus logika	intuicionizmus zavaros logika Szubstrukturális logika logika Leírás logika Többértékű logika Logikai szintézis Kötési logika Időbeli logika Modális logika ( Hibrid logika ) episztemikus logika
Filozófiai logika	Kritikus gondolkodás informális logika deduktív érvelés

Alkatrészek

Logikai szimbólumok listája