Fria variabler och bundna variabler - Free variables and bound variables

I matematik och i andra discipliner som involverar formella språk , inklusive matematisk logik och datavetenskap , är en fri variabel en notation (symbol) som anger platser i ett uttryck där substitution kan äga rum och inte är en parameter för detta eller något containeruttryck. Vissa äldre böcker använder termerna verklig variabel och uppenbar variabel för fri variabel respektive bunden variabel. Idén är relaterad till en platshållare (en symbol som senare kommer att ersättas av något värde), eller ett jokertecken som står för en ospecificerad symbol.

I datorprogrammering avser termen fri variabel variabler som används i en funktion som varken är lokala variabler eller parametrar för den funktionen. Termen icke-lokal variabel är ofta en synonym i detta sammanhang.

En bunden variabel är en variabel som tidigare var ledig , men har varit bunden till ett specifikt värde eller en uppsättning värden som kallas diskursdomän eller universum . Till exempel blir variabeln x en bunden variabel när vi skriver:

För alla x , ( x + 1) ² = x ² + 2 x + 1 .

eller

Det finns x så att x ² = 2 .

I någon av dessa propositioner spelar det ingen roll logiskt om x eller någon annan bokstav används. Det kan dock vara förvirrande att använda samma bokstav igen någon annanstans i något sammansatt förslag . Det vill säga att fria variabler blir bundna och sedan i viss mening går tillbaka från att vara tillgängliga som stand-in-värden för andra värden i skapandet av formler.

Begreppet "dummyvariabel" används också ibland för en bunden variabel (oftare i allmän matematik än i datavetenskap), men den användningen kan skapa en oklarhet med definitionen av dummyvariabler i regressionsanalys .

Exempel

Innan du anger en exakt definition av fri variabel och bunden variabel är följande några exempel som kanske gör dessa två begrepp tydligare än definitionen skulle:

I uttrycket

${\ displaystyle \ sum _ {k = 1}^{10} f (k, n),}$

n är en fri variabel och k är en bunden variabel; följaktligen beror värdet på detta uttryck på värdet av n , men det finns inget som kallas k som det kan bero på.

I uttrycket

${\ displaystyle \ int _ {0}^{\ infty} x^{y-1} e^{-x} \, dx,}$

y är en ledig variabel och x är en bunden variabel; följaktligen beror värdet på detta uttryck på värdet av y , men det finns inget som heter x som det kan bero på.

I uttrycket

${\ displaystyle \ lim _ {h \ rightarrow 0} {\ frac {f (x+h) -f (x)} {h}},}$

x är en ledig variabel och h är en bunden variabel; följaktligen beror värdet på detta uttryck på värdet av x , men det finns inget som heter h som det kan bero på.

I uttrycket

${\ displaystyle \ forall x \ \ existerar y \ {\ Big [} \ varphi (x, y, z) {\ Big]},}$

z är en ledig variabel och x och y är bundna variabler, associerade med logiska kvantifierare ; följaktligen beror det logiska värdet på detta uttryck på värdet av z , men det finns inget som heter x eller y som det kan bero på.

Mer allmänt, i de flesta av bevisen, använder vi bundna variabler. Till exempel visar följande bevis att varje kvadrat med jämnt heltal är delbart med${\ displaystyle 4}$

Låt vara ett positivt jämnt heltal. Sedan finns det ett heltal så att . Sedan har vi delbart med${\ displaystyle n}$${\ displaystyle k}$${\ displaystyle n = 2k}$${\ displaystyle n^{2} = 4k^{2}}$${\ displaystyle n^{2}}$${\ displaystyle 4}$

inte bara k utan också n har använts som bundna variabler som helhet i beviset.

Variabelbindande operatörer

Det följande

${\ displaystyle \ sum _ {x \ i S} \ quad \ quad \ prod _ {x \ i S} \ quad \ quad \ int _ {0}^{\ infty} \ cdots \, dx \ quad \ quad \ lim _ {x \ till 0} \ quad \ quad \ forall x \ quad \ quad \ existerar x}$

är några vanliga variabelbindande operatörer . Var och en av dem binder variabeln x för vissa set S .

