Anti-unification (datavetenskap)

Anti-unification är processen att konstruera en generalisering som är gemensam för två givna symboliska uttryck. Liksom i unification urskiljs flera ramverk beroende på vilka uttryck (även kallade termer) som är tillåtna, och vilka uttryck som anses lika. Om variabler som representerar funktioner är tillåtna i ett uttryck kallas processen "högre ordningens anti-förening", annars "första ordningens anti-förening". Om generaliseringen krävs för att ha en instans som bokstavligen är lika med varje inmatningsuttryck, kallas processen "syntaktisk anti-förening", annars "E-anti-förening", eller "anti-förening modulo teori".

En anti-unifieringsalgoritm bör för givna uttryck beräkna en komplett och minimal generaliseringsuppsättning, det vill säga en uppsättning som täcker alla generaliseringar, och som inte innehåller några redundanta medlemmar. Beroende på ramverket kan en komplett och minimal generaliseringsuppsättning ha en, ändligt många, eller möjligen oändligt många medlemmar, eller kanske inte existera alls; den kan inte vara tom, eftersom en trivial generalisering finns i alla fall. För första ordningens syntaktiska anti-unifiering Gordon Plotkin en algoritm som beräknar en komplett och minimal singleton generaliseringsuppsättning innehållande den så kallade "minst allmänna generaliseringen" (lgg).

Anti-förening bör inte förväxlas med dis-unification . Det sistnämnda innebär processen att lösa inekvationssystem, det vill säga att hitta värden för variablerna så att alla givna inekvationer är uppfyllda. Denna uppgift är helt annorlunda än att hitta generaliseringar.

Förutsättningar

Formellt förutsätter ett anti-enhetsförhållningssätt

• En oändlig mängd V av variabler . För högre ordnings anti-unifiering är det bekvämt att välja V disjoint från uppsättningen av lambda-term bundna variabler .
• En uppsättning T av termer så att V ⊆ T . För första ordningens och högre ordningens anti-unifiering T vanligtvis uppsättningen av första ordningens termer (termer byggda från variabel- och funktionssymboler) respektive lambda -termer (termer som innehåller några högre ordningens variabler).
• En ekvivalensrelation $\equiv$ på $T$ , som indikerar vilka termer som anses lika. För högre ordnings anti-unifiering, vanligtvis $t\equiv u$ om $t$ och $u$ är alfaekvivalenta . För första ordningens E-anti-unification, $\equiv$ reflekterar bakgrundskunskapen om vissa funktionssymboler; till exempel, om $\oplus$ anses kommutativ, $t\equiv u$ om $u$ resulterar från $t$ genom att byta argumenten för $\oplus$ vid några (möjligen alla) förekomster. Om det inte finns någon bakgrundskunskap alls, så anses endast bokstavligen, eller syntaktiskt, identiska termer vara lika.

Första ordningens termin

Huvudartikel: Term (logik)

Givet en uppsättning $V$ av variabelsymboler, en uppsättning $C$ av konstantsymboler och uppsättningar $F_{n}$ av $n$ -ary funktionssymboler, även kallade operatorsymboler, för varje naturligt tal ${\displaystyle n\geq 1} ,$ är uppsättningen (osorterade första ordningens) termer $T$ rekursivt definierade som den minsta mängden med följande egenskaper:

• varje variabelsymbol är en term: V ⊆ T ,
• varje konstant symbol är en term: C ⊆ T ,
• från varje n termer t ₁ ,..., t _n , och varje n -är funktionssymbol f ∈ F _n , en större term $f(t_{1},\ ldots ,t_{n})$ kan byggas.

Till exempel, om x ∈ V är en variabel symbol, 1 ∈ C är en konstant symbol och add ∈ F ₂ är en binär funktionssymbol, då x ∈ T , 1 ∈ T , och (därav) add( x ,1) ∈ T av byggregeln för första, andra och tredje termen. Den senare termen skrivs vanligtvis som x +1, med hjälp av Infix-notation och den vanligare operatorsymbolen + för enkelhetens skull.

