Regras de tratamento de restrições - Constraint Handling Rules

Regras de tratamento de restrições (CHR)
Paradigmas	Lógica de restrição , declarativa
Projetado por	Thom Frühwirth
Apareceu pela primeira vez	1991 ; 30 anos atrás
Influenciado por
	Prolog

Regras de tratamento de restrições ( CHR ) é uma linguagem de programação declarativa baseada em regras , introduzida em 1991 por Thom Frühwirth na época com o Centro Europeu de Pesquisa da Indústria de Computadores (ECRC) em Munique, Alemanha. Originalmente planejado para programação de restrição , o CHR encontra aplicações em indução gramatical , sistemas de tipo , raciocínio abdutivo , sistemas multiagentes , processamento de linguagem natural , compilação , programação , raciocínio espaço-temporal , teste e verificação .

Um programa CHR, às vezes chamado de manipulador de restrição , é um conjunto de regras que mantém um armazenamento de restrição , um conjunto múltiplo de fórmulas lógicas. A execução de regras pode adicionar ou remover fórmulas da loja, alterando assim o estado do programa. A ordem em que as regras "disparam" em um determinado armazenamento de restrição é não determinística , de acordo com sua semântica abstrata e determinística (aplicação de regra de cima para baixo), de acordo com sua semântica refinada .

Embora o CHR seja Turing completo , ele não é comumente usado como uma linguagem de programação por si só. Em vez disso, é usado para estender uma linguagem host com restrições. Prolog é de longe a linguagem hospedeira mais popular e CHR está incluído em várias implementações de Prolog, incluindo SICStus e SWI-Prolog , embora implementações de CHR também existam para Haskell , Java , C , SQL e JavaScript. Em contraste com o Prolog, as regras CHR são multi-head e são executadas em uma maneira de escolha confirmada usando um algoritmo de encadeamento direto .

Visão geral da linguagem

A sintaxe concreta dos programas CHR depende da linguagem hospedeira e, de fato, os programas incorporam instruções na linguagem hospedeira que são executadas para lidar com algumas regras. A linguagem do host fornece uma estrutura de dados para representar os termos , incluindo variáveis lógicas . Os termos representam restrições, que podem ser consideradas "fatos" sobre o domínio do problema do programa. Tradicionalmente, Prolog é usado como a linguagem hospedeira, então suas estruturas de dados e variáveis são usadas. O restante desta seção usa uma notação matemática neutra que é comum na literatura CHR.

Um programa CHR, então, consiste em regras que manipulam um conjunto múltiplo desses termos, chamado de armazenamento de restrição . As regras vêm em três tipos:

As regras de simplificação têm a forma . Quando elas combinam com as cabeças e os guardas seguram, as regras de simplificação podem reescrever as cabeças no corpo . ${\ displaystyle h_ {1}, \ dots, h_ {n} \ Longleftrightarrow g_ {1}, \ dots, g_ {m} \, | \, b_ {1}, \ dots, b_ {o}}$ ${\ displaystyle h_ {1}, \ dots, h_ {n}}$ ${\ displaystyle g_ {1}, \ dots, g_ {m}}$ ${\ displaystyle b_ {1}, \ dots, b_ {o}}$
As regras de propagação têm o formulário . Essas regras adicionam as restrições do corpo à loja, sem remover as cabeças. ${\ displaystyle h_ {1}, \ dots, h_ {n} \ Longrightarrow g_ {1}, \ dots, g_ {m} \, | \, b_ {1}, \ dots, b_ {o}}$
As regras de simulação combinam simplificação e propagação. Eles estão escritos . Para uma regra de simpagação disparar, o armazenamento de restrição deve corresponder a todas as regras na cabeça e os guardas devem ser verdadeiros. As restrições antes do são mantidas, como em uma regra de propagação; as restrições restantes são removidas. ${\ displaystyle h_ {1}, \ dots, h _ {\ ell} \, \ barra invertida \, h _ {\ ell +1}, \ dots, h_ {n} \ Longleftrightarrow g_ {1}, \ dots, g_ {m } \, | \, b_ {1}, \ dots, b_ {o}}$ ${\ displaystyle \ ell}$ ${\ displaystyle \ barra invertida}$ ${\ displaystyle n- \ ell}$

Uma vez que as regras de simpagação incluem simplificação e propagação, todas as regras CHR seguem o formato

{\ displaystyle H_ {k} \, \ barra invertida \, H_ {r} \ Longleftrightarrow G \, | \, B}

onde cada um é uma conjunção de restrições: e contém restrições CHR, enquanto os guardas são integrados. Apenas um de precisa estar vazio. ${\ displaystyle H_ {k}, H_ {r}, G, B}$ ${\ displaystyle H_ {k}, H_ {r}}$ ${\ displaystyle B}$ ${\ displaystyle G}$ ${\ displaystyle H_ {k}, H_ {r}}$

A linguagem do host também deve definir restrições internas sobre os termos. As proteções nas regras são restrições integradas, portanto, executam com eficácia o código da linguagem do host. A teoria de restrição embutida deve incluir pelo menos true(a restrição que sempre é válida), fail(a restrição que nunca é válida e é usada para sinalizar falha) e igualdade de termos, ou seja, unificação . Quando a linguagem do host não oferece suporte a esses recursos, eles devem ser implementados junto com o CHR.

