Birleştirme (bilgisayar bilimi) - Unification (computer science)

Gelen mantık ve bilgisayar bilimleri , birleşme algoritmik bir süreçtir denklemleri çözme sembolik arasındaki ifadeler .

Bir denklem setinde ( birleştirme problemi de denir) hangi ifadelerin ( terimler olarak da adlandırılır ) olmasına izin verildiğine ve hangi ifadelerin eşit olarak kabul edildiğine bağlı olarak, birkaç birleştirme çerçevesi ayırt edilir. Bir ifadede yüksek dereceli değişkenlere, yani işlevleri temsil eden değişkenlere izin verilirse, sürece yüksek dereceli birleştirme , aksi takdirde birinci derece birleştirme denir . Her denklemin her iki tarafını tam anlamıyla eşit yapmak için bir çözüm gerekiyorsa, sürece sözdizimsel veya serbest birleştirme denir , aksi takdirde anlamsal veya denklemsel birleştirme veya E-birleştirme denir.veya birleştirme modulo teorisi .

Bir birleştirme probleminin çözümü , ikame olarak belirtilir , yani problemin ifadelerinin her bir değişkenine sembolik bir değer atanan bir eşleme. Bir birleştirme algoritması, belirli bir problem için eksiksiz ve minimum ikame kümesi, yani tüm çözümlerini kapsayan ve fazla üye içermeyen bir küme hesaplamalıdır . Çerçeveye bağlı olarak, tam ve minimal bir ikame kümesi en fazla bir, en fazla sonlu sayıda veya muhtemelen sonsuz sayıda üyeye sahip olabilir veya hiç var olmayabilir. Bazı çerçevelerde herhangi bir çözümün var olup olmadığına karar vermek genellikle imkansızdır. Birinci mertebeden sözdizimsel birleşim için, Martelli ve Montanari, çözülemezliği bildiren veya en genel birleştirici olarak adlandırılanı içeren eksiksiz ve minimum bir tekil ikame kümesini hesaplayan bir algoritma verdiler .

Örneğin, x , y , z değişkenleri olarak kullanıldığında, { cons ( x , cons ( x , nil )) = cons (2, y ) } singleton denklem seti , { x ikamesine sahip sözdizimsel birinci dereceden bir birleştirme problemidir. ↦ 2, y ↦ eksileri (2, nil ) } tek çözüm olarak. Sözdizimsel birinci dereceden birleştirme probleminin { y = eksiler (2, y ) } sonlu terimler kümesi üzerinde çözümü yoktur ; ancak sonsuz ağaç kümesi üzerinde { y ↦ eksileri (2, eksileri (2, eksileri (2,...))) } tek çözümü vardır . Semantik birinci dereceden birleşme sorunu { bir ⋅ x = x ⋅ bir } formun her ikamesine sahiptir { x ↦ bir ⋅ ... ⋅ bir } a içinde bir çözelti olarak yarıgrubu yani eğer (⋅) olarak kabul edilir birleştirici ; Aynı problem, (⋅)'nin de değişmeli olarak kabul edildiği bir değişmeli grupta bakıldığında, çözüm olarak herhangi bir ikamesi vardır. { a = y ( x ) } singleton kümesi , y bir fonksiyon değişkeni olduğundan , sözdizimsel ikinci dereceden bir birleştirme problemidir . Çözümlerden biri { x ↦ a , y ↦ ( kimlik fonksiyonu ) }; diğeri ise { y ↦ ( her değeri a ile eşleyen sabit fonksiyon ), x ↦ (herhangi bir değer) }'dir.

Bir birleştirme algoritması ilk olarak Jacques Herbrand tarafından keşfedildi , ilk resmi araştırma ise birinci dereceden sözdizimsel birleştirmeyi birinci dereceden mantık için çözümleme prosedürünün temel bir yapı taşı olarak kullanan John Alan Robinson'a atfedilebilir . bir kombinatoryal patlama kaynağını ortadan kaldırdığı için otomatik akıl yürütme teknolojisi: terimlerin somutlaştırılmasını aramak. Günümüzde otomatik akıl yürütme, birleştirmenin ana uygulama alanı olmaya devam etmektedir. Sözdizimsel birinci dereceden birleştirme, mantık programlama ve programlama dili tipi sistem uygulamasında, özellikle Hindley-Milner tabanlı tür çıkarım algoritmalarında kullanılır. Semantik birleştirme, SMT çözücülerde , terim yeniden yazma algoritmalarında ve kriptografik protokol analizinde kullanılır. Yüksek mertebeden birleştirme, örneğin Isabelle ve Twelf gibi ispat yardımcılarında kullanılır ve yüksek mertebeden örüntüler ifade edici olduğundan , lambdaProlog gibi bazı programlama dili uygulamalarında yüksek mertebeden birleştirmenin kısıtlı biçimleri ( yüksek mertebeden örüntü birleştirme ) kullanılır. , yine de ilgili birleştirme prosedürü, birinci dereceden birleştirmeye daha yakın teorik özellikleri korur.

Ortak resmi tanımlar

Önkoşullar

Resmi olarak, bir birleştirme yaklaşımı,

• Sonsuz seti ait değişkenler . Daha yüksek dereceli birleştirme için, lambda terimine bağlı değişkenler kümesinden ayrık olanı seçmek uygundur .${\görüntüleme stili V}$${\görüntüleme stili V}$
• Bir dizi ait açısından öyle ki . Birinci dereceden birleştirme ve yüksek dereceden birleştirme için, genellikle birinci dereceden terimler (değişken ve fonksiyon sembollerinden oluşturulan terimler ) ve lambda terimleri (bazı yüksek dereceli değişkenleri içeren terimler ) kümesidir .${\görüntüleme stili T}$${\ Displaystyle V\subseteq T}$${\görüntüleme stili T}$
• Bir eşleme değişkendir : her terime içinde meydana gelen serbest değişkenler kümesini atar .${\görüntüleme stili T\sağ ok }$ ${\displaystyle \mathbb {P} }$${\görüntüleme stili (V)}$${\görüntüleme stili t}$${\displaystyle {\text{vars}}(t)\subsetneq V}$${\görüntüleme stili t}$
• Bir eşdeğerlik ilişkisi ile ilgili şartlar eşit olarak kabul edilir, işaret etmektedir. Daha yüksek dereceli birleştirme için, genellikle if ve are alfa eşdeğeri . Birinci dereceden E-birleştirme için, belirli fonksiyon sembolleri hakkında arka plan bilgisini yansıtır; örneğin, değişmeli olarak kabul edilirse , bazı (muhtemelen tüm) olayların argümanlarının değiştirilmesinden kaynaklanırsa . Hiç arka plan bilgisi yoksa, o zaman sadece kelimenin tam anlamıyla veya sözdizimsel olarak aynı terimler eşit kabul edilir; bu durumda, ≡, serbest teori (çünkü bu serbest bir nesnedir ), boş teori (çünkü denklem cümleleri kümesi veya arka plan bilgisi boştur), yorumlanmamış fonksiyonlar teorisi (çünkü birleştirme yorumlanmamış terimler ) veya yapıcılar teorisi (çünkü tüm işlev sembolleri, üzerinde çalışmak yerine yalnızca veri terimleri oluşturur).${\görüntüleme stili \eşdeğer }$${\görüntüleme stili T}$${\görüntüleme stili t\eşdeğer u}$${\görüntüleme stili t}$${\görüntüleme stili u}$${\görüntüleme stili \eşdeğer }$${\görüntüleme stili\oplus }$${\görüntüleme stili t\eşdeğer u}$${\görüntüleme stili u}$${\görüntüleme stili t}$${\görüntüleme stili\oplus }$