Observera att många av dessa är operatörer som agerar på funktioner i den bundna variabeln. I mer komplicerade sammanhang kan sådana beteckningar bli besvärliga och förvirrande. Det kan vara användbart att byta till notationer som gör bindningen tydlig, t.ex.

${\ displaystyle \ sum _ {1, \ ldots, 10} \ left (k \ mapsto f (k, n) \ right)}$

för summor eller

${\ displaystyle D \ vänster (x \ mapsto x^{2}+2x+1 \ höger)}$

för differentiering.

Formell förklaring

Träd som sammanfattar syntaxen för uttrycket ${\ displaystyle \ forall x \, ((\ existerar y \, A (x)) \ vee B (z))}$

Variabelbindande mekanismer förekommer i olika sammanhang inom matematik, logik och datavetenskap. I alla fall är de dock rent syntaktiska egenskaper hos uttryck och variabler i dem. För detta avsnitt kan vi sammanfatta syntax genom att identifiera ett uttryck med ett träd vars bladnoder är variabler, konstanter, funktionskonstanter eller predikatkonstanter och vars icke-bladnoder är logiska operatorer. Detta uttryck kan sedan bestämmas genom att göra en inorder traversal av trädet. Variabelbindande operatörer är logiska operatorer som förekommer på nästan alla formella språk. En bindande operator Q tar två argument: en variabel v och ett uttryck P , och när det appliceras på dess argument producerar det ett nytt uttryck Q ( v , P ). Betydelsen av bindande operatörer tillhandahålls av språkets semantik och berör oss inte här.

Variabelbindning avser tre saker: en variabel v , en plats a för den variabeln i ett uttryck och en icke-bladnod n av formen Q ( v , P ). Obs! Vi definierar en plats i ett uttryck som en bladnod i syntaxträdet. Variabel bindning sker när den platsen ligger under noden n .

I lambdakalkyl , xär en bunden variabel i uttrycket M = λx. Toch en fri variabel i uttrycket T. Vi säger xär bunden Moch fri in T. Om Tinnehåller en subterm λx. Udå xär rebound i denna term. Denna kapslade, inre bindning av xsägs "skugga" den yttre bindningen. Förekomster av xin Uär fria förekomster av det nya x.

Variabler bundna på programmets översta nivå är tekniskt fria variabler inom de termer som de är bundna till men behandlas ofta speciellt eftersom de kan sammanställas som fasta adresser. På samma sätt är en identifierare bunden till en rekursiv funktion också tekniskt sett en ledig variabel i sin egen kropp men behandlas speciellt.

En sluten term är en som inte innehåller några fria variabler.

Funktionsuttryck

För att ge ett exempel från matematik, överväga ett uttryck som definierar en funktion

${\ displaystyle f = \ left [(x_ {1}, \ ldots, x_ {n}) \ mapsto t \ right]}$

där t är ett uttryck. t kan innehålla några, alla eller inga av x ₁ ,…, x _n och den kan innehålla andra variabler. I det här fallet säger vi att funktionsdefinitionen binder variablerna x ₁ , ..., x _n .

På detta sätt kan funktionsdefinitionsuttryck av det slag som visas ovan betraktas som den variabla bindningsoperatorn, analog med lambda -uttryck för lambda -kalkyl . Andra bindande operatörer, som summeringsskylten , kan ses som funktioner av högre ordning som gäller för en funktion. Så till exempel uttrycket

${\ displaystyle \ sum _ {x \ i S} {x^{2}}}$

kan behandlas som en notation för

${\ displaystyle \ sum _ {S} {(x \ mapsto x^{2})}}$

var är en operatör med två parametrar-en enparameterfunktion och en uppsättning för att utvärdera den funktionen över. De andra operatörerna som anges ovan kan uttryckas på liknande sätt; till exempel, den universella kvantifierare kan betraktas som en operator som utvärderas till den logiskt samband av boolean-värd funktion P appliceras över (eventuellt oändlig) uppsättning S . ${\ displaystyle \ sum _ {S} {f}}$ ${\ displaystyle \ forall x \ i S \ P (x)}$

Naturligt språk

När de analyseras i formell semantik kan naturliga språk ses ha fria och bundna variabler. På engelska kan personliga pronomen som han , hon , de , etc. fungera som fria variabler.

