File:Solving the word problem without and with completion.pdf
Summary
| Description |
English: Shows a simplified example of the search space for deciding the word problem, i.e., given a set E of equations and two terms s,t (represented by the left- and rightmost vertice), to decide if s=t follows from E. Proof search usually runs into dead ends (red paths); to find a valid proof (green path) may be infeasible without human intuition. However, if the Knuth-Bendix completion algorithm was able to compute from E an equivalent confluent (and terminating) term rewriting system R (shadow paths), deciding if s=t is simple: apply rules from R to s as long as possible to obtain a term s’ (s’ is unique, no matter in which the order rules are applied), rewrite t to some t’ in a similar way, then s=t if and only if s’=t’. |
| Date | |
| Source | Own work |
| Author | Jochen Burghardt |
| Other versions | File:Solving the word problem without and with completion svg.svg |
LaTeX source Code |
|---|
\documentclass[12pt]{article}
\usepackage[pdftex]{color}
\usepackage[paperwidth=205mm,paperheight=210mm]{geometry}
\setlength{\topmargin}{-36mm}
\setlength{\textwidth}{205mm}
\setlength{\textheight}{210mm}
\setlength{\evensidemargin}{-2.7cm}
\setlength{\oddsidemargin}{-2.5cm}
\setlength{\parindent}{0cm}
\setlength{\parskip}{1ex}
\setlength{\unitlength}{1mm}
\sloppy
%%%%% labyrinth convenience macros %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\conn}{\vector}
\newcounter{curX} % current x coordinate (in unit lengths)
\newcounter{curY} % current y coordinate (in unit lengths)
% dir{X}{Y}: advance line in direction 10*X,10*Y
\newcommand{\dir}[2]{%
\put(\arabic{curX},\arabic{curY}){\conn(#1,#2){10}}%
\addtocounter{curX}{#1}\addtocounter{curX}{#1}%
\addtocounter{curX}{#1}\addtocounter{curX}{#1}%
\addtocounter{curX}{#1}\addtocounter{curX}{#1}%
\addtocounter{curX}{#1}\addtocounter{curX}{#1}%
\addtocounter{curX}{#1}\addtocounter{curX}{#1}%
\addtocounter{curY}{#2}\addtocounter{curY}{#2}%
\addtocounter{curY}{#2}\addtocounter{curY}{#2}%
\addtocounter{curY}{#2}\addtocounter{curY}{#2}%
\addtocounter{curY}{#2}\addtocounter{curY}{#2}%
\addtocounter{curY}{#2}\addtocounter{curY}{#2}%
\put(\arabic{curX},\arabic{curY}){\circle*{1}}%
}
% \go{X}{Y}: start line at X,Y
\newcommand{\go}[2]{%
\setcounter{curX}{#1}%
\setcounter{curY}{#2}%
\put(\arabic{curX},\arabic{curY}){\circle*{1}}%
}
% windrose commands
\renewcommand{\ne}{\dir{+1}{+1}}
\newcommand{\nw}{\dir{-1}{+1}}
\newcommand{\sw}{\dir{-1}{-1}}
\newcommand{\se}{\dir{+1}{-1}}
%%%%% colors %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\definecolor{cSuc} {rgb}{0.00,0.50,0.00} % successful eqn proof
\definecolor{cFai} {rgb}{0.99,0.30,0.30} % failed eqn proof attempts
\definecolor{cAvl} {rgb}{0.90,0.90,0.90} % available rewrites
\definecolor{cUse} {rgb}{0.40,0.40,0.40} % used rewrites
\begin{document}
~
\begin{picture}(200,200)
% confluent and terminating rewriting system
\color{cAvl}
\multiput(0,97)(10,10){11}{\multiput(0,0)(10,-10){11}{\circle*{1}}}%
\multiput(0,97)(10,10){11}{\multiput(0,0)(10,-10){10}{\vector(1,-1){10}}}%
\multiput(100,197)(10,-10){11}{\multiput(0,0)(-10,-10){10}{\vector(-1,-1){10}}}%
% actually used to compute normal forms
\color{cUse}
\put(20,97){\circle*{2}}% left
\go{20}{97}\se\se\se\se\sw\se\se\se\se\se%
\put(170,107){\circle*{2}}% right
\go{170}{107}\sw\sw\se\sw\sw\se\sw\sw\sw\sw\sw%
\put(100,-4){\circle*{2}}% normal form
\renewcommand{\conn}{\line}%
\thicklines%
% unsuccessful equations
\color{cFai}%
\go{10}{90}\nw\ne\ne\ne\se\ne\nw\ne\se\se\ne\ne\nw\sw\nw\ne\ne\se\ne\ne\nw\sw%
\go{70}{130}\sw\sw\se\se%
\go{20}{100}\ne\se\se%
\go{190}{90}\ne\nw\nw\nw\nw\sw\sw\nw\nw\ne\nw\sw\nw\ne%
\go{160}{140}\nw\sw%
\go{110}{190}\se\se\se%
\go{20}{80}\se\se\se\ne\se\ne\ne\ne\ne\nw\nw%
\go{110}{130}\se\se\se\ne\ne
\go{100}{60}\sw\sw\sw\nw%
\go{140}{60}\sw\se\sw\nw\sw\nw\sw\sw\se\ne\se\ne\ne%
\go{170}{110}\se\se\sw\nw\sw\se\sw\sw%
\go{90}{10}\se%
% successful equations
\color{cSuc}%
\go{20}{100}\sw\se\ne\se\se\ne\se\ne\ne\nw\nw\ne\ne\ne\se\sw\se\se\se%
\sw\sw\sw\se\ne\ne\se\ne\nw\ne\ne\ne%
\put(20,100){\circle*{2}}%
\put(170,110){\circle*{2}}%
\end{picture}
\end{document}
|
Licensing
I, the copyright holder of this work, hereby publish it under the following license:
This file is licensed under the Creative Commons Attribution-Share Alike 3.0 Unported license.
- You are free:
- to share – to copy, distribute and transmit the work
- to remix – to adapt the work
- Under the following conditions:
- attribution – You must give appropriate credit, provide a link to the license, and indicate if changes were made. You may do so in any reasonable manner, but not in any way that suggests the licensor endorses you or your use.
- share alike – If you remix, transform, or build upon the material, you must distribute your contributions under the same or compatible license as the original.