Codificação Mogensen-Scott - Mogensen–Scott encoding

Na ciência da computação , a codificação Scott é uma maneira de representar tipos de dados (recursivos) no cálculo lambda . A codificação da igreja executa uma função semelhante. Os dados e operadores formam uma estrutura matemática que está embutida no cálculo lambda.

Enquanto a codificação de Church começa com representações dos tipos de dados básicos e se desenvolve a partir deles, a codificação de Scott começa com o método mais simples para compor tipos de dados algébricos .

A codificação Mogensen – Scott estende e modifica ligeiramente a codificação Scott aplicando a codificação à Metaprogramação . Esta codificação permite a representação de termos de cálculo lambda , como dados, a serem operados por um metaprograma.

História

A codificação de Scott aparece pela primeira vez em um conjunto de notas de aula não publicadas por Dana Scott, cuja primeira citação ocorre no livro Combinatorial Logic, Volume II . Michel Parigot deu uma interpretação lógica de um recursor fortemente normalizado para numerais codificados por Scott, referindo-se a eles como a representação de números do "tipo pilha". Torben Mogensen posteriormente estendeu a codificação Scott para a codificação dos termos Lambda como dados.

Discussão

O cálculo lambda permite que os dados sejam armazenados como parâmetros para uma função que ainda não possui todos os parâmetros necessários para a aplicação. Por exemplo,

${\ displaystyle ((\ lambda x_ {1} \ ldots x_ {n}. \ lambda cc \ x_ {1} \ ldots x_ {n}) \ v_ {1} \ ldots v_ {n}) \ f}$

Pode ser considerado como um registro ou estrutura onde os campos foram inicializados com os valores . Esses valores podem então ser acessados ​​aplicando o termo a uma função f . Isso se reduz a, ${\ displaystyle x_ {1} \ ldots x_ {n}}$${\ displaystyle v_ {1} \ ldots v_ {n}}$

${\ displaystyle f \ v_ {1} \ ldots v_ {n}}$

c pode representar um construtor para um tipo de dados algébrico em linguagens funcionais como Haskell . Agora, suponha que haja N construtores, cada um com argumentos; ${\ displaystyle A_ {i}}$

${\ displaystyle {\ begin {array} {c | c | c} {\ text {Construtor}} & {\ text {Argumentos dados}} & {\ text {Resultado}} \\\ hline ((\ lambda x_ { 1} \ ldots x_ {A_ {1}}. \ Lambda c_ {1} \ ldots c_ {N} .c_ {1} \ x_ {1} \ ldots x_ {A_ {1}}) \ v_ {1} \ ldots v_ {A_ {1}}) & f_ {1} \ ldots f_ {N} & f_ {1} \ v_ {1} \ ldots v_ {A_ {1}} \\ ((\ lambda x_ {1} \ ldots x_ {A_ {2}}. \ Lambda c_ {1} \ ldots c_ {N} .c_ {2} \ x_ {1} \ ldots x_ {A_ {2}}) \ v_ {1} \ ldots v_ {A_ { 2}}) & f_ {1} \ ldots f_ {N} & f_ {2} \ v_ {1} \ ldots v_ {A_ {2}} \\\ vdots & \ vdots & \ vdots \\ ((\ lambda x_ { 1} \ ldots x_ {A_ {N}}. \ Lambda c_ {1} \ ldots c_ {N} .c_ {N} \ x_ {1} \ ldots x_ {A_ {N}}) \ v_ {1} \ ldots v_ {A_ {N}}) & f_ {1} \ ldots f_ {N} & f_ {N} \ v_ {1} \ ldots v_ {A_ {N}} \ end {array}}}$

Cada construtor seleciona uma função diferente dos parâmetros da função . Isso fornece ramificação no fluxo do processo, com base no construtor. Cada construtor pode ter uma aridade diferente (número de parâmetros). Se os construtores não tiverem parâmetros, o conjunto de construtores atua como um enum ; um tipo com um número fixo de valores. Se os construtores tiverem parâmetros, estruturas de dados recursivas podem ser construídas. ${\ displaystyle f_ {1} \ ldots f_ {N}}$

Definição

Deixe- D ser um tipo de dados com N construtores , , de tal forma que construtor tem aridade . ${\ displaystyle \ {c_ {i} \} _ {i = 1} ^ {N}}$${\ displaystyle c_ {i}}$ ${\ displaystyle A_ {i}}$

Codificação Scott

A codificação Scott do construtor do tipo de dados D é ${\ displaystyle c_ {i}}$

