Editing Unification (computer science) (section)

==Order-sorted unification==
''[[Order-sorted logic]]'' allows one to assign a ''sort'', or ''type'', to each term, and to declare a sort ''s''<sub>1</sub> a ''subsort'' of another sort ''s''<sub>2</sub>, commonly written as ''s''<sub>1</sub> ⊆ ''s''<sub>2</sub>. For example, when reаsoning about biological creatures, it is useful to declare a sort ''dog'' to be a subsort of a sort ''animal''. Wherever a term of some sort ''s'' is required, a term of any subsort of ''s'' may be supplied instead.
For example, assuming a function declaration ''mother'': ''animal'' → ''animal'', and a constant declaration ''lassie'': ''dog'', the term  ''mother''(''lassie'') is perfectly valid and has the sort ''animal''. In order to supply the information that the mother of a dog is a dog in turn, another declaration ''mother'': ''dog'' → ''dog'' may be issued; this is called ''function overloading'', similar to [[overloading in programming languages]].

[[Christoph Walther|Walther]] gave a unification algorithm for terms in order-sorted logic, requiring for any two declared sorts ''s''<sub>1</sub>, ''s''<sub>2</sub> their intersection ''s''<sub>1</sub> ∩ ''s''<sub>2</sub> to be declared, too: if ''x''<sub>1</sub> and ''x''<sub>2</sub> is a variable of sort ''s''<sub>1</sub> and ''s''<sub>2</sub>, respectively, the equation ''x''<sub>1</sub> ≐ ''x''<sub>2</sub> has the solution { ''x''<sub>1</sub> = ''x'', ''x''<sub>2</sub> = ''x'' }, where ''x'': ''s''<sub>1</sub> ∩ ''s''<sub>2</sub>.
<ref>{{cite journal|first1=Christoph|last1=Walther|author-link=Christoph Walther|title=A Mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution|journal=Artif. Intell.|volume=26|number=2|pages=217–224|url=http://www.inferenzsysteme.informatik.tu-darmstadt.de/media/is/publikationen/Schuberts_Steamroller_by_Many-Sorted_Resolution-AIJ-25-2-1985.pdf|year=1985|doi=10.1016/0004-3702(85)90029-3|access-date=2013-06-28|archive-date=2011-07-08|archive-url=https://web.archive.org/web/20110708231225/http://www.inferenzsysteme.informatik.tu-darmstadt.de/media/is/publikationen/Schuberts_Steamroller_by_Many-Sorted_Resolution-AIJ-25-2-1985.pdf|url-status=dead}}</ref>
After incorporating this algorithm into a clause-based automated theorem prover, he could solve a benchmark problem by translating it into order-sorted logic, thereby boiling it down an order of magnitude, as many unary predicates turned into sorts.

Smolka generalized order-sorted logic to allow for [[parametric polymorphism]].
<ref>{{cite conference|first1=Gert|last1=Smolka|title=Logic Programming with Polymorphically Order-Sorted Types|conference=Int. Workshop Algebraic and Logic Programming|publisher=Springer|series=LNCS|volume=343|pages=53–70|date=Nov 1988|url=https://link.springer.com/content/pdf/10.1007/3-540-50667-5_58.pdf|doi=10.1007/3-540-50667-5_58}}</ref>
In his framework, subsort declarations are propagated to complex type expressions.
As a programming example, a parametric sort ''list''(''X'') may be declared (with ''X'' being a type parameter as in a [[Template (C++)#Function templates|C++ template]]), and from a subsort declaration ''int'' ⊆ ''float'' the relation ''list''(''int'') ⊆ ''list''(''float'') is automatically inferred, meaning that each list of integers is also a list of floats.

Schmidt-Schauß generalized order-sorted logic to allow for term declarations.
<ref>{{cite book|first1=Manfred|last1=Schmidt-Schauß|title=Computational Aspects of an Order-Sorted Logic with Term Declarations|publisher=Springer|series=[[Lecture Notes in Artificial Intelligence]] (LNAI)|volume=395|date=Apr 1988}}</ref>
As an example, assuming subsort declarations ''even'' ⊆ ''int'' and ''odd'' ⊆ ''int'', a term declaration like ∀ ''i'' : ''int''. (''i'' + ''i'') : ''even'' allows to declare a property of integer addition that could not be expressed by ordinary overloading.