Voltar


Calculo Lambda

Cálculo Lambda

 

Histórico

       Linguagens Funcionais

Utilidade do Cálculo Lambda em Programação Funcional

Fundamentos Teóricos

     A Sintaxe do Cálculo Lambda

       Implementação de um Programa Lambda

       A Semântica Operacional do Cálculo Lambda

       Ordem de Redução

       Funções Recursivas

 

 

 

 

 

 

1.                    Histórico:

 

A elaboração de modelos de computação (resolução de problemas por uma máquina) baseia-se em trabalhos de dois pesquisadores com enfoques bastante diferentes:

 

  - Máquinas de Turing (Alan Turing, 1936)

  - Cálculo Lambda (Alonzo Church, 1936)

 

  Alan Turing provou em 1937 a equivalência entre uma Máquina de Turing e o Cálculo Lambda em termos de computabilidade.

 

 

Linguagens Funcionais:

 

• Interessantes pela sua simplicidade sintática

• Facilidade de descrever problemas recursivos.

• Maioria das implementações são poucos aceitas devido à ineficiência em comparação com linguagens de programação ''tradicionais".

Novas implementações de interpretadores/compiladores e novas linguagens mais modernas tem ressurgido.

 

Exemplos:

 

- LISP (LISt Processing - década de 60). Muito simples em muitos aspectos. Atuamente é ainda a mais utilizada.

- Miranda (Turner 1985)

- Haskell (1990)

- Orwell (Wadler 1985)

- Outras: ML, KRC, LML, SASL.

topo

 

 

 

Utilidade do Cálculo Lambda em Programação Funcional:

 

Ponto de Partida: Maioria da Linguagens de Programação Funcional são semelhantes e diferem somente em aspectos sintáticos .

topo

 

2.                    Fundamentos Teóricos

 

O cálculo lambda  é uma coleção de diversos sistemas formais baseados em uma notação para funções inventada por Alonzo Church em 1936  com o intuito de capturar os aspectos mais básicos da maneira pela qual operadores ou funções podem ser combinados para formar outros operadores.

 

O cálculo lambda serve como uma ponte entre linguagens funcionais de alto nível e suas implementavéis de baixo nível. Raízes para a apresentação do cálculo lambda como uma linguagem intermediária: uma linguagem extremamente simples, consistindo de somente algumas poucas construções sintáticas e de uma semântica simples.

 

Uma implementação do cálculo lambda necessita somente suportar algumas construções simples.

 

A sua semântica simples nos permite analisar facilmente a correção de sua implementação.

 

Trata-se de uma linguagem expressiva, a qual é suficientemente poderosa para expressar todos os programas funcionais e, por conseguinte, todas as funções computáveis. Isto significa que, se uma boa implementação do cálculo lambda é disponível, pode-se implementar qualquer linguagem funcional através da implementação de um compilador desta para o cálculo lambda.

 

 

2.1. A Sintaxe do Cálculo Lambda

 

A linguagem do cálculo lambda usa um alfabeto S constituído de:

 

- um conjunto de variáveis: vo, v1, v2,....vn....

- abstrator l (lambda)

- agrupadores (,)

 

Ao conjunto de cadeias finitas sobre S denota-se por S* e a cadeia que não contem elementos denota-se por e. Usam-se as variáveis x, y, z, ... para denotar cadeias de S*.

 

Definicão (Equivalência de duas cadeias)

Duas cadeias x e y são equivalentes e se escreve (x,y) Œ ∫    x = y

 

Definicão (Comprimento de uma cadeia)

É uma função:

ln:  S*  Æ Z+

em que o número inteiro exprime o número de elementos da cadeia.

 

Definicão (Termo Lambda)

 

Um termo lambda, denotado pelas letras M, N, O, P,.. é um elemento da linguagem L, onde  S*   L definido da seguinte forma:

 

         - vi é termo lambda;

         - dado M, (lvi M) é termo lambda;

         - dados dois termos lambda M, N então (MN) é termo

         lambda;

         - e nada mais é termo lambda.

 

Exemplos:

 

Verificar quais das expressões são termos lambda.

 

  vo                                     (vov1)                       (vo)