Lisa hittade sin bok.

I meningen ovan är det possessiva pronomenet henne en ledig variabel. Det kan hänvisa till den tidigare nämnda Lisa eller till någon annan kvinna. Med andra ord kan hennes bok syfta på Lisas bok (ett exempel på korrespondens ) eller på en bok som tillhör en annan kvinna (t.ex. Janes bok). Vem som helst som referensen till henne kan fastställas utifrån det situationella (dvs. pragmatiska ) sammanhanget. Referensens identitet kan visas med hjälp av samindexering av abonnemang där i indikerar en referens och j indikerar en andra referens (annorlunda än i ). Således har meningen Lisa hittade sin bok följande tolkningar:

Lisa _Jag fann henne _i boken. (tolkning #1: henne = av Lisa )

Lisa _Jag fann henne _j bok. (tolkning #2: henne = av en hona som inte är Lisa)

Skillnaden är inte enbart av akademiskt intresse, eftersom vissa språk faktiskt har olika former för henne _i och hennes _j : till exempel översätter norska och svenska coreferent her _i som synd och noncoreferent hennes _j som hennes .

Engelska tillåter visserligen att specificera referens, men det är valfritt, eftersom båda tolkningarna av det föregående exemplet är giltiga (den ogrammatiska tolkningen indikeras med en asterisk):

Lisa _Jag fann henne _i egen bok. (tolkning #1: henne = av Lisa )

* Lisa _Jag hittade henne _j egen bok. (tolkning #2: henne = av en hona som inte är Lisa)

Men reflexiva pronomen , som han själv , sig själv , sig själv , etc. och ömsesidiga pronomen , som varandra , fungerar som bundna variabler. I en mening som följande:

Jane skadade sig själv .

reflexen själv kan bara hänvisa till det tidigare nämnda föregångaren , i detta fall Jane , och kan aldrig hänvisa till en annan kvinnlig person. I detta exempel är variabeln själv bunden till substantivet Jane som förekommer i ämnesposition . För att indikera sammankopplingen är den första tolkningen med Jane och hon självindexerad tillåten, men den andra tolkningen där de inte är sammanlänkade är ogrammatisk :

Jane _Jag skadar sig _i . (tolkning #1: sig själv = Jane )

* Jane _jag skadade sig själv _j . (tolkning #2: sig själv = en kvinna som inte är Jane)

Observera att referensbindningen kan representeras med hjälp av ett lambda -uttryck som nämnts i föregående avsnitt om formell förklaring . Meningen med reflexen kan representeras som

(λ x . x skadar x ) Jane

där Jane är ämnesreferensargumentet och λx.x skadar x är predikatfunktionen (en lambda -abstraktion) med lambda -notationen och x indikerar både det semantiska subjektet och det semantiska objektet i meningen som bundna. Detta återger den semantiska tolkningen JANE skadade JANE med JANE som samma person.

Pronomin kan också bete sig på ett annat sätt. I meningen nedan

Ashley slog henne .

pronomenet her kan bara referera till en kvinna som inte är Ashley. Det betyder att det aldrig kan ha en reflexiv betydelse som motsvarar Ashley -slaget själv . De grammatiska och ogrammatiska tolkningarna är:

* Ashley _jag slog henne _i . (tolkning #1: henne = Ashley )

Ashley _jag slog henne _j . (tolkning #2: henne = en hona som inte är Ashley)

Den första tolkningen är omöjlig. Endast den andra tolkningen är tillåten av grammatiken.

Således kan det ses att reflexer och ömsesidiga är bundna variabler (tekniskt kända som anaforer ) medan sanna pronomen är fria variabler i vissa grammatiska strukturer men variabler som inte kan bindas i andra grammatiska strukturer. De bindande fenomen som finns i naturliga språk var särskilt viktiga för den syntaktiska regeringen och bindande teori (se även: Bindning (lingvistik) ).

Se även

• Avslutning (datavetenskap)
• Kombinerande logik
• Lambda lyft
• Namnbindning
• Omfattning (programmering)

Referenser

• Thompson, Simon (1991). Typteori och funktionell programmering . Wokingham, England: Addison-Wesley. ISBN 0201416670. OCLC  23287456 .