Zmienne wolne i zmienne powiązane - Free variables and bound variables

W matematyce i innych dyscyplinach obejmujących języki formalne , w tym w logice matematycznej i informatyce , zmienna wolna jest zapisem (symbolem) określającym miejsca w wyrażeniu, w których może nastąpić podstawienie, i nie jest parametrem tego ani żadnego wyrażenia kontenerowego. Niektóre starsze książki używają terminów zmienna rzeczywista i zmienna pozorna odpowiednio dla zmiennej wolnej i zmiennej związanej. Pomysł jest powiązany z placeholderem ( symbolem , który później zostanie zastąpiony jakąś wartością) lubsymbol wieloznaczny, który oznacza nieokreślony symbol.

W programowaniu komputerowym termin wolna zmienna odnosi się do zmiennych używanych w funkcji , które nie są ani zmiennymi lokalnymi, ani parametrami tej funkcji. Termin zmienna nielokalna jest często w tym kontekście synonimem.

Zmienna związana jest zmienną, która była poprzednio darmo , ale został zobowiązany do wartości określonej lub zbioru wartości zwanych domeny dyskursu lub wszechświata . Na przykład zmienna x staje się zmienną związaną, gdy piszemy:

Dla wszystkich x , ( x + 1) ² = x ² + 2 x + 1 .

lub

Istnieje x takie, że x ² = 2 .

W obu tych twierdzeniach nie ma logicznie znaczenia, czy użyto x, czy jakaś inna litera. Jednak może być mylące ponowne użycie tej samej litery w innym miejscu w jakiejś złożonej propozycji . Oznacza to, że wolne zmienne zostają powiązane, a następnie w pewnym sensie wycofują się z bycia dostępnymi jako wartości zastępcze dla innych wartości przy tworzeniu formuł.

Termin „zmienna fikcyjna” jest również czasami używany dla zmiennej powiązanej (częściej w matematyce ogólnej niż w informatyce), ale takie użycie może spowodować niejednoznaczność definicji zmiennych fikcyjnych w analizie regresji .

Przykłady

Zanim podamy dokładną definicję zmiennej wolnej i zmiennej związanej , poniżej znajduje się kilka przykładów, które mogą sprawić, że te dwa pojęcia będą bardziej zrozumiałe niż definicja:

W wyrażeniu

${\ Displaystyle \ suma _ {k = 1} ^ {10} f (k, n)}$

n jest zmienną wolną, a k jest zmienną związaną; w konsekwencji wartość tego wyrażenia zależy od wartości n , ale nie ma niczego, co nazywa się k, od którego mogłoby ono zależeć.

W wyrażeniu

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

y jest zmienną wolną, a x jest zmienną związaną; w konsekwencji wartość tego wyrażenia zależy od wartości y , ale nie ma niczego, co nazywa się x, od którego mogłoby ono zależeć.

W wyrażeniu

${\ Displaystyle \ lim _ {h \ rightarrow 0} {\ Frac {f (x + h)-f (x)} {h}}}$

x jest zmienną wolną, a h jest zmienną związaną; w konsekwencji wartość tego wyrażenia zależy od wartości x , ale nie ma niczego, co nazywa się h, od którego mogłoby ono zależeć.

W wyrażeniu

${\ Displaystyle \ forall x \ \ istnieje r \ {\ duży [} \ varphi (x, y, z) {\ duży]},}$

z jest zmienną wolną, a x i y są zmiennymi związanymi, powiązanymi z kwantyfikatorami logicznymi ; w konsekwencji wartość logiczna tego wyrażenia zależy od wartości z , ale nie istnieje nic takiego jak x lub y, od którego mogłoby ono zależeć.

Szerzej, w większości dowodów używamy zmiennych powiązanych. Na przykład poniższy dowód pokazuje, że każdy kwadrat parzystej liczby całkowitej jest podzielny przez${\ Displaystyle 4}$

Niech będzie dodatnią parzystą liczbą całkowitą. Następnie jest liczba całkowita taka, że . Ponieważ mamy podzielne przez${\ Displaystyle n}$${\displaystyle k}$${\displaystyle n=2k}$${\ Displaystyle n ^ {2} = 4 k ^ {2}}$${\displaystyle n^{2}}$${\ Displaystyle 4}$

nie tylko k, ale także n zostały użyte jako zmienne powiązane jako całość w dowodzie.

Operatory ze zmiennymi wiązaniami

Następujące

${\ Displaystyle \ suma _ {x \ w s} \ quad \ quad \ prod _ {x \ w s} \ quad \ quad \ int _ {0} ^ {\ infty} \ cdots \, dx \ quad \ quad \ lim _{x\to 0}\quad \quad \forall x\quad \quad \exists x}$

to kilka typowych operatorów wiążących zmienne . Każdy z nich wiąże zmienną x dla pewnego zbioru S .