Term av högre ordning

Huvudartikel: Lambdakalkyl

Utbyte

Huvudartikel: Substitution (logik)

En substitution är en avbildning $\sigma :V\longrightarrow T$ från variabler till termer; beteckningen $\{x_{1}\mapsto t_{1},\ldots ,x_{k}\mapsto t_{k}\}$ avser till en substitution som mappar varje variabel $x_{i}$ till termen $t_{i}$ , för $i=1,\ldots ,k$ , och varje annan variabel för sig själv. Att tillämpa denna substitution på en term t skrivs i postfix-notation som $t\{x_{1}\mapsto t_{1},\ldots ,x_ {k}\mapsto t_{k}\}$ ; det betyder att (samtidigt) ersätta varje förekomst av varje variabel $x_{i}$ i termen t med $t_{i}$ . Resultatet tσ av att tillämpa en substitution σ på en term t kallas en instans av den termen t . Som ett första ordningens exempel, att tillämpa substitutionen $\{x\mapsto h(a,y),z\mapsto b\}$ på termen

f (	x	, a , g (	z	), y )	avkastning
f (	h ( a , y )	, a , g (	b	), y )	.

Generalisering, specialisering

Om en term $t$ har en instans som motsvarar en term ${\displaystyle u} ,$ det vill säga om $t\sigma \equiv u$ för någon ersättning $\sigma$ , då kallas $t$ mer generell än $u$ , och $u$ kallas mer speciell än, eller subsumeras av, $t$ . Till exempel $x\oplus a$ mer allmän än $a\oplus b$ om $\oplus$ är kommutativ , eftersom då $(x\oplus a)\{x\mapsto b\}=b\oplus a\equiv a\oplus b$ .

Om $\equiv$ är bokstavlig (syntaktisk) identitet för termer, kan en term vara både mer allmän och mer speciell än en annan endast om båda termerna skiljer sig bara i deras variabelnamn, inte i deras syntaktiska struktur; sådana termer kallas varianter eller byter namn på varandra. Till exempel $f(x_{1},a,g(z_{1}),y_{1})$ en variant av $f(x_{2},a,g(z_{2}),y_{2})$ , eftersom $f( x_{1},a,g(z_{1}),y_{1})\{x_{1}\mapsto x_{2},y_{1}\mapsto y_{2},z_{1}\mapsto z_{2}\}=f(x_{2},a,g(z_{2}),y_{2})$ och $f(x_{2},a,g(z_{2 }),y_{2})\{x_{2}\mapsto x_{1},y_{2}\mapsto y_{1},z_{2}\mapsto z_{1}\}=f(x_{1 },a,g(z_{1}),y_{1})$ . Men $f(x_{1},a,g(z_{1}),y_{1})$ är dock inte en variant av $f(x_{2},a,g(x_{2}),x_{2})$ eftersom ingen substitution kan transformera den senare termen till den förra, även om $\{x_{1}\mapsto x_{2},z_{1}\mapsto x_{2 },y_{1}\mapsto x_{2}\}$ uppnår den omvända riktningen. Den senare termen är därför mer speciell än den förra.

En substitution $\sigma$ är mer speciell än, eller subsumerad av, en substitution $\tau$ om $x\sigma$ är mer speciell än $x\tau$ för varje variabel $x$ . Till exempel $\{x\mapsto f(u),y\mapsto f(f(u))\}$ mer speciell än $\{x\mapsto z,y\mapsto f(z)\}$ , eftersom $f(u)$ och $f(f(u))$ är mer speciell än $z$ respektive $f(z)$ .

Antiföreningsproblem, generaliseringsuppsättning