Birinci dereceden terim

Verilen bir dizi bir dizi değişken sembollerin, sabit semboller ve setleri arasında , n her bir doğal sayı -ary fonksiyon sembolleri olarak da adlandırılan operatör semboller, (ayrıştırılmamış birinci dereceden) terimler grubu olduğu ardışık tanımlandığı ile en az grubu olduğu aşağıdaki özellikler: ${\görüntüleme stili V}$${\görüntüleme stili C}$${\displaystyle F_{n}}$${\displaystyle n\geq 1}$${\görüntüleme stili T}$

• her değişken sembolü bir terimdir: ,${\ Displaystyle V\subseteq T}$
• her sabit sembol bir terimdir: ,${\ Displaystyle C\subseteq T}$
• her n terimden ve her n -ary işlev sembolünden daha büyük bir terim oluşturulabilir.${\görüntüleme stili t_{1},...t_{n}}$${\displaystyle f\in F_{n}}$${\displaystyle f(t_{1},...,t_{n})}$

Örneğin, if bir değişken sembolüdür, sabit bir semboldür ve bir ikili fonksiyon sembolüdür , sırasıyla birinci, ikinci ve üçüncü terim oluşturma kuralına göre sırasıyla , ve (dolayısıyla) . İkinci terim genellikle , kolaylık sağlamak için ek notasyonu ve daha yaygın operatör sembolü + kullanılarak olarak yazılır . ${\displaystyle x\in V}$${\ Displaystyle 1\C'de}$${\displaystyle {\metin{ekle}}\F_{2}}$${\displaystyle x\T'de,1\T'de}$${\displaystyle {\metin{ekle}}(x,1)\T} içinde$${\ Displaystyle x+1}$

Daha yüksek dereceli terim

ikame

Bir ikame , değişkenlerden terimlere bir eşlemedir ; gösterim , her değişkeni , for terimiyle ve diğer tüm değişkenleri de kendisine eşleyen bir ikameyi ifade eder . Uygulanması bir dönem için bu ikame yazılır sonek gösterimde olarak ; Bu (aynı anda) her bir değişkenin, her geçtiği yerde değiştirmek anlamına gelir vadede göre . Bir terime bir ikame uygulanmasının sonucuna o terimin bir örneği denir . Birinci dereceden bir örnek olarak, terime { x ↦ h ( a , y ), z ↦ b } ikamesinin uygulanması${\displaystyle \sigma :V\rightarrow T}$${\displaystyle \{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}}$${\displaystyle x_{i}}$${\görüntüleme stili t_{i}}$${\görüntüleme stili i=1,...,k}$${\görüntüleme stili t}$${\displaystyle t\{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}}$${\displaystyle x_{i}}$${\görüntüleme stili t}$${\görüntüleme stili t_{i}}$${\görüntüleme stili t\tau }$${\görüntüleme stili\tau }$${\görüntüleme stili t}$${\görüntüleme stili t}$

	${\görüntüleme stili f(}$	${\displaystyle {\textbf {x}}}$	${\görüntüleme stili ,a,g(}$	${\displaystyle {\textbf {z}}}$	${\görüntüleme stili),y)}$
verim
	${\görüntüleme stili f(}$	${\displaystyle {\textbf {h}}({\textbf {a}},{\textbf {y}})}$	${\görüntüleme stili ,a,g(}$	${\displaystyle {\textbf {b}}}$	${\görüntüleme stili),y).}$

Genelleme, uzmanlaşma

Bir terim Eğer bir dönem için bir örnek eşdeğer olan ise, olduğu, bir ikame için , daha sonra adı daha genel fazla ve denir daha özel fazla ya da sınıflandırılır ile . Örneğin , o zamandan beri ⊕ değişmeli ise daha geneldir . ${\görüntüleme stili t}$${\görüntüleme stili u}$${\displaystyle t\sigma \eşdeğer u}$${\görüntüleme stili \sigma }$${\görüntüleme stili t}$${\görüntüleme stili u}$${\görüntüleme stili u}$${\görüntüleme stili t}$${\displaystyle x\oplus a}$${\ Displaystyle a\oplus b}$${\displaystyle (x\oplus a)\{x\mapsto b\}=b\oplus a\equiv a\oplus b}$

Eğer ≡ terimlerin değişmez (sözdizimsel) özdeşliğiyse, bir terim diğerinden hem daha genel hem de daha özel olabilir, ancak her iki terim de sözdizimsel yapılarında değil de yalnızca değişken adlarında farklılık gösteriyorsa; bu tür terimlere değişkenler veya birbirlerinin yeniden adlandırmaları denir . Örneğin , bir varyantıdır , çünkü ${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$${\displaystyle f(x_{2},a,g(z_{2}),y_{2})}$

ve

Bununla birlikte, ' nin bir varyantı değildir , çünkü hiçbir ikame ikinci terimi birincisine dönüştüremez. Bu nedenle ikinci terim, öncekinden daha özeldir. ${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$${\displaystyle f(x_{2},a,g(x_{2}),x_{2})}$

Keyfi için , bir terim yapısal olarak farklı bir terimden hem daha genel hem de daha özel olabilir. Örneğin, ffi halinde olan İdempotent zaman eğer varsa, daha sonra terimi daha genel rağmen, ve bunun, tam tersi ve farklı bir yapıya sahiptirler. ${\görüntüleme stili \eşdeğer }$${\displaystyle x\oplus x\eşdeğer x}$${\displaystyle x\oplus y}$${\görüntüleme stili z}$${\displaystyle x\oplus y}$${\görüntüleme stili z}$

Bir ikame , her terim için olduğundan daha özel ise , bir ikameden daha özeldir veya ikame tarafından kapsanır . Bunun daha genel olduğunu da söylüyoruz . Örneğin , 'den daha özeldir , ancak ' den daha özel olmadığı için değildir . ${\görüntüleme stili \sigma }$${\görüntüleme stili\tau }$${\görüntüleme stili t\sigma }$${\görüntüleme stili t\tau }$${\görüntüleme stili t}$${\görüntüleme stili\tau }$${\görüntüleme stili \sigma }$${\displaystyle \{x\mapsto a,y\mapsto a\}}$${\displaystyle \tau =\{x\mapsto y\}}$${\displaystyle \sigma =\{x\mapsto a\}}$${\görüntüleme stili f(x,y)\sigma =f(a,y)}$${\görüntüleme stili f(x,y)\tau =f(y,y)}$

Birleştirme sorunu, çözüm kümesi

Bir birleştirme problemi , potansiyel denklemlerin { l ₁ ≐ r ₁ , ..., l _n ≐ r _n } sonlu kümesidir , burada l _i , r _i ∈ T . Bir ikame σ a, çözelti bu sorun, eğer L _i σ ≡ r _i σ için . Böyle bir ikame aynı zamanda birleştirme probleminin birleştiricisi olarak da adlandırılır . Örneğin, ⊕ ise birleştirici , birleşme sorun { x ⊕ bir ≐ bir ⊕ x } çözümler {sahip X ↦ bir }, { x ↦ bir ⊕ bir }, { x ↦ bir ⊕ bir ⊕ bir } vs. { x ⊕ a ≐ a } probleminin çözümü yoktur. ${\görüntüleme stili i=1,...,n}$

Belirli bir birleştirme problemi için, eğer her bir çözüm ikamesi bir ikame σ ∈ S ile toplanıyorsa , bir S birleştiriciler kümesi tam olarak adlandırılır ; Üyelerinden hiçbiri bir diğerini içermiyorsa, S kümesine minimal denir .

Birinci dereceden terimlerin sözdizimsel birleşimi

Bir σ ikamesi ile t ₁ ve t ₂ terimlerini sözdizimsel olarak birleştiren şematik üçgen diyagramı

Birinci dereceden terimlerin sözdizimsel birleşimi , en yaygın kullanılan birleştirme çerçevesidir. Bu dayanmaktadır T grubu olan birinci sıra açısından (bazı belirli bir resim üzerinde V değişkenler, Cı- sabitler ve F _N arasında N -ary fonksiyonu semboller) ve ilgili ≡ olmak sözdizimsel eşitlik . Bu çerçevede, çözülebilir her bir birleştirme problemi { l ₁ ≐ r ₁ , ..., l _n ≐ r _n } , eksiksiz ve açıkça minimal, tekil bir çözüm kümesine sahiptir { σ } . Üyesi σ , problemin en genel birleştiricisi ( mgu ) olarak adlandırılır . Her potansiyel denklemin sol ve sağ tarafındaki terimler, mgu uygulandığında sözdizimsel olarak eşit hale gelir, yani l ₁ σ = r ₁ σ ∧ ... ∧ l _n σ = r _n σ . Problemin herhangi bir birleştiricisi mgu σ tarafından kapsanır . Mgu, varyantlara kadar benzersizdir: S ₁ ve S ₂ , aynı sözdizimsel birleştirme probleminin hem tam hem de minimum çözüm kümeleriyse, o zaman bazı ikameler için S ₁ = { σ ₁ } ve S ₂ = { σ ₂ } σ ₁ ve σ ₂ , ve xσ ₁ bir varyantı xσ ₂ , her bir değişken için x sorun meydana gelen.

Örneğin, { x ≐ z , y ≐ f ( x ) } birleştirme problemi { x ↦ z , y ↦ f ( z ) } bir birleştiriciye sahiptir , çünkü

x	{ x ↦ z , y ↦ f ( z ) }	=	z	=	z	{ x ↦ z , y ↦ f ( z ) }	, ve
y	{ x ↦ z , y ↦ f ( z ) }	=	f ( z )	=	f ( x )	{ x ↦ z , y ↦ f ( z ) }	.

Bu aynı zamanda en genel birleştiricidir. Aynı problem için diğer birleştiriciler örneğin { x ↦ f ( x ₁ ), y ↦ f ( f ( x ₁ )), z ↦ f ( x ₁ ) }, { x ↦ f ( f ( x ₁ )), y ↦ f ( f ( f ( x ₁ ))), z ↦ f ( f ( x ₁ )) } ve benzeri; sonsuz sayıda benzer birleştirici vardır.

Başka bir örnek olarak, g ( x , x ) ≐ f ( y ) probleminin , ≡ değişmez özdeşlik olması bakımından hiçbir çözümü yoktur, çünkü sol ve sağ tarafa uygulanan herhangi bir ikame , sırasıyla en dıştaki g ve f'yi tutacaktır ve farklı en dıştaki işlev sembollerine sahip terimler sözdizimsel olarak farklıdır.

Bir birleştirme algoritması

Robinson (1965) tarafından verilen ilk algoritma oldukça verimsizdi; bkz. kutu. Aşağıdaki daha hızlı algoritma Martelli, Montanari'den (1982) kaynaklanmıştır. Bu makale ayrıca verimli bir sözdizimsel birleştirme algoritması bulmaya yönelik önceki girişimleri listeler ve doğrusal zaman algoritmalarının Martelli, Montanari (1976) ve Paterson, Wegman (1978) tarafından bağımsız olarak keşfedildiğini belirtir.

Sonlu bir potansiyel denklemler kümesi verildiğinde , algoritma onu { x ₁ ≐ u ₁ , ..., x _m ≐ u _m } biçimindeki eşdeğer bir denklemler kümesine dönüştürmek için kurallar uygular ; burada x ₁ , ..., x _m, farklı değişkenler ve u ₁ , ..., u _m hiçbirini ihtiva eden terimler x _i . Bu formun bir seti ikame olarak okunabilir. Çözüm yoksa algoritma ⊥ ile sonlanır; diğer yazarlar bu durumda "Ω", "{}" veya " fail " kullanır. Değişken tüm oluşumlarını ikame işlemi x sorun, G terimi ile t ifade edilir G { x ↦ t }. Basitlik için, sabit semboller, sıfır argümana sahip fonksiyon sembolleri olarak kabul edilir. ${\displaystyle G=\{s_{1}\doteq t_{1},...,s_{n}\doteq t_{n}\}}$

${\displaystyle G\cup \{t\doteq t\}}$	${\ Displaystyle \ Sağ Ok }$	${\görüntüleme stili G}$		silmek
${\displaystyle G\cup \{f(s_{0},...,s_{k})\doteq f(t_{0},...,t_{k})\}}$	${\ Displaystyle \ Sağ Ok }$	${\displaystyle G\cup \{s_{0}\doteq t_{0},...,s_{k}\doteq t_{k}\}}$		ayrıştırmak
${\displaystyle G\cup \{f(s_{0},\ldots ,s_{k})\doteq g(t_{0},...,t_{m})\}}$	${\ Displaystyle \ Sağ Ok }$	${\görüntüleme stili\bot }$	eğer veya${\ Displaystyle f\neq g}$${\görüntüleme stili k\neq m}$	çatışma
${\displaystyle G\cup \{f(s_{0},...,s_{k})\doteq x\}}$	${\ Displaystyle \ Sağ Ok }$	${\displaystyle G\cup \{x\doteq f(s_{0},...,s_{k})\}}$		takas
${\displaystyle G\cup \{x\doteq t\}}$	${\ Displaystyle \ Sağ Ok }$	${\displaystyle G\{x\mapsto t\}\cup \{x\doteq t\}}$	eğer ve${\displaystyle x\değil {\metin{vars}}(t)}$${\displaystyle x\in {\metin{vars}}(G)}$	bertaraf etmek
${\displaystyle G\cup \{x\doteq f(s_{0},...,s_{k})\}}$	${\ Displaystyle \ Sağ Ok }$	${\görüntüleme stili\bot }$	Eğer ${\displaystyle x\in {\text{vars}}(f(s_{0},...,s_{k}))}$	Kontrol

Kontrol gerçekleşir

Değişken birleştirme çalışmaları x terimi içeren x katı subterm olarak X ≐ f (..., x , ...) için çözüm olarak sonsuz bir dönem yol açacak x , çünkü x kendisinin bir subterm olarak ortaya çıkabilecek . Yukarıda tanımlandığı gibi (sonlu) birinci mertebeden terimler kümesinde , x ≐ f (..., x , ...) denkleminin çözümü yoktur; bu nedenle eleme kuralı yalnızca x ∉ değişkense ( t ) uygulanabilir. Oluşan kontrol denilen bu ek denetim algoritmayı yavaşlattığından, örneğin çoğu Prolog sisteminde atlanır. Teorik bir bakış açısından, kontrol miktarlarını atlamak sonsuz ağaçlar üzerinde denklemleri çözmek anlamına gelir, aşağıya bakınız .

Fesih kanıtı

Algoritmanın sonlandırıldığının kanıtı için bir üçlü düşünün; burada n _var denklem setinde birden fazla meydana gelen değişkenlerin sayısıdır, n _lhs potansiyel denklemlerin sol tarafındaki fonksiyon sembollerinin ve sabitlerin sayısıdır ve n _{eqn denklem} sayısıdır. Zaman kural ortadan tatbik edilir , n _var itibaren azalır, X elimine edilir G ve sadece muhafaza { x ≐ t }. Başka bir kural uygulamak, n _{var'ı bir} daha asla artıramaz . Kural ayrıştırma , çakışma veya takas uygulandığında, en azından sol tarafın en dıştaki f kaybolduğu için n _lhs azalır . Kalan silme veya denetleme kurallarından herhangi birinin uygulanması , n _lhs'yi artıramaz , ancak n _eqn'yi azaltır . Bu nedenle, herhangi bir kural uygulaması , sözlük düzenine göre üçlüyü azaltır , bu yalnızca sınırlı sayıda mümkündür. ${\displaystyle \langle n_{var},n_{lhs},n_{eqn}\rangle }$${\displaystyle \langle n_{var},n_{lhs},n_{eqn}\rangle }$

Conor McBride "birleşme sömüren yapıyı ifade ederek" Bir de gözlemlemektedir bağımlı yazılan gibi dilin nükte , Robinson 'ın algoritması yapılabilir değişkenlerin sayısı özyinelemeli ayrı sonlandırma kanıtı gereksiz hale durumda.

Birinci dereceden terimlerin sözdizimsel birleşim örnekleri

Prolog sözdizimsel kuralında, büyük harfle başlayan bir sembol, bir değişken adıdır; küçük harfle başlayan bir sembol, bir fonksiyon sembolüdür; virgül mantıksal ve operatör olarak kullanılır . Matematiksel gösterim için x,y,z değişkenler, f,g fonksiyon sembolleri ve a,b sabitler olarak kullanılır.

giriş gösterimi	matematiksel gösterim	birleştirici ikame	Açıklama
a = a	{ bir = bir }	{}	Başarılı. ( totoloji )
a = b	{ bir = b }	⊥	a ve b eşleşmiyor
X = X	{ x = x }	{}	Başarılı. ( totoloji )
a = X	{ bir = x }	{ x ↦ bir }	x , a sabiti ile birleştirilir
X = Y	{ x = y }	{ x ↦ y }	x ve y takma addır
f(a,X) = f(a,b)	{ f ( bir , x ) = f ( bir , b ) }	{ x ↦ b }	fonksiyon ve sabit semboller eşleşir, x sabit b ile birleştirilir
f(a) = g(a)	{ f ( bir ) = g ( bir ) }	⊥	f ve g eşleşmiyor
f(X) = f(Y)	{ f ( x ) = f ( y ) }	{ x ↦ y }	x ve y takma addır
f(X) = g(Y)	{ f ( x ) = g ( y ) }	⊥	f ve g eşleşmiyor
f(X) = f(Y,Z)	{ f ( x ) = f ( y , z ) }	⊥	Başarısız. F fonksiyonu semboller farklı Arity sahip
f(g(X)) = f(Y)	{ f ( g ( x )) = f ( y ) }	{ y ↦ g ( x ) }	Bütünleştirir y terimi ile${\görüntüleme stili g(x)}$
f(g(X),X) = f(Y,a)	{ f ( g ( x ), x ) = f ( y , a ) }	{ x ↦ bir , y ↦ g ( bir ) }	Bütünleştirir x sabitine sahip a ve y terimi ile${\görüntüleme stili g(a)}$
X = f(X)	{ x = f ( x )}	⊥ olmalı	Birinci dereceden mantıkta ve birçok modern Prolog lehçesinde ⊥ döndürür (oluş denetimi tarafından zorlanır ). Geleneksel Prolog ve Prolog II'de başarılıdır, x'i sonsuz terimle birleştirir x=f(f(f(f(...)))).
X = Y, Y = a	{ x = y , y = bir }	{ x ↦ bir , y ↦ bir }	Hem x hem de y , a sabitiyle birleştirilir
a = Y, X = Y	{ a = y , x = y }	{ x ↦ bir , y ↦ bir }	Yukarıdaki gibi (kümedeki denklemlerin sırası önemli değil)
X = a, b = X	{ x = bir , b = x }	⊥	Başarısız. a ve b eşleşmez, bu nedenle x her ikisiyle de birleştirilemez

En az yaygın örnekleri için katlanarak daha büyük bir ağaç içeren iki terim. Onun dag gösterimi (en sağdaki, portakal parçası) doğrusal boyutta hala.

n boyutundaki bir sözdizimsel birinci dereceden birleştirme probleminin en genel birleştiricisi 2 ⁿ boyutunda olabilir . Örneğin, problem en genel birleştiriciye sahiptir , bkz. resim. Bu tür patlamaların neden olduğu üstel zaman karmaşıklığından kaçınmak için, gelişmiş birleştirme algoritmaları ağaçlar yerine yönlendirilmiş asiklik grafikler (daglar) üzerinde çalışır . ${\displaystyle (((a*z)*y)*x)*w\doteq w*(x*(y*(z*a)))}$${\displaystyle \{z\mapsto a,y\mapsto a*a,x\mapsto (a*a)*(a*a),w\mapsto ((a*a)*(a*a))*( (a*a)*(a*a))\}}$

Uygulama: mantıksal programlamada birleştirme

Birleştirme kavramı , en iyi Prolog dili aracılığıyla bilinen, mantık programlamasının arkasındaki ana fikirlerden biridir . Değişkenlerin içeriğini bağlama mekanizmasını temsil eder ve bir tür tek seferlik atama olarak görülebilir. Prolog'da bu işlem eşitlik sembolü ile gösterilir , ancak değişkenler başlatılırken de yapılır (aşağıya bakın). Diğer dillerde eşitlik sembolünün kullanımıyla ve aynı zamanda , , , dahil olmak üzere birçok işlemle birlikte kullanılır . Tür çıkarım algoritmaları tipik olarak birleştirmeye dayanır. ==+-*/

Prolog'da:

1. Örneklendirilmemiş bir değişken - yani üzerinde daha önce hiçbir birleştirme yapılmamış - bir atom, bir terim veya başka bir örneklenmemiş değişken ile birleştirilebilir, böylece etkin bir şekilde onun takma adı olur. Birçok modern Prolog lehçesinde ve birinci dereceden mantıkta , bir değişken onu içeren bir terimle birleştirilemez; bu sözde gerçekleşir kontrolüdür .
2. İki atom ancak özdeş olduklarında birleştirilebilir.
3. Benzer şekilde, eğer terimlerin üst fonksiyon sembolleri ve ariteleri aynıysa ve parametreler aynı anda birleştirilebiliyorsa, bir terim başka bir terimle birleştirilebilir. Bunun özyinelemeli bir davranış olduğunu unutmayın.

Uygulama: tür çıkarımı

Birleştirme, tür çıkarımı sırasında, örneğin işlevsel programlama dili Haskell'de kullanılır . Bir yandan programcının her fonksiyon için tip bilgisi vermesi gerekmez, diğer yandan yazım hatalarını tespit etmek için kullanılır. Haskell ifadesi True : ['x', 'y', 'z']doğru yazılmamış. Liste yapı işlevi (:)tiptedir a -> [a] -> [a], birinci parametre için Truepolimorfik tipi değişken aile birleşik olmak zorundadır True, çeşidini Bool. İkinci argüman, ['x', 'y', 'z'], türündedir, [Char]ancak aynı anda ve aikisi birden olamaz . BoolChar

Prolog'da olduğu gibi, tür çıkarımı için bir algoritma verilebilir:

1. Herhangi bir tür değişkeni, herhangi bir tür ifadesi ile birleşir ve bu ifadeye örneklenir. Belirli bir teori, bu kuralı bir meydana gelme kontrolü ile kısıtlayabilir.
2. İki tür sabiti, yalnızca aynı tür olduklarında birleşir.
3. İki tip yapı, yalnızca aynı tür kurucunun uygulamalarıysa ve tüm bileşen türleri özyinelemeli olarak birleşirse birleşir.

Bildirim niteliğinde olması nedeniyle, bir dizi birleştirmedeki sıra (genellikle) önemsizdir.

Birinci mertebeden mantık terminolojisinde bir atomun temel bir önerme olduğuna ve Prolog terimine benzer şekilde birleşik olduğuna dikkat edin.

Sıralı birleştirme

Sipariş olarak ayrılmış mantığı biri atamak için izin verir sıralama veya türünü her terimin, ve bir tür ilan etmek lar ₁ bir subsort başka tür ler ₂ , yaygın olarak yazılır s ₁ ⊆ s ₂ . Örneğin, biyolojik canlılar hakkında akıl yürütürken, bir tür köpeğini bir tür hayvanın alttürü olarak ilan etmek yararlıdır. Bazı tür bir terim her yerde ler gereklidir, herhangi subsort bir dönem s yerine temin edilebilir. Örneğin, anne : hayvan → hayvan işlev bildirimive sabit bir lassie : köpek bildirimi varsayarsak, anne ( lassie ) terimi tamamen geçerlidir ve hayvan türüne sahiptir. Bir köpeğin annesinin de köpek olduğu bilgisini sağlamak için başka bir anne : köpek → köpek beyanıverilebilir; buna, programlama dillerindeki aşırı yüklemeye benzer şekilde, işlev aşırı yüklemesi denir.

Walther , sıralanmış mantıkta terimler için bir birleştirme algoritması verdi, beyan edilen herhangi iki tür s ₁ , s _{2 için} bunların kesişimlerinin s ₁ ∩ s ₂ de bildirilmesini gerektirir: eğer x ₁ ve x ₂ , s ₁ türünde bir değişkense ve s ₂ , sırasıyla x ₁ ≐ x ₂ denklemi { x ₁ = x , x ₂ = x } çözümüne sahiptir , burada x : s ₁ ∩ s ₂ . Bu algoritmayı yan tümce tabanlı otomatik teorem ispatlayıcısına dahil ettikten sonra, bir kıyaslama problemini onu sıralı mantığa çevirerek çözebilir ve böylece birçok tekli yüklemin türe dönüştüğü gibi onu bir büyüklük sırasına indirebilir.

Smolka, parametrik polimorfizme izin vermek için genelleştirilmiş sıralı mantık . Onun çerçevesinde, alt sıralama bildirimleri karmaşık tür ifadelerine yayılır. Bir programlama örneği olarak, bir parametrik sıralama listesi ( X ) bildirilebilir ( X , bir C++ şablonunda olduğu gibi bir tür parametresidir ) ve bir alt sıralama bildiriminden int ⊆ float ilişki listesi ( int ) ⊆ list ( float ) otomatik olarak çıkarsama, yani her tamsayı listesinin aynı zamanda bir kayan nokta listesi olduğu anlamına gelir.

Schmidt-Schauß, terim bildirimlerine izin vermek için genelleştirilmiş sıralı mantık. Örnek olarak, alt sıralama bildirimlerinin bile ⊆ int ve tek ⊆ int olduğunu varsayarsak , ∀ i  : int gibi bir terim bildirimi . ( i + i ) : normal aşırı yükleme ile ifade edilemeyen bir tamsayı toplama özelliğinin bildirilmesine bile izin verir.

Sonsuz terimlerin birleşimi

Sonsuz ağaçların arka planı:

• B. Courcelle (1983). "Sonsuz Ağaçların Temel Özellikleri" (PDF) . Teori. Bilgisayar. Sci . 25 (2): 95–169. doi : 10.1016/0304-3975(83)90059-2 . Arşivlenmiş orijinal (PDF) 2014-04-21 tarihinde . 2013-06-28 alındı .
• Michael J. Maher (Tem 1988). "Sonlu, Rasyonel ve Sonsuz Ağaçların Cebirlerinin Tam Aksiyomatizasyonları". Proc. IEEE 3. Yıllık Semptom. Bilgisayar Biliminde Mantık Üzerine, Edinburgh . s. 348–357.
• Joxan Jaffar; Peter J. Stuckey (1986). "Sonsuz Ağaç Mantığı Programlamanın Semantiği" . Teorik Bilgisayar Bilimi . 46 : 141–158. doi : 10.1016/0304-3975(86)90027-7 .

Birleştirme algoritması, Prolog II:

• A. Colmerauer (1982). KL Clark; S.-A. Tarnlund (ed.). Prolog ve Sonsuz Ağaçlar . Akademik Basın.
• Alain Colmerauer (1984). "Sonlu ve Sonsuz Ağaçlarda Denklemler ve Eşitsizlikler". ICOT'ta (ed.). Proc. Int. Konf. Beşinci Nesil Bilgisayar Sistemlerinde . s. 85–99.

Uygulamalar:

• Francis Giannesini; Jacques Cohen (1984). "Prolog'un Sonsuz Ağaçlarını Kullanarak Ayrıştırıcı Oluşturma ve Dilbilgisi Manipülasyonu" . Mantık Programlama Dergisi . 1 (3): 253–265. doi : 10.1016/0743-1066(84)90013-X .

e-birleşme

E-birleştirme , belirli bir denklem kümesine, bazı denklemsel arka plan bilgisi E dikkate alınarak çözüm bulma problemidir . İkincisi bir dizi evrensel eşitlik olarak verilir . Bazı belirli E kümeleri için , denklem çözme algoritmaları (aka E-birleştirme algoritmaları ) geliştirilmiştir; diğerleri için böyle bir algoritmanın olamayacağı kanıtlanmıştır.

Örneğin, a ve b farklı sabitlerse, denklemin , operatör hakkında hiçbir şeyin bilinmediği, salt sözdizimsel birleştirmeye göre bir çözümü yoktur . Bununla birlikte, 'nin değişmeli olduğu biliniyorsa , o zaman { x ↦ b , y ↦ a } ikamesi yukarıdaki denklemi çözer, çünkü ${\displaystyle x*a\doteq y*b}$${\görüntüleme stili *}$${\görüntüleme stili *}$

	${\görüntüleme stili x*a}$	{ x ↦ b , y ↦ bir }
=	${\görüntüleme stili b*a}$		ile ikame uygulama
=	${\görüntüleme stili a*b}$		değişmeliliği ile ${\görüntüleme stili *}$
=	${\görüntüleme stili y*b}$	{ x ↦ b , y ↦ bir }	(converse) ikame uygulamasıyla

Arka plan bilgisi E , evrensel eşitlikle " tüm u , v için " değişkenliğini ifade edebilir . ${\görüntüleme stili *}$${\görüntüleme stili u*v=v*u}$

Özel arka plan bilgisi kümeleri E

Kullanılan adlandırma kuralları

∀ u , v , w :	${\ Displaystyle u*(v*w)}$	=	${\görüntüleme stili (u*v)*w}$	A	ilişkiselliği ${\görüntüleme stili *}$
∀ u , v :	${\görüntüleme stili u*v}$	=	${\ Displaystyle v*u}$	C	değişmeliliği ${\görüntüleme stili *}$
∀ u , v , w :	${\ Displaystyle u*(v+w)}$	=	${\ Displaystyle u*v+u*w}$	D l	Sol distributivity over${\görüntüleme stili *}$${\görüntüleme stili +}$
∀ u , v , w :	${\görüntüleme stili (v+w)*u}$	=	${\ Displaystyle v*u+w*u}$	D r	üzerinde doğru dağıtım${\görüntüleme stili *}$${\görüntüleme stili +}$
∀ u :	${\görüntüleme stili u*u}$	=	sen	ben	iktidarsızlığı ${\görüntüleme stili *}$
∀ u :	${\görüntüleme stili n*u}$	=	sen	N l	Sol nötr eleman n'ye göre${\görüntüleme stili *}$
∀ u :	${\görüntüleme stili u*n}$	=	sen	N r	Sağ nötr eleman n'ye göre${\görüntüleme stili *}$

Herhangi bir girdi problemi için sona eren bir birleştirme algoritması geliştirildiyse, bir teori için birleştirmenin kararlaştırılabilir olduğu söylenir . Söylenir birleştirmenin yarı Karar verilebilen bir birleşme algoritma herhangi biri için bunun için o sona erer icat edilmişse, bir teori çözülebilir giriş problemi ancak bir çözülemeyen giriş sorununun çözüm sonsuza aramaya devam edebilir.

Birleştirme, aşağıdaki teoriler için kararlaştırılabilir :

• A
• bir , C
• A , C , ben
• A , C , N _l
• bir , ben
• A , N _l , N _r (monoid)
• C
• Boole halkaları
• Değişken gruplar , imza isteğe bağlı ek sembollerle genişletilse bile (ancak aksiyomlarla değil)
• K4 mod cebirleri

Birleştirme, aşağıdaki teoriler için yarı karar verilebilir :

• A , D _l , D _r
• A , C , D _l
• değişmeli halkalar

Tek taraflı paramodülasyon

Bir varsa yakınsak terimi yeniden sistemi R için E , tek taraflı paramodulation algoritması verilen denklem tüm çözümler numaralandırmak için kullanılabilir.

İle başlayarak G birleşme çözülmesi gereken problem olan ve S kimlik ikame olan kurallar gerçek boş grubu görüntülenene kadar nondeterministically uygulanır G mevcut durumda, S birleştirici bir substitusyondur. Düzenine bağlı olarak paramodulation kuralları gerçek denklem seçimine uygulanır, G ve seçimine R ' s kurallar mutasyona farklı hesaplamaların yollar da mümkündür. Sadece bazıları bir çözüme yol açarken, diğerleri başka bir kuralın uygulanamadığı bir G ≠ {} ile biter (örn. G = { f (...) ≐ g (...) }).

Örnek olarak, cons ve nil öğelerinden oluşturulan listelerin ekleme operatörünü tanımlayan bir yeniden yazma sistemi R terimi kullanılır ; burada eksiler ( x , y ) infix notasyonunda x olarak yazılır . kısalık için y ; örneğin, uygulama ( a . b . sıfırdır , c . d . nil →) bir . Uygulama ( b . sıfırdır , c . d . nil →) bir . b . Uygulama ( sıfır , c . d . nil →) bir . b . c . d . nil , a listelerinin sıralanmasını gösterir . b . sıfır ve c . d . nil , yazma kuralı 2,2 ve 1. equational teori kullanılarak e karşılık gelen R bir uyum kapak arasında R , her iki şartlarda ikili ilişkiler olarak görülmektedir. Örneğin, uygulama ( a . b . nil , c . d . nil ) ≡ a . b . c . d . nil ≡ uygulaması ( a . b . c . d . nil , nil ). Paramodülasyon algoritması , R örneği ile beslendiğinde bu E'ye göre denklemlerin çözümlerini sıralar .

Birleştirme problemi için başarılı bir örnek hesaplama yolu { app ( x , app ( y , x )) ≐ a . bir . nil } aşağıda gösterilmiştir. Değişken adı çakışmalarını önlemek için, yeniden yazma kuralları, kural mutasyonuyla kullanılmadan önce her seferinde tutarlı bir şekilde yeniden adlandırılır ; v ₂ , v ₃ , ... bu amaç için bilgisayar tarafından oluşturulan değişken adlarıdır. Her satırda, G'den seçilen denklem kırmızıyla vurgulanır. Her mutasyon kuralı uygulanır, seçilen yeniden yazma kuralı ( 1 ya da 2 ) parantez içinde gösterilmektedir. Son satırdan, birleştirici ikame S = { y ↦ nil , x ↦ a . nil } elde edilebilir. Aslında, app ( x , app ( y , x )) { y ↦ nil , x ↦ a . nil } = Uygulama ( a . sıfır , uygulama ( sıfır , bir . nil )) ≡ Uygulama ( a . nil , bir . nil ) ≡ bir . app ( nil , a . nil ) ≡ a . bir . nil verilen sorunu çözer. "mutate(1), mutasyona(2), mutasyona(2), mutasyona(1)" seçilerek elde edilebilen ikinci bir başarılı hesaplama yolu, S = { y ↦ a ikamesine yol açar . bir . nil , x ↦ nil }; burada gösterilmemiştir. Başka hiçbir yol başarıya götürmez.

daraltma

Adım daralması Üçgen diyagramı s ↝ t pozisyonunda p terimi içinde lar yeniden yazma kuralı kullanılarak, ikame S (alt sıra) birleştirici ile, l → R (üst sıra)

Eğer R, a, yakınsak terimi yeniden sistemi için E , önceki bölüme bir yaklaşım alternatif "birbirini takip eden uygulama oluşur daralan adımları "; bu sonunda belirli bir denklemin tüm çözümlerini sıralayacaktır. Bir daraltma adımı (bkz. resim) şunlardan oluşur:

• mevcut terimin değişken olmayan bir alt terimini seçme,
• R'den bir kuralın sol tarafıyla sözdizimsel olarak birleştirir ve
• somutlaştırılmış kuralın sağ tarafını somutlaştırılmış terimle değiştirmek.

Resmi olarak eğer l → r bir olan yeniden adlandırılmış kopyası bir yeniden yazma kuralının R bir terim ile ortak noktası hiç değişkeni olan lar ve subterm s | _p , bir değişken değildir ile unifiable olan l ile mgu σ , o s edilebilir daralmış terime t = sσ [ rσ ] _p terimi, yani sσ de subterm ile, p ikame ile rσ . Bu durum, s için daraltılabilir t genel olarak ifade edilir s ↝ t . Sezgisel olarak, adımlar daralan bir dizi t ₁ ↝ t ₂ ↝ ... ↝ T _N yeniden yazma bir dizi adım olarak düşünülebilir t ₁ → t ₂ → ... → t _{, n} , ancak ilk terimiyle t ₁ olmak kullanılan kuralların her birini uygulanabilir kılmak için gerektiğinde daha fazla somutlaştırılır.

Yukarıdaki , aşağıdaki daralma sekansı ( "↓" burada örnekleme gösteren) için örnek paramodulation hesaplama karşılık:

Son terim, v ₂ . v ₂ . nil , orijinal sağ taraftaki terim a ile sözdizimsel olarak birleştirilebilir . bir . sıfır .

Daralması lemması bir terim bir örneği her sağlar s dönem için yeniden olabilir t yakınsak bir dönem yeniden sistemi ile, daha sonra s ve t daraltılmış bir dönem için yeniden edilebilir ler ' ve T ' , sırasıyla, bu şekilde t ' bir örneğidir s ' .

Resmi olarak: ne zaman sσ →∗ t , bir miktar σ ikamesi için geçerlidir, o zaman s ′ , t ′ terimleri vardır , öyle ki s ↝∗ s ' ve t →∗ t ′ ve s ′ τ = t ′ bazı ikameler için τ.

Üst düzey birleştirme

Birçok uygulama, birinci dereceden terimler yerine yazılan lambda terimlerinin birleştirilmesini dikkate almayı gerektirir. Bu tür bir birleşmeye genellikle üst düzey birleştirme denir . Yüksek mertebeden birleştirmenin iyi çalışılmış bir dalı, αβη dönüşümleri tarafından belirlenen eşitliği modülo olarak basitçe yazılan lambda terimlerini birleştirme problemidir. Bu tür birleştirme problemlerinin çoğu genel birleştiriciye sahip değildir. Yüksek mertebeden birleştirme kararsız olsa da , Gérard Huet , birleştiriciler uzayının sistematik olarak aranmasına izin veren yarı karar verilebilir (ön) bir birleştirme algoritması verdi (Martelli-Montanari'nin birleştirme algoritmasını daha yüksek mertebeden değişkenler içeren terimler için kurallarla genelleştirerek) bu pratikte yeterince iyi çalışıyor gibi görünüyor. Huet ve Gilles Dowek bu konuyu araştıran makaleler yazdılar.

Dale Miller , şimdi daha yüksek mertebeden örüntü birleştirme olarak adlandırılan şeyi tanımladı . Üst düzey birleştirmenin bu alt kümesi karar verilebilir ve çözülebilir birleştirme sorunlarının çoğu genel birleştiriciye sahiptir. Üst düzey mantık programlama dilleri λProlog ve Twelf gibi daha yüksek düzeyde birleştirme içeren birçok bilgisayar sistemi , genellikle tam üst düzey birleştirmeyi değil, yalnızca model parçasını uygular.

Hesaplamalı dilbilimde, en etkili üç nokta teorilerinden biri, elipslerin, değerleri daha sonra Yüksek Dereceli Birleştirme (HOU) kullanılarak belirlenen serbest değişkenlerle temsil edilmesidir. Örneğin, "Jon Mary'yi seviyor ve Peter da seviyor" ifadesinin semantik gösterimi like( j , m ) ∧ R( p ) şeklindedir ve R'nin değeri (üç noktanın semantik gösterimi) like( j , m ) = R( j ) . Bu tür denklemleri çözme işlemine Yüksek Dereceli Birleştirme denir.

Örneğin , tek değişkenin f olduğu { f ( a , b , a ) ≐ d ( b , a , c ) } birleştirme problemi , { f ↦ λ x .λ y .λ z . d ( y , x , c ) }, { f ↦ λ x .λ y .λ z . d ( y , z , c ) }, { f ↦ λ x .λ y .λ z . d ( y , a , c ) }, { f ↦ λ x .λ y .λ z . d ( b , x , c ) }, { f ↦ λ x .λ y .λ z . d ( b , z , c ) } ve { f ↦ λ x .λ y .λ z . d ( b , a , c )}.

Wayne Snyder , hem yüksek dereceli birleştirmenin hem de E-birleştirmenin bir genellemesini verdi, yani lambda terimlerini bir denklem teorisi olarak birleştirmek için bir algoritma.

Ayrıca bakınız

• yeniden yazma
• kabul edilebilir kural
• Açık ikame olarak lambda hesabı
• Matematiksel denklem çözme
• Dis- unification: sembolik ifade arasındaki eşitsizlikleri çözme
• Anti-birleştirme : iki terimin en az genel genellemesinin (lgg) hesaplanması, en genel bir örneğin (mgu) hesaplanması için ikili
• Ontology hizalama (kullanımı birleşmesi ile semantik denklik )

Notlar

Referanslar

daha fazla okuma

• Franz Baader ve Wayne Snyder (2001). "Unification Theory" 2015-06-08 tarihinde Wayback Machine sitesinde arşivlendi . In John Alan Robinson ve Andrei Voronkov , editörler, Otomatik MUHAKEMENİN Handbook , hacim I, sayfalar 447-533. Elsevier Bilim Yayıncıları.
• Gilles Dowek (2001). "Üst düzey Birleştirme ve Eşleştirme" . In Otomatik MUHAKEMENİN Handbook .
• Franz Baader ve Tobias Nipkow (1998). Terim Yeniden Yazma ve Hepsi . Cambridge Üniversitesi Yayınları.
• Franz Baader ve Jörg H. Siekmann  [ de ] (1993). "Birleşme Teorisi". In Yapay Zeka ve Mantık Programlama Mantık El Kitabı .
• Jean-Pierre Jouannaud ve Claude Kirchner (1991). "Soyut Cebirlerde Denklemleri Çözme: Bir Kurala Dayalı Birleştirme Araştırması". In Hesaplamalı Mantık: Alan Robinson Adına 'Denemeler .
• Nachum Dershowitz ve Jean-Pierre Jouannaud , Rewrite Systems , içinde: Jan van Leeuwen (ed.), Handbook of Theoretical Computer Science , cilt B Biçimsel Modeller ve Semantik , Elsevier, 1990, s. 243–320
• Jörg H. Siekmann (1990). "Birleşme Teorisi". In Claude Kirchner (editör) Birleşme . Akademik Basın.
• Kevin Şövalye (Mar 1989). "Birleştirme: Çok Disiplinli Bir Araştırma" (PDF) . ACM Bilgi İşlem Anketleri . 21 (1): 93–124. CiteSeerX  10.1.1.64.8967 . doi : 10.1145/62029.62030 . S2CID  14619034 .
• Gérard Huet ve Derek C. Oppen (1980). "Denklemler ve Yeniden Yazma Kuralları: Bir Anket" . Teknik rapor. Stanford Üniversitesi.
• Raulefs, Peter; Siekmann, Jörg; Szabo, P.; Unvericht, E. (1979). "Eşleştirme ve birleştirme problemlerinde son teknoloji üzerine kısa bir araştırma". ACM SIGSAM Bülteni . 13 (2): 14–20. doi : 10.1145/1089208.1089210 . S2CID  17033087 .
• Claude Kirchner ve Helene Kirchner. Yeniden Yazma, Çözme, Kanıtlama . Hazırlık aşamasında.