ueq-binary-op.tex

\documentclass[leqno,fleqn,12pt]{article}

\usepackage{euler,beton,concrete,url,a4wide}
\usepackage[T1]{fontenc}

%% ODER: format ==         = "\mathrel{==}"
%% ODER: format /=         = "\neq "
%
%
\makeatletter
\@ifundefined{lhs2tex.lhs2tex.sty.read}%
  {\@namedef{lhs2tex.lhs2tex.sty.read}{}%
   \newcommand\SkipToFmtEnd{}%
   \newcommand\EndFmtInput{}%
   \long\def\SkipToFmtEnd#1\EndFmtInput{}%
  }\SkipToFmtEnd

\newcommand\ReadOnlyOnce[1]{\@ifundefined{#1}{\@namedef{#1}{}}\SkipToFmtEnd}
\usepackage{amstext}
\usepackage{amssymb}
\usepackage{stmaryrd}
\DeclareFontFamily{OT1}{cmtex}{}
\DeclareFontShape{OT1}{cmtex}{m}{n}
  {<5><6><7><8>cmtex8
   <9>cmtex9
   <10><10.95><12><14.4><17.28><20.74><24.88>cmtex10}{}
\DeclareFontShape{OT1}{cmtex}{m}{it}
  {<-> ssub * cmtt/m/it}{}
\newcommand{\texfamily}{\fontfamily{cmtex}\selectfont}
\DeclareFontShape{OT1}{cmtt}{bx}{n}
  {<5><6><7><8>cmtt8
   <9>cmbtt9
   <10><10.95><12><14.4><17.28><20.74><24.88>cmbtt10}{}
\DeclareFontShape{OT1}{cmtex}{bx}{n}
  {<-> ssub * cmtt/bx/n}{}
\newcommand{\tex}[1]{\text{\texfamily#1}}	% NEU

\newcommand{\Sp}{\hskip.33334em\relax}


\newcommand{\Conid}[1]{\mathit{#1}}
\newcommand{\Varid}[1]{\mathit{#1}}
\newcommand{\anonymous}{\kern0.06em \vbox{\hrule\@width.5em}}
\newcommand{\plus}{\mathbin{+\!\!\!+}}
\newcommand{\bind}{\mathbin{>\!\!\!>\mkern-6.7mu=}}
\newcommand{\rbind}{\mathbin{=\mkern-6.7mu<\!\!\!<}}% suggested by Neil Mitchell
\newcommand{\sequ}{\mathbin{>\!\!\!>}}
\renewcommand{\leq}{\leqslant}
\renewcommand{\geq}{\geqslant}
\usepackage{polytable}

%mathindent has to be defined
\@ifundefined{mathindent}%
  {\newdimen\mathindent\mathindent\leftmargini}%
  {}%

\def\resethooks{%
  \global\let\SaveRestoreHook\empty
  \global\let\ColumnHook\empty}
\newcommand*{\savecolumns}[1][default]%
  {\g@addto@macro\SaveRestoreHook{\savecolumns[#1]}}
\newcommand*{\restorecolumns}[1][default]%
  {\g@addto@macro\SaveRestoreHook{\restorecolumns[#1]}}
\newcommand*{\aligncolumn}[2]%
  {\g@addto@macro\ColumnHook{\column{#1}{#2}}}

\resethooks

\newcommand{\onelinecommentchars}{\quad-{}- }
\newcommand{\commentbeginchars}{\enskip\{-}
\newcommand{\commentendchars}{-\}\enskip}

\newcommand{\visiblecomments}{%
  \let\onelinecomment=\onelinecommentchars
  \let\commentbegin=\commentbeginchars
  \let\commentend=\commentendchars}

\newcommand{\invisiblecomments}{%
  \let\onelinecomment=\empty
  \let\commentbegin=\empty
  \let\commentend=\empty}

\visiblecomments

\newlength{\blanklineskip}
\setlength{\blanklineskip}{1mm}

\newcommand{\hsindent}[1]{\quad}% default is fixed indentation
\let\hspre\empty
\let\hspost\empty
\newcommand{\NB}{\textbf{NB}}
\newcommand{\Todo}[1]{$\langle$\textbf{To do:}~#1$\rangle$}

\EndFmtInput
\makeatother
%
%
%
%
%
%
% This package provides two environments suitable to take the place
% of hscode, called "plainhscode" and "arrayhscode". 
%
% The plain environment surrounds each code block by vertical space,
% and it uses \abovedisplayskip and \belowdisplayskip to get spacing
% similar to formulas. Note that if these dimensions are changed,
% the spacing around displayed math formulas changes as well.
% All code is indented using \leftskip.
%
% Changed 19.08.2004 to reflect changes in colorcode. Should work with
% CodeGroup.sty.
%
\ReadOnlyOnce{polycode.fmt}%
\makeatletter

\newcommand{\hsnewpar}[1]%
  {{\parskip=0pt\parindent=0pt\par\vskip #1\noindent}}

% can be used, for instance, to redefine the code size, by setting the
% command to \small or something alike
\newcommand{\hscodestyle}{}

% The command \sethscode can be used to switch the code formatting
% behaviour by mapping the hscode environment in the subst directive
% to a new LaTeX environment.

\newcommand{\sethscode}[1]%
  {\expandafter\let\expandafter\hscode\csname #1\endcsname
   \expandafter\let\expandafter\endhscode\csname end#1\endcsname}

% "compatibility" mode restores the non-polycode.fmt layout.

\newenvironment{compathscode}%
  {\par\noindent
   \advance\leftskip\mathindent
   \hscodestyle
   \let\\=\@normalcr
   \(\pboxed}%
  {\endpboxed\)%
   \par\noindent
   \ignorespacesafterend}

\newcommand{\compaths}{\sethscode{compathscode}}

% "plain" mode is the proposed default.
% It should now work with \centering.
% This required some changes. The old version
% is still available for reference as oldplainhscode.

\newenvironment{plainhscode}%
  {\hsnewpar\abovedisplayskip
   \advance\leftskip\mathindent
   \hscodestyle
   \let\hspre\(\let\hspost\)%
   \pboxed}%
  {\endpboxed%
   \hsnewpar\belowdisplayskip
   \ignorespacesafterend}

\newenvironment{oldplainhscode}%
  {\hsnewpar\abovedisplayskip
   \advance\leftskip\mathindent
   \hscodestyle
   \let\\=\@normalcr
   \(\pboxed}%
  {\endpboxed\)%
   \hsnewpar\belowdisplayskip
   \ignorespacesafterend}

% Here, we make plainhscode the default environment.

\newcommand{\plainhs}{\sethscode{plainhscode}}
\newcommand{\oldplainhs}{\sethscode{oldplainhscode}}
\plainhs

% The arrayhscode is like plain, but makes use of polytable's
% parray environment which disallows page breaks in code blocks.

\newenvironment{arrayhscode}%
  {\hsnewpar\abovedisplayskip
   \advance\leftskip\mathindent
   \hscodestyle
   \let\\=\@normalcr
   \(\parray}%
  {\endparray\)%
   \hsnewpar\belowdisplayskip
   \ignorespacesafterend}

\newcommand{\arrayhs}{\sethscode{arrayhscode}}

% The mathhscode environment also makes use of polytable's parray 
% environment. It is supposed to be used only inside math mode 
% (I used it to typeset the type rules in my thesis).

\newenvironment{mathhscode}%
  {\parray}{\endparray}

\newcommand{\mathhs}{\sethscode{mathhscode}}

% texths is similar to mathhs, but works in text mode.

\newenvironment{texthscode}%
  {\(\parray}{\endparray\)}

\newcommand{\texths}{\sethscode{texthscode}}

% The framed environment places code in a framed box.

\def\codeframewidth{\arrayrulewidth}
\RequirePackage{calc}

\newenvironment{framedhscode}%
  {\parskip=\abovedisplayskip\par\noindent
   \hscodestyle
   \arrayrulewidth=\codeframewidth
   \tabular{@{}|p{\linewidth-2\arraycolsep-2\arrayrulewidth-2pt}|@{}}%
   \hline\framedhslinecorrect\\{-1.5ex}%
   \let\endoflinesave=\\
   \let\\=\@normalcr
   \(\pboxed}%
  {\endpboxed\)%
   \framedhslinecorrect\endoflinesave{.5ex}\hline
   \endtabular
   \parskip=\belowdisplayskip\par\noindent
   \ignorespacesafterend}

\newcommand{\framedhslinecorrect}[2]%
  {#1[#2]}

\newcommand{\framedhs}{\sethscode{framedhscode}}

% The inlinehscode environment is an experimental environment
% that can be used to typeset displayed code inline.

\newenvironment{inlinehscode}%
  {\(\def\column##1##2{}%
   \let\>\undefined\let\<\undefined\let\\\undefined
   \newcommand\>[1][]{}\newcommand\<[1][]{}\newcommand\\[1][]{}%
   \def\fromto##1##2##3{##3}%
   \def\nextline{}}{\) }%

\newcommand{\inlinehs}{\sethscode{inlinehscode}}

% The joincode environment is a separate environment that
% can be used to surround and thereby connect multiple code
% blocks.

\newenvironment{joincode}%
  {\let\orighscode=\hscode
   \let\origendhscode=\endhscode
   \def\endhscode{\def\hscode{\endgroup\def\@currenvir{hscode}\\}\begingroup}
   %\let\SaveRestoreHook=\empty
   %\let\ColumnHook=\empty
   %\let\resethooks=\empty
   \orighscode\def\hscode{\endgroup\def\@currenvir{hscode}}}%
  {\origendhscode
   \global\let\hscode=\orighscode
   \global\let\endhscode=\origendhscode}%

\makeatother
\EndFmtInput
%

% comment format $ = "\ "

\def\prompt#1{\noindent$\gg$ #1}

\title{On the Inexistence\\
       of a\\
       Unique Existential Binary Operator}
\author{
   Jo\~ao F. Ferreira \\{\tt\small joao@joaoff.com}
}
\date{\today}

\begin{document}
\maketitle

\begin{abstract}
We prove that there is not any boolean binary operator that can be quantified over an 
arbitrary set of values to express that exactly one of them is $\sf{true}$. 
Our proof is a Haskell program that verifies this fact for all sixteen
possible boolean binary operators.
\end{abstract}


\section{Introduction}
Boolean inequality, usually denoted by $\not\equiv$ and sometimes called exclusive-or, can be used to express
that exactly one of two values is ${\sf true}$. However, we can not use it to express
that exactly one of three values is ${\sf true}$ (e.g. ${\sf true}{\not\equiv}{\sf true}{\not\equiv}{\sf true}$ is {\sf true} and all of the operands are {\sf true}). In this note, we prove that there
is not any binary operator that can be quantified over an arbitrary set of values to express that
exactly one of them is $\sf{true}$. Our proof is a Haskell program that, for all binary boolean operators $\oplus$, shows that it is impossible to evaluate $(a{\oplus}b){\oplus}c$ or $a{\oplus}(b{\oplus}c)$ to
{\sf true} exactly when one of $a$, $b$, and $c$ is {\sf true} and to {\sf false} otherwise.


\section{Boolean Binary Operators}
We start by defining some useful datatypes. A binary operator $\oplus$ has type \ensuremath{\Conid{BinOp}};
it is represented as a list of pairs \ensuremath{(\Conid{Input},\Conid{Output})}, where \ensuremath{\Conid{Input}} is a pair of booleans 
$(a,b)$ and the \ensuremath{\Conid{Output}} is the result of $a{\oplus}b$.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{16}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\mathbf{type}\;\Conid{Input}{}\<[16]%
\>[16]{}\mathrel{=}(\Conid{Bool},\Conid{Bool}){}\<[E]%
\\
\>[3]{}\mathbf{type}\;\Conid{Output}{}\<[16]%
\>[16]{}\mathrel{=}\Conid{Bool}{}\<[E]%
\\
\>[3]{}\mathbf{type}\;\Conid{BinOp}{}\<[16]%
\>[16]{}\mathrel{=}[\mskip1.5mu (\Conid{Input},\Conid{Output})\mskip1.5mu]{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
The value \ensuremath{\Varid{boolvars}} is defined for convenience.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{13}{@{}>{\hspre}c<{\hspost}@{}}%
\column{13E}{@{}l@{}}%
\column{16}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\Varid{boolvars}{}\<[13]%
\>[13]{}\mathrel{=}{}\<[13E]%
\>[16]{}[\mskip1.5mu \Conid{True},\Conid{False}\mskip1.5mu]{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
The function \ensuremath{\Varid{inputs}} lists all four possible inputs.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{13}{@{}>{\hspre}l<{\hspost}@{}}%
\column{16}{@{}>{\hspre}l<{\hspost}@{}}%
\column{27}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\Varid{inputs}{}\<[13]%
\>[13]{}\mathbin{::}[\mskip1.5mu \Conid{Input}\mskip1.5mu]{}\<[E]%
\\
\>[3]{}\Varid{inputs}{}\<[13]%
\>[13]{}\mathrel{=}{}\<[16]%
\>[16]{}[\mskip1.5mu (\Varid{a},\Varid{b})\mid {}\<[27]%
\>[27]{}\Varid{a}\leftarrow \Varid{boolvars},{}\<[E]%
\\
\>[27]{}\Varid{b}\leftarrow \Varid{boolvars}\mskip1.5mu]{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
The function \ensuremath{\Varid{outputs}} lists all sixteen possible outputs.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{13}{@{}>{\hspre}l<{\hspost}@{}}%
\column{16}{@{}>{\hspre}l<{\hspost}@{}}%
\column{31}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\Varid{outputs}{}\<[13]%
\>[13]{}\mathbin{::}[\mskip1.5mu [\mskip1.5mu \Conid{Output}\mskip1.5mu]\mskip1.5mu]{}\<[E]%
\\
\>[3]{}\Varid{outputs}{}\<[13]%
\>[13]{}\mathrel{=}{}\<[16]%
\>[16]{}[\mskip1.5mu [\mskip1.5mu \Varid{a},\Varid{b},\Varid{c},\Varid{d}\mskip1.5mu]\mid {}\<[31]%
\>[31]{}\Varid{a}\leftarrow \Varid{boolvars},{}\<[E]%
\\
\>[31]{}\Varid{b}\leftarrow \Varid{boolvars},{}\<[E]%
\\
\>[31]{}\Varid{c}\leftarrow \Varid{boolvars},{}\<[E]%
\\
\>[31]{}\Varid{d}\leftarrow \Varid{boolvars}\mskip1.5mu]{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
The first element returned by \ensuremath{\Varid{outputs}} corresponds to the binary operator {\sl constant true},
as the following snippet shows:

\medskip
\indent\prompt{head outputs}\\
\indent\ensuremath{[\mskip1.5mu \Conid{True},\Conid{True},\Conid{True},\Conid{True}\mskip1.5mu]}
\medskip

\noindent Finally, the function \ensuremath{\Varid{operators}} returns the list of all the sixteen boolean binary operators.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{14}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\Varid{operators}{}\<[14]%
\>[14]{}\mathbin{::}[\mskip1.5mu \Conid{BinOp}\mskip1.5mu]{}\<[E]%
\\
\>[3]{}\Varid{operators}{}\<[14]%
\>[14]{}\mathrel{=}\Varid{map}\;(\Varid{zip}\;\Varid{inputs})\;\Varid{outputs}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
The first element returned by \ensuremath{\Varid{operators}} is the binary operator {\sl constant true}:

\medskip
\indent\prompt{head operators}\\
\indent\ensuremath{[\mskip1.5mu ((\Conid{True},\Conid{True}),\Conid{True}),((\Conid{True},\Conid{False}),\Conid{True}),((\Conid{False},\Conid{True}),\Conid{True}),((\Conid{False},\Conid{False}),\Conid{True})\mskip1.5mu]}
\medskip

\section{Unique Existential Operator}
Now, recall that our goal is to check the value of the two following expressions, for all
booleans $a$, $b$, and $c$, and for all boolean binary operators $\oplus$:

\[
(a{\oplus}b){\oplus}c {\textrm ~~~~and~~~~} a{\oplus}(b{\oplus}c) {\textrm ~~~.}
\]
First, we generate all possible inputs for the above expressions.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{10}{@{}>{\hspre}l<{\hspost}@{}}%
\column{25}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\Varid{tinps}{}\<[10]%
\>[10]{}\mathbin{::}[\mskip1.5mu (\Conid{Bool},\Conid{Bool},\Conid{Bool})\mskip1.5mu]{}\<[E]%
\\
\>[3]{}\Varid{tinps}{}\<[10]%
\>[10]{}\mathrel{=}[\mskip1.5mu (\Varid{a},\Varid{b},\Varid{c})\mid {}\<[25]%
\>[25]{}\Varid{a}\leftarrow \Varid{boolvars},{}\<[E]%
\\
\>[25]{}\Varid{b}\leftarrow \Varid{boolvars},{}\<[E]%
\\
\>[25]{}\Varid{c}\leftarrow \Varid{boolvars}\mskip1.5mu]{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
Second, we define two functions, \ensuremath{\Varid{checkl}} and \ensuremath{\Varid{checkr}}, that given a list of 
inputs and a binary operator, evaluates each of the inputs using that operator.
\ensuremath{\Varid{checkl}} associates to the left and \ensuremath{\Varid{checkr}} associates to the right.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{24}{@{}>{\hspre}l<{\hspost}@{}}%
\column{28}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\Varid{checkl}{}\<[28]%
\>[28]{}\mathbin{::}[\mskip1.5mu (\Conid{Bool},\Conid{Bool},\Conid{Bool})\mskip1.5mu]\to \Conid{BinOp}\to [\mskip1.5mu \Conid{Output}\mskip1.5mu]{}\<[E]%
\\
\>[3]{}\Varid{checkl}\;[\mskip1.5mu \mskip1.5mu]\;{}\<[24]%
\>[24]{}\anonymous {}\<[28]%
\>[28]{}\mathrel{=}[\mskip1.5mu \mskip1.5mu]{}\<[E]%
\\
\>[3]{}\Varid{checkl}\;((\Varid{a},\Varid{b},\Varid{c})\mathbin{:}\Varid{xs})\;{}\<[24]%
\>[24]{}\Varid{op}{}\<[28]%
\>[28]{}\mathrel{=}\Varid{checkop}\;\Varid{op}\;((\Varid{checkop}\;\Varid{op}\;(\Varid{a},\Varid{b})),\Varid{c})\mathbin{:}\Varid{checkl}\;\Varid{xs}\;\Varid{op}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{25}{@{}>{\hspre}l<{\hspost}@{}}%
\column{38}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\Varid{checkop}{}\<[25]%
\>[25]{}\mathbin{::}\Conid{BinOp}\to \Conid{Input}\to \Conid{Bool}{}\<[E]%
\\
\>[3]{}\Varid{checkop}\;((\Varid{e},\Varid{r})\mathbin{:}\Varid{es})\;\Varid{p}{}\<[25]%
\>[25]{}\mid \Varid{e}==\Varid{p}{}\<[38]%
\>[38]{}\mathrel{=}\Varid{r}{}\<[E]%
\\
\>[25]{}\mid \Varid{otherwise}{}\<[38]%
\>[38]{}\mathrel{=}\Varid{checkop}\;\Varid{es}\;\Varid{p}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{24}{@{}>{\hspre}l<{\hspost}@{}}%
\column{28}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\Varid{checkr}{}\<[28]%
\>[28]{}\mathbin{::}[\mskip1.5mu (\Conid{Bool},\Conid{Bool},\Conid{Bool})\mskip1.5mu]\to \Conid{BinOp}\to [\mskip1.5mu \Conid{Output}\mskip1.5mu]{}\<[E]%
\\
\>[3]{}\Varid{checkr}\;[\mskip1.5mu \mskip1.5mu]\;{}\<[24]%
\>[24]{}\anonymous {}\<[28]%
\>[28]{}\mathrel{=}[\mskip1.5mu \mskip1.5mu]{}\<[E]%
\\
\>[3]{}\Varid{checkr}\;((\Varid{a},\Varid{b},\Varid{c})\mathbin{:}\Varid{xs})\;{}\<[24]%
\>[24]{}\Varid{op}{}\<[28]%
\>[28]{}\mathrel{=}\Varid{checkop}\;\Varid{op}\;(\Varid{a},(\Varid{checkop}\;\Varid{op}\;(\Varid{b},\Varid{c})))\mathbin{:}\Varid{checkr}\;\Varid{xs}\;\Varid{op}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
We can now evaluate all the possible outputs for the expression $(a{\oplus}b){\oplus}c$ by 
mapping the function \ensuremath{\Varid{checkl}\;\Varid{tinps}} over the list \ensuremath{\Varid{operators}}. Symmetrically, we can evaluate all
the possible outputs for the expression $a{\oplus}(b{\oplus}c)$ by mapping the function
\ensuremath{\Varid{checkr}\;\Varid{tinps}} over the list \ensuremath{\Varid{operators}}.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{9}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\Varid{expl}{}\<[9]%
\>[9]{}\mathbin{::}[\mskip1.5mu [\mskip1.5mu \Conid{Output}\mskip1.5mu]\mskip1.5mu]{}\<[E]%
\\
\>[3]{}\Varid{expl}{}\<[9]%
\>[9]{}\mathrel{=}\Varid{map}\;(\Varid{checkl}\;\Varid{tinps})\;\Varid{operators}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{9}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\Varid{expr}{}\<[9]%
\>[9]{}\mathbin{::}[\mskip1.5mu [\mskip1.5mu \Conid{Output}\mskip1.5mu]\mskip1.5mu]{}\<[E]%
\\
\>[3]{}\Varid{expr}{}\<[9]%
\>[9]{}\mathrel{=}\Varid{map}\;(\Varid{checkr}\;\Varid{tinps})\;\Varid{operators}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
We now want to filter all the operators that have exactly three {\sf true} output entries.
We start by defining the function \ensuremath{\Varid{fthree}} that tests if a given list of outputs has exactly
three {\sf true} elements.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{11}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\Varid{fthree}{}\<[11]%
\>[11]{}\mathbin{::}[\mskip1.5mu \Conid{Output}\mskip1.5mu]\to \Conid{Bool}{}\<[E]%
\\
\>[3]{}\Varid{fthree}{}\<[11]%
\>[11]{}\mathrel{=}(==\mathrm{3})\mathbin{\circ}\Varid{length}\mathbin{\circ}\Varid{filter}\;(==\Conid{True}){}\<[E]%
\ColumnHook
\end{hscode}\resethooks
We then map \ensuremath{\Varid{fthree}} over \ensuremath{\Varid{expl}} and \ensuremath{\Varid{expr}}.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\Varid{tmp1}\mathrel{=}\Varid{map}\;\Varid{fthree}\;\Varid{expl}{}\<[E]%
\\
\>[3]{}\Varid{tmp2}\mathrel{=}\Varid{map}\;\Varid{fthree}\;\Varid{expr}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
Now, using the next function, \ensuremath{\Varid{flist}}, we can combine the lists of booleans constructed
by \ensuremath{\Varid{tmp1}} and \ensuremath{\Varid{tmp2}} with the list \ensuremath{\Varid{operators}} to filter the operators we are interested in.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{10}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\Varid{flist}{}\<[10]%
\>[10]{}\mathbin{::}[\mskip1.5mu \Conid{Bool}\mskip1.5mu]\to [\mskip1.5mu \Conid{BinOp}\mskip1.5mu]\to [\mskip1.5mu \Conid{BinOp}\mskip1.5mu]{}\<[E]%
\\
\>[3]{}\Varid{flist}{}\<[10]%
\>[10]{}\mathrel{=}(\Varid{map}\;\Varid{snd}\mathbin{\circ})\mathbin{\circ}(\Varid{filter}\;\Varid{fst}\mathbin{\circ})\mathbin{\circ}\Varid{zip}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
And so, the only operators that are of interest are:
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{8}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\Varid{opl}{}\<[8]%
\>[8]{}\mathbin{::}[\mskip1.5mu \Conid{BinOp}\mskip1.5mu]{}\<[E]%
\\
\>[3]{}\Varid{opl}{}\<[8]%
\>[8]{}\mathrel{=}\Varid{flist}\;\Varid{tmp1}\;\Varid{operators}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{8}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\Varid{opr}{}\<[8]%
\>[8]{}\mathbin{::}[\mskip1.5mu \Conid{BinOp}\mskip1.5mu]{}\<[E]%
\\
\>[3]{}\Varid{opr}{}\<[8]%
\>[8]{}\mathrel{=}\Varid{flist}\;\Varid{tmp2}\;\Varid{operators}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
For all the operators $\oplus$ in \ensuremath{\Varid{opl}}, we know that $(a{\oplus}b){\oplus}c$
returns exactly three {\sf true} values. Symmetrically, we also know that
for all the operators $\oplus$ in \ensuremath{\Varid{opr}}, $a{\oplus}(b{\oplus}c)$ returns
exactly three {\sf true} values. 

It remains to check if these three {\sf true}
values correspond to exactly when one of the arguments is {\sf true}.
We create a list with the three input combinations where exactly one
is {\sf true}.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\Varid{oneistrue}\mathrel{=}[\mskip1.5mu (\Conid{True},\Conid{False},\Conid{False}),(\Conid{False},\Conid{True},\Conid{False}),(\Conid{False},\Conid{False},\Conid{True})\mskip1.5mu]{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
Finally, using the operators in \ensuremath{\Varid{opl}} and \ensuremath{\Varid{opr}}, we determine if these
inputs evaluate to {\sf true}.
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{12}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\Varid{resultl}{}\<[12]%
\>[12]{}\mathbin{::}\Conid{Bool}{}\<[E]%
\\
\>[3]{}\Varid{resultl}{}\<[12]%
\>[12]{}\mathrel{=}\Varid{and}\mathbin{\$}\Varid{map}\;\Varid{and}\mathbin{\$}\Varid{map}\;(\Varid{checkl}\;\Varid{oneistrue})\;\Varid{opl}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
\begin{hscode}\SaveRestoreHook
\column{B}{@{}>{\hspre}l<{\hspost}@{}}%
\column{3}{@{}>{\hspre}l<{\hspost}@{}}%
\column{12}{@{}>{\hspre}l<{\hspost}@{}}%
\column{E}{@{}>{\hspre}l<{\hspost}@{}}%
\>[3]{}\Varid{resultr}{}\<[12]%
\>[12]{}\mathbin{::}\Conid{Bool}{}\<[E]%
\\
\>[3]{}\Varid{resultr}{}\<[12]%
\>[12]{}\mathrel{=}\Varid{and}\mathbin{\$}\Varid{map}\;\Varid{and}\mathbin{\$}\Varid{map}\;(\Varid{checkr}\;\Varid{oneistrue})\;\Varid{opr}{}\<[E]%
\ColumnHook
\end{hscode}\resethooks
As the following snippet shows, both \ensuremath{\Varid{resultl}} and \ensuremath{\Varid{resultr}} evaluate to {\sf false}. 
We can thus conclude that there is not any boolean binary operator that can be quantified over an 
arbitrary set of values to express that exactly one of them is $\sf{true}$. 

\medskip
\indent\prompt{resultl}\\
\indent\ensuremath{\Conid{False}}\\
\indent\prompt{resultr}\\
\indent\ensuremath{\Conid{False}}


\bibliographystyle{plain}
\bibliography{math,jff,bibliogr}
\end{document}