(lvo(vov1))                 (lv1(vo(lv1(vov1))))           (lvo(vov1)

 

Esta notação é precisa, mas bastante pesada. Algumas vezes, é conveniente introduzir mais algumas convenções com a finalidade de simplificar a notação. São quatro as principais convenções:

 

1-Precedência à esquerda.

  Assim, ((MN)L) pode ser escrita MNL

 

2-Sucessão de abstratores:

  (lx(ly(lz........)))  se escreve  lxyz...

 

3-Separador: usa-se um ponto para designar o final de uma lista de argumentos lambda

  Assim lx.xly.y  = (lx(x(ly.y)))

 

4-Supõe-se que letras diferentes designam entidades diferentes.

Assim x π y em lx.y

 

 

Exemplo Concreto

 

 Um exemplo simples de uma expressão em cálculo lambda é:

(+ 4 5)

topo

 

 

2.2 Implementação de um Programa Lambda

 

Um programa Lambda se escreve como um conjunto de expressões lambda. Normalmente, usando notação simplificada encontra-se o símbolo lambda seguido de lista de variáveis. Limitando estas variáveis vem um ponto ".'', seguido pelo corpo da função. As variáveis são chamadas de parâmetros formais e diz-se que o lambda os liga. Assim, seja :

 

lx.(x + 1)

 

O exemplo acima pode ser lido: ''Aquela ( ) função de (x) a qual (.) adiciona x a 1. Algumas vezes costuma-se usar operadores sempre prefixados, e neste caso se escreveria (+ x 1). Para calcular o valor da função para x = 5 se escreve:

 

lx.(x + 1).5

 

  Uma abstração lambda sempre consiste dessas partes: o l, o parâmetro formal,  e o corpo. Uma abstração lambda pode ser considerada similar a uma definição de função em uma linguagem de programação. convencional, como ''C":

 

        inc ( x )

        int x;

       ( return( x + 1); )

 

 

Funções Embutidas e Constantes

 

Funções embutidas como + não existem no cálculo lambda na sua forma mais pura. Para fins práticos, uma extensão que as suporte é útil. Estas incluem funções aritméticas (como +, -, *, /), constantes (como 0, 1,...), funções lógicas (como AND, NOT, OR,...) e constantes lógicas (TRUE, FALSE).

 

Exemplos:

 

- 5 4 -> 1

AND TRUE FALSE -> FALSE

 

Também incluímos uma função condicional, cujo valor é descrito pelas regras de redução abaixo:

IF TRUE E t E f ->E t

IF FALSE E t E f ->E f

 

Construtores de dados em cálculo lambda serão introduzidos inicialmente através da definição de três funções embutidas: CONS, HEAD e TAIL (as quais se comportam exatamente como as funções LISP: CONS, CAR e CDR).

CONS constrói um objeto composto, o qual pode ser desmantelado com HEAD e  TAIL. A operação é descrita pelas seguintes regras de redução:

 

                          HEAD (CONS a b) ->a

                          TAIL (CONS a b)  ->b

 

Além dessas funções , define-se a constante NIL, o valor nulo.

 A escolha exata de funções embutidas é arbitrária.

 

Abstrações Lambda

 

Abstrações lambda são construções em cálculo lambda que denotam funções novas, não embutidas em um cálculo específico.

 

Exemplo:

(lx . + x 1)

 

O l indica o início de uma função e é imediatamente seguido de uma variável.

 

A expressão (+ 3) denota a "funçåo + aplicada ao argumento 3", cujo resultado é uma ''funçåo aplicada ao valor 4".

Como em todas as linguagens funcionais, o cálculo lambda permite que uma função retorne uma função como resultado.

Este dispositivo nos permite imaginar todas as funções como possuindo somente um argumento.

Esta notação foi introduzida por Schonfinkel em 1924 e utilizada amplamente nos trabalhos de Curry, de onde provém a expressão currying.

 

  Todas as aplicações de funções no cálculo lambda são escritas em notação prefixada. Assim a função + precede os argumentos 4 e 5. Um exemplo um pouco mais complexo é:

 

(+ (* 5 6) (* 8 3))

 

  Do ponto de vista de implementação, um programa funcional pode ser visto como uma expressão, que é "executada'' através da sua avaliação. A avaliação ocorre através da seleção repetida de uma expressão redutível (redex) (abreviação do termo em inglêsreduced expression”' e de sua redução.

Expressão redutível é aquela que pode ser avaliada imediatamente.  No exemplo anterior existem dois redexes:

 

(* 5 6) e (* 8 3)

 

A expressão inteira (+ (* 5 6) (* 8 3)) não é um redex, uma vez que a função + necessita ser aplicada a dois números para poder ser redutível. Através da escolha arbitrária do primeiro redex para redução escreve-se:

 

(+ (* 5 6) (* 8 3)) -> (+ 30 (* 8 3))

 

onde -> le-se "reduz para''.

. Agora há somente um redex (* 8 3), do qual resulta: (+ 30 24)

. Esta redução gera um novo redex, que reduz: (+ 30 24) -> 54

topo

 

 

2.3. A Semântica Operacional do Cálculo Lambda

 

Até agora foi descrita a sintaxe do cálculo-l. Para chamá-lo de "cálculo'', devemos, porém dizer como "calcular'' com ele. Basicamente isto é realizado através de três regras de conversão, que descrevem como converter uma expressão-l em outra.

 

2.3.1.  Introdução a l-conversão: Variáveis atadas e livres (bound/free)

 

Seja a expressão-l:

                             (lx. + x y) 4

Para avaliar a expressão é necessário:

 

• saber o valor "global'' de y.

• não é necessário saber o valor global de x, pois é o parâmetro formal da função.

Vê-se que: x e y possuem um status bastante diferente.

  A razão é que x ocorre atado pelo lx, é somente um encaixe dentro do qual o argumento 4 é colocado quando a abstração-l for aplicada ao argumento. Por outro lado, y não é atado por nenhum e assim ocorre livre na expressão. A ocorrência de uma variável é atada se há uma expressão-l envolvente que a amarra, senão é livre. No exemplo a seguir, x e y ocorrem atados, z,   porém, ocorre livre:

lx. + ((ly. + y z) 7) x

Observe que os termos atado e livre se referem a ocorrências específicas da variável em uma expressão.

 

Resumindo a nomenclatura:

Uma aplicação-l é simplesmente a aplicação de uma expressão-l sobre outra. A primeira dessas duas expressões-l é chamada de operador, a segunda de operando.  Note que qualquer expressão-l pode ser utilizada tanto como operador como operando. Uma abstração-l é formada com o símbolo especial seguido por uma variável, seguida por um ponto, seguido por uma expressão arbitrária. . O propósito da operação de abstração é o de formar uma expressão unária a partir de uma expressão-l dada. A variável que ocorre próxima ao inicial do nome ao argumento. Funções com mais de um argumento são formadas por abstrações repetidas.

 

2.3.2. Conversão-Alfa

Considere:

(lx. + x 1) e (ly. + y 1)

  Evidentemente elas devem ser equivalentes. A conversão-a é o nome dado à operação de mudança de nome (consistente) de um parâmetro formal.

Notação:

(lx. + x 1) a (ly. + y 1)

a-congruência: duas expressões-l M e N são a-congruentes (ou a-equivalentes), denotado por M N se ou M=N ou M->N, ou N é obtido de M através da reposição de uma sub-expressão S de M por uma expressão-l T tal que S -> T, ou existe alguma expressão-l R tal que M -> R e R -> N.

 

 

Nomenclatura:

 

Nomes de parâmetros formais podem não ser únicos:

( x.( x. + ( - x 1)) x 3) 9 ( x. + (- x 1)) 9 3

+ (- 9 1) 3

11

 

Observe-se que o x interno não foi substituído na primeira redução, pois estava protegido pelo x envolvente, ou seja, a ocorrência interna de x não é livre no corpo da abstração x externa.

  Dada uma abstração-l, (lx.E), é possível identificar-se exatamente as ocorrências de x que deveriam ser substituídas através da identificação de todas as ocorrências de x que estão livres. Dessa forma, para o exemplo acima, examinamos o corpo da abstração:

( x. + (- x 1)) x 3

e vemos que a segunda ocorrência de x é livre, podendo ser substituída. A idéia do aninhamento do escopo de variáveis em uma linguagem de programação estruturada é análoga a esta regra.

  Outro exemplo:

 

          (lx. y.+ x (( x.- x 3) y)) 5 6

          (ly.+ 5 (( x.- x 3) y)) 6

          + 5 (( x.- x 3) 6)

          + 5 (- 6 3)

          8

 

Novamente, o x mais interno não é substituído, uma vez que não é livre no corpo da abstração mais externa.

 

  Nesse caso não há ocorrências do parâmetro formal (x), pelo qual o argumento 5 poderia ser substituído. Assim o argumento é descartado sem uso. O corpo de uma abstração poder ser constituído por outra abstração :

 

          (lx. (ly. - y x)) 4 5

          (ly. - y 4) 5

          - 5 4

          1

 

Observa-se que, ao se construir a instância do corpo da abstração x, o corpo inteiro inclusive a abstração y envolvida por esta, substituindo-se x, é copiado. Aqui se observa também o efeito do Currying: a aplicação da abstração x retornou uma função (a abstração y) como seu resultado. Esta por sua vez, aplicada resultou em ( - 5 4). Funções encapsuladas umas dentro das outras são comumente abreviadas:

(lx. (ly. E)) para (lx. y. E)

 

 

2.3.3. Conversão-Beta

 

Uma abstração-b denota uma função. Assim necessitamos descrever como aplicá-la a um argumento.

A função (lx. + x 1) 4 é a justaposição do função (lx. + x 1) e do argumento 4 e, por conseguinte, denota a aplicação de uma certa função, denotada pela abstração-l, ao argumento 4.

A regra para a aplicação de uma função é muito simples:

·                        O resultado da aplicação de uma abstração-l a um argumento é uma instância do corpo da abstração-l no qual ocorrências (livres) do parâmetro formal no corpo são repostas pelo argumento. O resultado de se aplicar a abstração ao argumento é: + 4 1 onde o (+ 4 1) é um instância do corpo (+ x 1) no qual ocorrências do parâmetro formal x foram repostas pelo argumento 4. Escreve-se as conversões utilizando o símbolo como antes:

                                  (lx. + x 1) 4

                                  + 4 1

                                  5

Esta operação é chamada de b-redução e a sua implementação eficiente é um aspecto importante na elaboração de linguagens de programação funcional.

Exemplos simples de b-redução:

O parâmetro formal pode ocorrer várias vezes no corpo:

                  (lx. + x x) 5

                  + 5 5

                  10

  Da mesma forma, pode não haver ocorrências do parâmetro formal no corpo. Ex:  (lx. 3) 5 3

 

Uma variável pode possuir tanto uma ocorrência atada como uma livre em uma expressão. Considere o exemplo:

+ x ((lx. + x 1) 4)

 

Aqui x ocorre livre (a primeira vez) e atada (a segunda). Cada ocorrência individual de uma variável deve ser ou atada ou livre.

As definições formais de livre a atado são dadas abaixo:

 

Definição de ocorre  livre:

• x ocorre livre em x (mas não em outra variável ou constante qualquer)

• x ocorre livre em (E F) se x ocorre livre em E ou x ocorre livre em F

• x ocorre livre em y.E x se x, y são variáveis diferentes e x ocorre livre em E

Nota: nenhuma variável ocorre atada em uma expressão consistindo e uma única constante.

Definição de ocorre atada:

• x ocorre atada em (E F) se x ocorre atada em E ou x ocorre atada em F

• x ocorre atada em y.E (x e y) são a mesma variável e x ocorre livre em E ou

  x ocorre atada em E

 

 

2.3.4. Conversão-Eta

 

Sejam: (lx. + 1 x) e (+ 1). Estas expressões se comportam exatamente da mesma maneira, quando aplicadas a um argumento: ambas adicionam 1 ao argumento. Conversão-z é o nome dado à regra que expressa essa equivalência. Assim:

(lx. + 1 x) -> (+ 1)

  De forma mais geral, a regra da conversão-z pode ser expressa assim:

(lx. F x) -> F

desde que x não ocorra livre em F e F denote uma função. A condição de que x não deve ocorrer livre em F previne conversões errôneas. Exemplo:

(lx. + x x) não é e-conversível para (+ x),

pois x ocorre livre em (+ x).

 

  A condição de que F deve denotar uma função previne outras conversões errôneas envolvendo constantes embutidas (pré-definidas). Exemplo: TRUE não é e-conversível para (lx. TRUE x)

  Quando a conversão-z é utilizada da esquerda para a direita, é chamada de redução-l

 

 

2.3.5 Resumo

 

As três regras de conversão que possibilitam a inter-conversão de expressões envolvendo abstrações-l:

1. Mudança de nome: a conversão-a permite que se troque o nome de par‚metros formais de uma abstração- , enquanto isto for feito de forma consistente.

2. Aplicação de funções: A redução-b permite a aplicação de abstrações- a um argumento através de geração de uma nova instância do corpo da abstração, substituindo o argumento por ocorrências livres do parâmetro formal. Cuidado especial deve ser tomado quando o argumento contém variáveis livres.

3. Eliminação de abstrações-l redundantes: A redução-z pode às vezes eliminar uma abstração-l . Dentro deste contexto, podemos considerar as funções embutidas (pré-definidas) como mais uma forma de conversão. Esta forma de conversão recebe o nome de conversão-z .

 

 

2.3.6. Provas de Inter-convertibilidade

 

Freqüentemente será necessário poder-se demonstrar a inter-convertibilidade de duas expressões-l. Quando as duas expressões denotam funções, esta prova pode se tornar extremamente longa. Há, porém, métodos para abreviar provas, que não sacrificam o seu rigor.

Exemplo: Sejam as duas expressões abaixo:

 ((lp.p) 3) e (lx. 3)

Ambas as expressões denotam a mesma função, que invariavelmente retorna o valor 3, não importa o valor de seu argumento e seria de se esperar que ambas sejam inter-convertíveis. Isto realmente ocorre:

IF TRUE (( p.p) 3) IF TRUE 3

( x. IF TRUE 3 x)

( x. 3)

 

onde o passo final é a regra de redução para IF.

  Um método alternativo de se provar a inter-convertibilidade de duas expressões, muito mais conveniente, é o de se aplicar as duas expressões a um argumento w.

topo

 

2.4. Ordem de Redução

       Se uma expressão não contém mais redexes, então a avaliação está completa. Uma expressão nesta forma é dita estar na forma normal.

       Assim, a avaliação de uma expressão consiste na  redução sucessiva de redexes, até que a expressão esteja na forma normal.

       Definição (forma normal): uma expressão-l é dita estar na forma normal, se nenhum redex-b, isto é, nenhuma sub-expressão da forma (lx.P)Q ocorre nela.

       Uma expressão pode conter mais do que um redex, assim a redução pode acontecer por caminhos diferentes.

       Exemplo:

(+ (* 3 4) (* 7 8))

pode ser reduzido à forma normal pelas seguintes seqüências: (+ (* 3 4) (* 7 8))

-> (+ 12 (* 7 8))
-> (+ 12 56)
-> 68

ou

(+ (* 3 4) (* 7 8))
-> (+ (* 3 4) 56)
-> ( 12 56)
-> 68

       Nem toda expressão possui uma forma normal,
considere:

(D D)

       onde D é (lx.x x). A avaliação desta expressão jamais terminaria, uma vez que (D D) reduz para (D D):

  (lx.x x)(lx.x x) -> (lx.x x)(lx.x x)
-> (
lx.x x)(lx.x x)

       Por conseguinte, algumas seqüências de redução poderão atingir a forma normal, outras não. Considere:

(lx.3) (D D)

       Se nós primeiro reduzirmos a aplicação de (lx.3) a (D D) (sem avaliar (D D)), obteremos o resultado 3; porém se primeiro reduzimos a aplicação de D sobre D, nós simplesmente obtemos (D D) novamente.

       Se nós continuamos insistindo em escolher a aplicação de D sobre D, a avaliação vai continuar indefinidamente, não terminando.

       Esta situação corresponde à de um programa imperativo que entra em um laço infinito. Dizemos que a avaliação ou execução não termina.

       Para contornar esta situação, existe a ordem normal de redução, que garante que uma forma normal, caso exista, será encontrada.

 

 

2.4.1. Ordem Normal de Redução

 

       Uma questão que se coloca, além da questão "poderei encontrar uma forma normal ?", é a questão de se existe mais de uma forma normal para uma expressão, ou:

    Poderá uma seqüência de redução diferente levar a uma forma normal diferente?

    Ambas as questões estão interligadas.

       A resposta para a última pergunta é: não.
    Isto é uma conseqüência dos teoremas de Church-Rosser TCR1 e TCR2.

 

 

Teorema de Church-Rosser 1 (TCR1):

 

Se E1 <-> E2, então existe uma expressão E, tal que

E1 -> E e E2 -> E

Corolário: Nenhuma expressão pode ser convertida em duas formas normais distintas. Isto significa que não existem duas formas normais para uma expressão que não sejam a-convertíveis entre si.

 

Prova:

Suponha que E1 <-> E e E2 <-> E , onde E1 e E2 estão na forma normal.
      

Então E1 <-> E2 e, pelo TCR1, deve haver uma expressão F tal que E1 -> F e E2 -> F.
Como tanto E1 como E2 não possuem redexes, logo E1 = F = E2

       Informalmente, o teorema TCR1 diz que todas as seqüências de redução que terminam, haverão de atingir o mesmo resultado.

    O segundo teorema de Church-Rosser, TCR2, diz respeito a uma ordem particular de redução, chamada ordem normal de redução.

 

 

Teorema de Church-Rosser 2 (TCR2):

 

Se E1 -> E2, e E2 está na forma normal, então existe uma ordem normal  de seqüência de redução de E1 para E2.

 

Conseqüências:

       Existe no mínimo um resultado possível e

       a ordem normal de redução encontrará este resultado, caso ele exista.

       Observe que nenhuma seqüência de redução poderá levar a um resultado incorreto, o máximo que poderá acontecer é a não-terminação. A Ordem Normal de Redução especifica que o redex mais à esquerda mais externo deverá ser reduzido primeiro.

       No exemplo anterior (lx.3) (D D), escolheríamos o redex-lx primeiro, não o (D D).

       Esta regra encorpa a intuição de que argumentos para funções podem ser descartados, de forma que deveríamos aplicar a função (lx.3) primeiro, ao invés de primeiro avaliarmos o argumento (D D).

 

2.4.2. Ordens de redução ótimas

       Enquanto a ordem normal de redução garante que ou uma solução seja encontrada ou o não-término ocorra, ela não garante que isto ocorra no número mínimo de passos de redução, o que é um fato relevante na utilização do cálculo-l para a implementação de linguagens de programação interpretadas.

       No caso da implementação da resolução através de redução de grafos - que estudaremos mais tarde - porém, aparentemente a ordem normal de redução é "geralmente ótima" em questão de tempo de execução.

  Analisar uma expressão para encontrar o redex ótimo para ser reduzido é aparentemente muito mais trabalhoso e gasta mais tempo do que arriscar uma redução com mais passos seguindo "cegamente" a ordem normal.

       Alguns autores como (Levy, J.J.; Optimal Reductions in the Lambda Calculus in Essays on Combinatory Logic, Academic Press, 1980) se ocuparam de algoritmos para encontrar ordens ótimas ou quase-ótimas de redução que preservassem as qualidades da ordem normal de redução. Isto é assunto de um tópico avançado que não cabe nesta disciplina.

topo

 

2.5. Funções Recursivas

 

       Se o propósito da utilização de cálculo lambda é a conversão de programas funcionais neste para que possamos resolvê-los, devemos ser capazes de representar uma das características mais marcantes das linguagens funcionais, a recurssão.

       O cálculo lambda suporta a representação de recursividade sem maiores extensões através da utilização de alguns pequenos truques.

 

2.5.1. Funções Recursivas e o Y

       Considere a definição da função fatorial abaixo:

FAC = (ln.IF (= n 0) 1 (* n (FAC (- n 1))))

       Esta definição baseia-se na capacidade de se dar um nome a uma abstração lambda e de fazer referência a esta dentro dela mesma.

       Nenhuma construção deste tipo é provida pelo cálculo lambda.

       O maior problema aqui é que funções lambda são anônimas.

       Dessa forma elas não podem nomear-se e assim não podem se referenciar a si mesmas.

Para resolver este problema iniciamos com um caso onde encontramos a recursão na sua forma mais pura:

FAC = (ln. ... FAC ... )

       Aplicando uma abstração-b sobre FAC, usada de modo inverso, pode-se transformar esta definição em:

FAC = (lfac.(ln. (...fac...)))FAC

       Esta definição pode ser escrita da forma:

                         FAC = H FAC                                     (2.1)

       onde:

H = (lfac.(ln. (...fac...)))

       A definição de H é trivial. É uma abstração lambda ordinária e não usa recursão.

       A recursão é expressa somente pela definição 2.1.

  A definição 2.1 pode ser encarada mais como uma equação matemática. Por exemplo, para resolver a equação matemática

x2 - 2 = x

 

procura-se por valores de x que satisfaçam