Ett problem mot förening är ett par $\langle t_{1},t_{2}\rangle$ termer. En term $t$ är en vanlig generalisering , eller anti-unifier , av $t_{1}$ och $t_{2}$ om $t\sigma _{1}\equiv t_{1}$ och $t\sigma _{2}\equiv t_{2}$ för vissa substitutioner $\ sigma _{1},\sigma _{2}$ . För ett givet anti-unifieringsproblem kallas en uppsättning ${\displaystyle S} av anti-unifierare$ komplett om varje generalisering subsumerar någon term $t\in S$ ; uppsättningen $S$ kallas minimal om ingen av dess medlemmar subsumerar en annan.

Första ordningens syntaktiska anti-förening

Ramverket för första ordningens syntaktiska antiförening är baserat på att $T$ är uppsättningen av första ordningens termer (över en viss uppsättning $V$ av variabler, $C$ av konstanter och $F_{n}$ av $n$ -ary funktionssymboler) och på $\equiv$ är syntaktisk likhet . I detta ramverk har varje anti-unifieringsproblem $\langle t_{1},t_{2}\rangle$ en komplett och uppenbarligen minimal singellösningsuppsättning $\{t\}$ . Dess medlem $t$ kallas den minsta allmänna generaliseringen (lgg) av problemet, den har en instans syntaktiskt lika med $t_{1}$ och en annan syntaktisk lika med $t_ {2}$ . All vanlig generalisering av $t_{1}$ och $t_{2}$ subsumerar $t$ . Lgg är unik upp till varianter: om $S_{1}$ och $S_{2}$ är både kompletta och minimala lösningsuppsättningar av samma syntaktiska anti-unifieringsproblem, då är $S_{1}=\{s_{1}\}$ och $S_{2}=\{s_{2}\}$ för vissa termer $s_{1}$ och ${\displaystyle s_{2}} ,$ som byter namn på varandra.

Plotkin har gett en algoritm för att beräkna lgg för två givna termer. Det förutsätter en injektiv mappning ${\displaystyle \phi :T\times T\longrightarrow V} ,$ det vill säga en mappning som tilldelar varje par $s,t$ av termer en egen variabel $\phi (s,t)$ , så att inga två par delar samma variabel. Algoritmen består av två regler:

$f(s_{1},\dots ,s_{n})\sqcup f(t_{1},\ldots ,t_{n})$	$\rightsquigarrow$	$f(s_{1}\sqcup t_{1},\ldots ,s_{n}\sqcup t_{n})$
$s\sqcup t$	$\rightsquigarrow$	$\phi (s,t)$	om tidigare regel inte är tillämplig

Till exempel, $(0*0)\displaystyle (0*0) *4)\rightsquigarrow (0\sqcup 4)*(0\sqcup 4)\rightsquigarrow \phi (0,4)*\phi (0,4)\rightsquigarrow x*x$ ; denna minst allmänna generalisering återspeglar den gemensamma egenskapen för båda inmatningarna att vara kvadrattal.

Plotkin använde sin algoritm för att beräkna den " relativa minsta allmänna generaliseringen (rlgg) " av två klausuluppsättningar i första ordningens logik, vilket var grunden för Golem - metoden för induktiv logikprogrammering .

Första ordningens anti-unification modulo teori

• Jacobsen, Erik (juni 1991), Unification and Anti-unification (PDF) , Teknisk rapport
• Østvold, Bjarte M. (apr 2004), A Functional Reconstruction of Anti-Unification (PDF) , NR Note, vol. DART/04/04, Norwegian Computing Center
• Boytcheva, Svetla; Markov, Zdravko (2002). "En algoritm för att inducera minsta generalisering under relativ implikation" ( PDF) . {{ citera journal }} : Citera journal kräver |journal= ( hjälp )
• Kutsia, Temur; Levy, Jordi; Villaret, Mateu (2014). "Anti-unifiering för orankade villkor och säkringar" (PDF) . Journal of Automated Reasoning . 52 (2): 155–190. doi : 10.1007/s10817-013-9285-6 . Programvara.

