# File:Solving the word problem without and with completion.pdf

Original file(1,210 × 1,240 pixels, file size: 9 KB, MIME type: application/pdf)

### Captions

Add a one-line explanation of what this file represents

## 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 6 June 2014, 22:46:12 Source Own work Author Other versions

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}}%
\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:

## File history

Click on a date/time to view the file as it appeared at that time.

Date/TimeThumbnailDimensionsUserComment
current14:02, 9 June 20141,210 × 1,240 (9 KB)Jochen Burghardt (talk | contribs)several possible normalizing paths in canonical rewrite system
20:49, 6 June 20141,210 × 1,240 (14 KB)Jochen Burghardt (talk | contribs)User created page with UploadWizard

There are no pages that use this file.