Zauważ, że wiele z nich to operatory, które działają na funkcje zmiennej powiązanej. W bardziej skomplikowanych kontekstach takie zapisy mogą stać się niezręczne i mylące. Przydatne może być przełączenie się na notacje, które czynią wiązanie wyraźnym, na przykład

${\ Displaystyle \ suma _ {1, \ ldots, 10} \ lewo (k \ mapsto f (k, n) \ prawo)}$

dla kwot lub

${\ Displaystyle D \ lewo (x \ mapsto x ^ {2} + 2 x + 1 \ po prawej)}$

do zróżnicowania.

Formalne wyjaśnienie

Drzewo podsumowujące składnię wyrażenia ${\displaystyle \forall x\((\istnieje y\,A(x))\vee B(z))}$

Mechanizmy wiązania zmiennych występują w różnych kontekstach w matematyce, logice i informatyce. We wszystkich jednak przypadkach są to czysto syntaktyczne właściwości wyrażeń i zawartych w nich zmiennych. W tej sekcji możemy podsumować składnię, identyfikując wyrażenie z drzewem, którego węzły liści są zmiennymi, stałymi, stałymi funkcyjnymi lub stałymi predykatów, a węzły nie będące liśćmi są operatorami logicznymi. Wyrażenie to można następnie określić, wykonując inorder przechodzenia drzewa. Operatory powiązania zmiennych to operatory logiczne, które występują w prawie każdym języku formalnym. Operator powiązania Q przyjmuje dwa argumenty: zmienną v i wyrażenie P , a po zastosowaniu do jego argumentów tworzy nowe wyrażenie Q( v , P ). Znaczenie operatorów wiążących jest dostarczane przez semantykę języka i nie dotyczy nas tutaj.

Wiązanie zmiennej dotyczy trzech rzeczy: zmiennej v , lokalizacji a dla tej zmiennej w wyrażeniu oraz węzła nie będącego liściem n postaci Q( v , P ). Uwaga: definiujemy lokalizację w wyrażeniu jako węzeł liścia w drzewie składni. Powiązanie zmiennej występuje, gdy ta lokalizacja znajduje się poniżej węzła n .

W rachunku lambda , xjest zmienną związaną w wyrażeniu M = λx. Ti zmienną wolną w wyrażeniu T. Mówimy, że xjest związany Mi wolny T. Jeśli Tzawiera subterm λx. Unastępnie xjest odbicie w tym okresie. xMówi się, że to zagnieżdżone, wewnętrzne wiązanie „zacienia” zewnętrzne wiązanie. Wystąpienia xw Uto bezpłatne wystąpienia nowego x.

Zmienne powiązane na najwyższym poziomie programu są technicznie wolnymi zmiennymi w warunkach, z którymi są związane, ale często są traktowane specjalnie, ponieważ mogą być kompilowane jako stałe adresy. Podobnie identyfikator powiązany z funkcją rekurencyjną jest technicznie wolną zmienną w swoim własnym ciele, ale jest traktowany specjalnie.

Zamknięty termin jest nie zawierające zmienne wolne.

Wyrażenia funkcyjne

Aby podać przykład z matematyki, rozważ wyrażenie definiujące funkcję

${\ Displaystyle f = \ lewo [(x_ {1}, \ ldots, x_ {n}) \ mapsto t \ prawo]}$

gdzie t jest wyrażeniem. t może zawierać niektóre, wszystkie lub żadne z x ₁ , …, x _n i może zawierać inne zmienne. W tym przypadku mówimy, że definicja funkcji wiąże zmienne x ₁ , …, x _n .

W ten sposób, funkcja definicja wyrażenia w rodzaju przedstawionej powyżej, może być uważany za zmienny wiążący operatora, analogiczny do wyrażenia lambda lambda rachunku . Inne operatory wiążące, takie jak znak sumy , można traktować jako funkcje wyższego rzędu mające zastosowanie do funkcji. Na przykład wyrażenie

${\ Displaystyle \ suma _ {x \ w S} {x ^ {2}}}$

może być traktowany jako notacja dla

${\ Displaystyle \ suma _ {S} {(x \ mapsto x ^ {2})}}$