${\ displaystyle \ lambda x_ {1} \ ldots x_ {A_ {i}}. \ lambda c_ {1} \ ldots c_ {N} .c_ {i} \ x_ {1} \ ldots x_ {A_ {i}} }$

Codificação Mogensen-Scott

Mogensen estende a codificação Scott para codificar qualquer termo lambda não digitado como dados. Isso permite que um termo lambda a ser representada como dados, dentro de um cálculo Lambda programa de meta . A metafunção mse converte um termo lambda na representação de dados correspondente do termo lambda;

${\ displaystyle {\ begin {alinhado} \ operatorname {mse} [x] & = \ lambda a, b, ca \ x \\\ operatorname {mse} [M \ N] & = \ lambda a, b, cb \ \ operatorname {mse} [M] \ \ operatorname {mse} [N] \\\ operatorname {mse} [\ lambda xM] & = \ lambda a, b, cc \ (\ lambda x. \ operatorname {mse} [ M]) \\\ fim {alinhado}}}$

O "termo lambda" é representado como uma união marcada com três casos:

• Construtor a - uma variável ( aridade 1, não recursiva)
• Construtor b - aplicação de função (aridade 2, recursiva em ambos os argumentos),
• Construtor c - abstração lambda (aridade 1, recursiva).

Por exemplo,

${\ displaystyle {\ begin {array} {l} \ operatorname {mse} [\ lambda xf \ (x \ x)] \\\ lambda a, b, cc \ (\ lambda x. \ operatorname {mse} [f \ (x \ x)]) \\\ lambda a, b, cc \ (\ lambda x. \ lambda a, b, cb \ \ operatorname {mse} [f] \ \ operatorname {mse} [x \ x] ) \\\ lambda a, b, cc \ (\ lambda x. \ lambda a, b, cb \ (\ lambda a, b, ca \ f) \ \ operatorname {mse} [x \ x]) \\\ lambda a, b, cc \ (\ lambda x. \ lambda a, b, cb \ (\ lambda a, b, ca \ f) \ (\ lambda a, b, cb \ \ operatorname {mse} [x] \ \ operatorname {mse} [x])) \\\ lambda a, b, cc \ (\ lambda x. \ lambda a, b, cb \ (\ lambda a, b, ca \ f) \ (\ lambda a, b, cb \ (\ lambda a, b, ca \ x) \ (\ lambda a, b, ca \ x))) \ end {array}}}$

Comparação com a codificação da Igreja

A codificação Scott coincide com a codificação Church para booleanos. A codificação da igreja de pares pode ser generalizada para tipos de dados arbitrários pela codificação de D acima como ${\ displaystyle c_ {i}}$

${\ displaystyle \ lambda x_ {1} \ ldots x_ {A_ {i}}. \ lambda c_ {1} \ ldots c_ {N} .c_ {i} (x_ {1} c_ {1} \ ldots c_ {N }) \ ldots (x_ {A_ {i}} c_ {1} \ ldots c_ {N})}$

compare isso com a codificação Mogensen Scott,

${\ displaystyle \ lambda x_ {1} \ ldots x_ {A_ {i}}. \ lambda c_ {1} \ ldots c_ {N} .c_ {i} x_ {1} \ ldots x_ {A_ {i}}}$

Com essa generalização, as codificações de Scott e Church coincidem em todos os tipos de dados enumerados (como o tipo de dados booleano) porque cada construtor é uma constante (sem parâmetros).

Com relação à praticidade de usar a codificação Church ou Scott para programação, há uma compensação simétrica: os numerais codificados por Church suportam uma operação de adição de tempo constante e não têm nada melhor do que uma operação predecessora de tempo linear; Os numerais codificados por Scott suportam uma operação predecessora de tempo constante e não têm nada melhor do que uma operação de adição de tempo linear.

Definições de tipo

Dados codificados por igreja e operações neles podem ser tipificados no sistema F , mas dados e operações codificados por Scott não são obviamente tipáveis ​​no sistema F. Universal, bem como tipos recursivos parecem ser necessários. Como a normalização forte não é válida para tipos recursivos irrestritos, estabelecer o término de programas que manipulam dados codificados por Scott determinando a boa tipagem requer que o sistema de tipos forneça restrições adicionais sobre a formação de termos digitados recursivamente.

Veja também

• Codificação de igreja
• Sistema F
• Cubo lambda

Notas

Referências

• Stump, A. (2009). Meta-programação diretamente reflexiva . Higher-Order and Symbolic Computation, 22 , 115-144.
• Mogensen, T.Æ. (1992). Autointerpretações eficientes em cálculo lambda . J. Funct. Programa., 2 , 345-363.