Ekvationsteorier

• En associativ och kommutativ operation: Pottier, Loic (feb 1989), Algorithms des completion et generalization en logic du premier order (These de doctorat) ; Pottier, Loic (1989), Generalization de termes en theorie equationelle – Cas associatif-commutatif , INRIA Report, vol. 1056, INRIA
• Kommutativa teorier: Baader, Franz (1991). "Enande, svagt enande, övre gräns, nedre gräns och generaliseringsproblem" . Proc. 4:e konf. om Rewriting Techniques and Applications (RTA) . LNCS. Vol. 488. Springer. s. 86–91. doi : 10.1007/3-540-53904-2_88 .
• Fria monoider: Biere, A. (1993), Normalisierung, Unifikation und Antiunifikation in Freien Monoiden (PDF) , Univ. Karlsruhe, Tyskland
• Reguljära kongruensklasser:   Heinz, Birgit (dec 1995), Anti-Unifikation modulo Gleichungstheorie und deren Anwendung zur Lemmagenerierung , GMD Berichte, vol. 261, TU Berlin, ISBN 978-3-486-23873-0 ;   Burghardt, Jochen (2005). "E-generalisering med hjälp av grammatik". Artificiell intelligens . 165 (1): 1–35. arXiv : 1403.8118 . doi : 10.1016/j.artint.2005.01.008 . S2CID 5328240 .
• A-, C-, AC-, ACU-teorier med ordnade sorter: Alpuente, Maria; Escobar, Santiago; Espert, Javier; Meseguer, Jose (2014). "En modulär ordningssorterad ekvationell generaliseringsalgoritm" (PDF) . Information och beräkning . 235 : 98–136. doi : 10.1016/j.ic.2014.01.006 . hdl : 2142/25871 .
• Rent idempotenta teorier:   Cerna, David; Kutsia, Temur (2020). "Idempotent anti-Enande" . ACM-transaktioner på beräkningslogik . 21 (2): 1–32. doi : 10.1145/3359060 . hdl : 10.1145/3359060 . S2CID 207861304 .

Första ordningens sorterad antiförening

• Taxonomiska sorter: Frisch, Alan M.; Page, David (1990). "Generalisering med taxonomisk information". AAAI : 755–761. ; Frisch, Alan M.; Page Jr., C. David (1991). "Generalisera atomer i begränsningslogik" . Proc. Konf. om Kunskapsrepresentation . ;   Frisch, AM; Sida, CD (1995). "Bygga teorier till instansiering". I Mellish, CS (red.). Proc. 14:e IJCAI . Morgan Kaufmann. s. 1210–1216. CiteSeerX 10.1.1.32.1610 .
• Feature termer:   Plaza, E. (1995). "Cases as Terms: A Feature Term Approach to the Structured Representation of Cases". Proc. Första internationella konferensen om fallbaserade resonemang (ICCBR) . LNCS. Vol. 1010. Springer. s. 265–276. ISSN 0302-9743 .
• Idestam-Almquist, Peter (juni 1993). "Generalisering under implikation genom rekursiv anti-förening" . Proc. 10:e konf. om maskininlärning . Morgan Kaufmann. s. 151–158.
• Fischer, Cornelia (maj 1994), PAntUDE – An Anti-Uniification Algorithm for Expressing Refined Generalizations (PDF) , Research Report, vol. TM-94-04, DFKI
• A-, C-, AC-, ACU-teorier med ordnade sorteringar: se ovan

Nominell anti-förening

• Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu (juni 2013). Nominell Anti-Enande . Proc. RTA 2015. Vol. 36 av LIPIcs. Schloss Dagstuhl, 57-73. Programvara.

Ansökningar