gdzie jest operatorem z dwoma parametrami — funkcją jednoparametrową i zestawem do oceny tej funkcji. Inne wymienione powyżej operatory można wyrazić w podobny sposób; Na przykład, kwantyfikator mogą być traktowane jako podmiot, którego wartość logiczna połączeniu z logicznego wartościach funkcji P nakłada się na nieskończonej) (ewentualnie zestawu S . ${\ Displaystyle \ suma _ {S} {f}}$ ${\ Displaystyle \ forall x \ w S \ P (x)}$

Język naturalny

Analizując semantykę formalną , można zauważyć, że języki naturalne mają zmienne wolne i związane . W języku angielskim zaimki osobowe takie jak he , ona , they itd. mogą działać jako zmienne wolne.

Lisa znalazła swoją książkę.

W powyższym zdaniu zaimek dzierżawczy her jest zmienną swobodną. Może odnosić się do wspomnianej wcześniej Lisy lub dowolnej innej kobiety. Innymi słowy, jej książka może odnosić się do książki Lisy (przykład współreferencji ) lub do książki należącej do innej kobiety (np. książka Jane). Kimkolwiek referent od niej to może być ustalona zgodnie z sytuacyjnej (tj pragmatycznej ) kontekście. Tożsamość referenta można pokazać za pomocą indeksów współindeksujących, gdzie i wskazuje jeden referent, a j wskazuje drugi referent (inny niż i ). Tak więc zdanie, które Lisa znalazła w swojej książce, ma następujące interpretacje:

Lisa _i znalazł ją _í książkę. (interpretacja #1: jej = Lisy )

Lisa _i znalazł jej _j książkę. (interpretacja #2: jej = kobiety, która nie jest Lisą)

Rozróżnienie to nie ma charakteru czysto akademickiego, ponieważ niektóre języki mają w rzeczywistości różne formy jej _i i jej _j : na przykład norweski i szwedzki tłumaczą coreferent her _i jako grzech, a noncoreferent her _j jako hennes .

Angielski pozwala na określenie koreferencji, ale jest to opcjonalne, ponieważ obie interpretacje poprzedniego przykładu są ważne (interpretacja niegramatyczna jest oznaczona gwiazdką):

Lisa _i ją znalazł _i właścicielem książkę. (interpretacja #1: jej = Lisy )

* Lisa _i znalazł jej _j własną książkę. (interpretacja #2: jej = kobiety, która nie jest Lisą)

Jednak zaimki zwrotne , takie jak on sam , sama , siebie , itp. oraz zaimki odwrotne , takie jak siebie nawzajem , działają jako zmienne związane. W zdaniu podobnym do poniższego:

Jane zraniła się .

sama refleksyjna może odnosić się tylko do wcześniej wspomnianego poprzednika , w tym przypadku Jane , i nigdy nie może odnosić się do innej osoby płci żeńskiej. W tym przykładzie sama zmienna jest powiązana z rzeczownikiem Jane występującym w pozycji podmiotu . Wskazując na koindeksację, pierwsza interpretacja z Jane i nią samą jest dozwolona, ​​ale druga interpretacja, w której nie są współindeksowani, jest niegramatyczna :

Jane _i zranić sobie _ja . (interpretacja #1: ona = Jane )

* Jane _i zranić sobie _j . (interpretacja #2: ona = kobieta, która nie jest Jane)

Zauważ, że wiązanie coreference może być reprezentowane przy użyciu wyrażenia lambda, jak wspomniano w poprzedniej sekcji Formalne wyjaśnienie . Zdanie ze zwrotem można przedstawić jako

(λ x . x boli x )Jane

w którym Jane jest argumentem referencyjnym podmiotu, a λx.x hurt x jest funkcją predykatu (abstrakcja lambda) z notacją lambda, a x wskazuje zarówno podmiot semantyczny, jak i obiekt semantyczny zdania jako związane. To zwraca semantycznej interpretacji JANE boli JANE z JANE jest ta sama osoba.

Zaimki mogą również zachowywać się w inny sposób. W zdaniu poniżej

Ashley ją uderzyła .

zaimek her może odnosić się tylko do kobiety, która nie jest Ashley. Oznacza to, że to nigdy nie może mieć odruchowego znaczenia odpowiadającego uderzeniu się Ashley . Interpretacje gramatyczne i niegramatyczne to:

* Ashley _i uderzył ją _ja . (interpretacja #1: ona = Ashley )

Ashley _i uderzyła się w _j . (interpretacja #2: ona = kobieta, która nie jest Ashley)

Pierwsza interpretacja jest niemożliwa. Gramatyka dopuszcza tylko drugą interpretację.

Można więc zauważyć, że zwroty i odwrotności są zmiennymi związanymi (znanymi technicznie jako anafory ), podczas gdy prawdziwe zaimki są zmiennymi wolnymi w niektórych strukturach gramatycznych, ale zmiennymi, których nie można powiązać w innych strukturach gramatycznych. Zjawiska wiążące występujące w językach naturalnych były szczególnie ważne dla rządu syntaktycznego i teorii wiążącej (patrz też: Binding (lingwistyka) ).

Zobacz też

• Zamknięcie (informatyka)
• Logika kombinacyjna
• Podnoszenie lambdy
• Wiązanie nazwy
• Zakres (programowanie)

Bibliografia

• Thompson, Simon (1991). Teoria typów i programowanie funkcjonalne . Wokingham, Anglia: Addison-Wesley. Numer ISBN 0201416670. OCLC  23287456 .