A execução de um programa CHR começa com um armazenamento de restrição inicial. O programa então prossegue combinando as regras com o armazenamento e aplicando-as, até que não haja mais correspondência de regras (sucesso) ou a failrestrição seja derivada. No primeiro caso, o armazenamento de restrições pode ser lido por um programa de linguagem host para procurar fatos de interesse. A correspondência é definida como "unificação unilateral": ela vincula variáveis apenas em um lado da equação. A correspondência de padrões pode ser facilmente implementada como unificação, quando a linguagem do host oferece suporte.

Programa de exemplo

O seguinte programa CHR, na sintaxe Prolog, contém quatro regras que implementam um solucionador para uma restrição de menor ou igual . As regras são rotuladas por conveniência (rótulos são opcionais no CHR).

 % X leq Y means variable X is less-or-equal to variable Y 
 reflexivity  @ X leq X <=> true.
 antisymmetry @ X leq Y, Y leq X <=> X = Y.
 transitivity @ X leq Y, Y leq Z ==> X leq Z.
 idempotence  @ X leq Y \ X leq Y <=> true.

As regras podem ser lidas de duas maneiras. Na leitura declarativa, três das regras especificam os axiomas de uma ordenação parcial :

Reflexividade: X ≤ X
Antissimetria: se X ≤ Y e Y ≤ X , então X = Y
Transitividade: se X ≤ Y e Y ≤ Z , então X ≤ Z

Todas as três regras são implicitamente quantificadas universalmente (identificadores em maiúsculas são variáveis na sintaxe Prolog). A regra da idempotência é uma tautologia do ponto de vista lógico, mas tem um propósito na segunda leitura do programa.

A segunda maneira de ler o acima é como um programa de computador para manter um armazenamento de restrições, uma coleção de fatos (restrições) sobre objetos. O armazenamento de restrição não faz parte deste programa, mas deve ser fornecido separadamente. As regras expressam as seguintes regras de computação:

A reflexividade é uma regra de simplificação : expressa que, se um fato da forma X ≤ X for encontrado na loja, ele pode ser removido.
A anti-simetria também é uma regra de simplificação, mas com duas cabeças . Se dois factos da forma X ≤ Y e Y ≤ X pode ser encontrado na loja (com correspondentes X e Y ), em seguida, eles podem ser substituídos com o único facto de X = Y . Tal restrição de igualdade é considerada embutida e implementada como uma unificação que normalmente é tratada pelo sistema Prolog subjacente.
A transitividade é uma regra de propagação . Ao contrário da simplificação, ele não remove nada do armazenamento de restrições; em vez disso, quando fatos da forma X ≤ Y e Y ≤ Z (com o mesmo valor para Y ) estão na loja, um terceiro fato X ≤ Z pode ser adicionado.
A idempotência, finalmente, é uma regra de simpagação , uma simplificação e propagação combinadas. Ao encontrar fatos duplicados, ele os remove da loja. Podem ocorrer duplicatas porque os armazenamentos de restrições são vários conjuntos de fatos.

Dada a consulta

A leq B, B leq C, C leq A

as seguintes transformações podem ocorrer:

Restrições atuais	Regra aplicável às restrições	Conclusão da aplicação da regra
`A leq B, B leq C, C leq A`	transitividade	`A leq C`
`A leq B, B leq C, C leq A, A leq C`	antissimetria	`A = C`
`A leq B, B leq A, A = C`	antissimetria	`A = B`
`A = B, A = C`	Nenhum

A regra de transitividade adiciona A leq C. Em seguida, ao aplicar a regra de antissimetria , A leq Ce C leq Asão removidos e substituídos por A = C. Agora, a regra de antissimetria se torna aplicável às duas primeiras restrições da consulta original. Agora todas as restrições CHR foram eliminadas, portanto nenhuma regra adicional pode ser aplicada e a resposta A = B, A = Cé retornada: CHR inferiu corretamente que todas as três variáveis devem se referir ao mesmo objeto.

Execução de programas CHR

Para decidir qual regra deve "disparar" em um determinado armazenamento de restrição, uma implementação de CHR deve usar algum algoritmo de correspondência de padrões . Os algoritmos candidatos incluem RETE e TREATS , mas a maioria das implementações usa um algoritmo lento chamado LEAPS .

A especificação original da semântica do CHR era inteiramente não determinística, mas a chamada "semântica de operação refinada" de Duck et al. removeu muito do não determinismo para que os criadores de aplicativos pudessem confiar na ordem de execução para desempenho e correção de seus programas.

A maioria das aplicações de CHRs requer que o processo de reescrita seja confluente ; caso contrário, os resultados da busca por uma atribuição satisfatória serão não determinísticos e imprevisíveis. O estabelecimento da confluência geralmente é feito por meio das três propriedades a seguir:

Um programa CHR é localmente confluente se todos os seus pares críticos forem juntáveis .
Um programa CHR é chamado de finalização se não houver cálculos infinitos.
Um programa CHR de encerramento é confluente se todos os seus pares críticos forem uníveis .

Veja também

Referências

Leitura adicional

Christiansen, Henning. " Gramáticas CHR ." Theory and Practice of Logic Programming 5.4-5 (2005): 467-501.

Languages

In other projects