\documentclass[12pt]{article}

\title{18.510 HW1\\An Algorithm for Validating WWFs}

\author{by Nada Amin {\tt(namin@mit.edu)}, \\
in collaboration with Bernardo Zacka {\tt(nardoz@mit.edu)}}

\begin{document}

\maketitle

\paragraph{}{
  An expression is a completely arbitrary finite sequence of the
atomic propositional letters, parentheses and the operators ($\neg$,
$\vee$, $\wedge$, $\rightarrow$, $\leftrightarrow$).  We propose an
algorithm that decides whether or not an arbitrary expression is a
well-formed formula (WFF).  }

\section{Algorithm}

\paragraph{} {
  Let E be an expression we wish to validate.
}

\paragraph{1} {
  The first symbol of $E$ must be $($ and the last must be $)$.
  Otherwise,  E is not a WFF. 
}

\paragraph{2} {
  Now, consider $E'$, such that $E$ is $(E')$.
}

\paragraph{2.1} {
  If $E'$ is a propositional letter, then $E$ is a WFF.
}

\paragraph{2.2} {
  If the first symbol of $E'$ is $\neg$, 
  then $E$ is a WFF if $E''$, such that $'E=\neg E''$, is a WFF.
}

\paragraph{2.3} {
  We check if $E'$ has the form $F\textrm{op}J$, 
  where $F$ and $J$ are WFFs, and op is one of the valid binary operators
  $\vee$, $\wedge$, $\rightarrow$, $\leftrightarrow$.

  If $F$ and $J$ are WFFs, they must have the same number of $($ and $)$,
  because in the recursive definition of a WFF, $($ and $)$ always come in
  pairs.  Furthermore, if $E$ is a WFF, there can only be one
  operator op, such that $E=(F\textrm{op}J)$. If there were more than
  one such operator, say two, op1 and op2, then
  $E=(F\textrm{op1}J\textrm{op2}K)$.  But then, the expression at the
  left of op1, $J\textrm{op2}K$ is not well-formed, since it lacks the
  parentheses, as is the expression at the right of op2. Therefore,
  the decomposition of $E$ into $F$ and $J$ is unique.

  To find this decomposition, we scan $E'$. The first symbol must be
  $($.  While we scan, we keep track of the difference between the
  number of $($ and the number of $)$.  When this difference is null
  (if it never is, then E is not a WFF), we check that what follows is
  a valid binary operator. If it is, we let $F$ be everything in $E'$
  that is on the left of the operator and $J$ to be everything in $E'$
  that is on the right of the operator, such that
  $E'=F\textrm{op}J$. E is a WFF, if both $F$ and $J$ are WFFs.

  }

\section{Remarks}

\paragraph{Termination} {
  At every step, the algorithm either terminates by reaching a
  propositional letter or by concluding that the expression is not a
  WFF, or either repeats itself for shorter expressions (potential
  WFFs). Since the expression it starts with is a finite sequence and
  since it is reduced at ever iteration, the algorithm must terminate.
}

\paragraph{Correctness} {
  The algorithm attempts to find the only possible decomposition of an
  expression by following the hierarchy of parentheses. If it finds
  it, then the expression is a WFF and we can actually reconstruct it
  by applying the definition. If it doesn't find it, then the expression
  is not a WFF, because the only possible attempt to find such a
  decomposition failed.
}

\section{Annex}

\paragraph{} {
  An implementation of the algorithm in Scheme is provided.
}

\section{Reference}

\paragraph{} {
  ENDERTON, \it{A Mathematical Introduction to Logic}
}

\end{document} 