• Programanalys: Bulychev, Peter; Minea, Marius (2008). "Duplicerad koddetektering med anti-unifiering" . Proceedings of the Spring/Summer Young Researchers Colloquium on Software Engineering (2). ; Bulychev, Peter E.; Kostylev, Egor V.; Zakharov, Vladimir A. (2009). "Anti-Uniification Algorithms and their Applications in Program Analysis". {{ citera journal }} : Citera journal kräver |journal= ( hjälp )
• Kodfaktorering: Cottrell, Rylan (sep 2008), Halvautomatisk återanvändning av småskalig källkod via strukturell korrespondens (PDF) , Univ. Calgary
• Induktionsbevisande: Heinz, Birgit (1994), Lemma Discovery by Anti-Unification of Regular Sorts , Technical Report, vol. 94–21, TU Berlin
• Informationsutvinning: Thomas, Bernd (1999). "Anti-Enhetsbaserad inlärning av T-Wrappers för informationsextraktion" ( PDF) . AAAI teknisk rapport . WS-99-11: 15–20.
• Fallbaserat resonemang: Armengol, Eva; Plaza, Enric (2005). "Använda symboliska beskrivningar för att förklara likheter på CBR" . {{ citera journal }} : Citera journal kräver |journal= ( hjälp )
• Programsyntes: Idén att generalisera termer med avseende på en ekvationsteori kan spåras tillbaka till Manna och Waldinger (1978, 1980) som ville tillämpa den i programsyntes. I avsnittet "Generalisering" föreslår de (på s. 119 i artikeln från 1980) att generalisera reverse ( l ) och reverse ( tail ( l ))<>[ huvud ( l )] för att erhålla reverse(l')<>m ' . Denna generalisering är endast möjlig om bakgrundsekvationen u <>[]= u beaktas.

Zohar Manna ; Richard Waldinger (dec 1978). En deduktiv metod för programsyntes (PDF) (teknisk anmärkning). SRI International . — förtryck av 1980 års artikel

  Zohar Manna och Richard Waldinger (januari 1980). "Ett deduktivt tillvägagångssätt för programsyntes". ACM-transaktioner på programmeringsspråk och system . 2 : 90–121. doi : 10.1145/357084.357090 . S2CID 14770735 .

• Naturlig språkbehandling:   Amiridze, Nino; Kutsia, Temur (2018). "Anti-unifiering och naturlig språkbehandling" . Femte workshop om naturligt språk och datavetenskap, NLCS'18 . EasyChair Preprints. EasyChair Rapport nr 203. doi : 10.29007/fkrh . S2CID 49322739 .

Högre ordning mot enande

• Konstruktionskalkyl: Pfenning, Frank (jul 1991). "Enande och anti-Enande i konstruktionskalkylen" ( PDF) . Proc. 6:e LICS . Springer. s. 74–85.
• Enkelt skriven lambda-kalkyl (Input: Termer i den eta-långa beta-normala formen. Utdata: mönster av högre ordning): Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu (juni 2013). En variant av högre ordnings anti-unifiering . Proc. RTA 2013. Vol. 21 av LIPIcs. Schloss Dagstuhl, 113-127. Programvara.
• Enkelt typad lambdakalkyl (Input: Termer i den eta-långa beta-normala formen. Utdata: Olika fragment av den enkelt maskinskrivna lambdakalkylen inklusive mönster): Cerna, David; Kutsia, Temur (juni 2019). "A Generic Framework for Higher Order Generalizations" (PDF) . 4:e internationella konferensen om formella strukturer för beräkning och avdrag, FSCD, 24–30 juni 2019, Dortmund, Tyskland . Schloss Dagstuhl - Leibniz-Zentrum für Informatik. s. 74–85.
• Restricted Higher Order Substitutions: Wagner, Ulrich (apr 2002), Combinatorically Restricted Higher Order Anti-Unification , TU Berlin ;   Schmidt, Martin (sep 2010), Restricted Higher-Order Anti-Uniification for Heuristic-Driven Theory Projection ( PDF) , PICS-Report, vol. 31–2010, Univ. Osnabrück, Tyskland, ISSN 1610-5389