% Filename: Lambda.sty % Author: Alan Jeffrey % Last modified: 12 Feb 1990 % % This style is (c) 1990 Alan Jeffrey. Permission is granted to make % copies, as long as % % a) no deletions are made, % % b) all additions are clearly marked, in amongst all this header information, % *and* where the addition has been made, and % % c) if you make any additions, then change the name of the file % % See the Gnu manifesto for details on why software ought to be free. % % If you are worrying about the first three clauses, they're just % there to make sure tons of different styles with the same name % don't proliferate. If you want to remove a definition, then just % comment it out (adding a %, not deleting anything). % % Tugboat are given permission to publish any or all of this. % % This style provides a pile of lambda-calculus and list-handling % macros of an incredibly obtuse nature. Read Lambda.tex to find out % what they all do and how they do it. This \TeX\ code was formally % verified. % % Alan Jeffrey, 25 Jan 1990. \def\Identity#1{#1} \def\Error% {\errmessage{Abandon verification all ye who enter here}} \def\First#1#2{#1} \def\Second#1#2{#2} \def\Compose#1#2#3{#1{#2{#3}}} \def\Twiddle#1#2#3{#1{#3}{#2}} \let\True=\First \let\False=\Second \let\Not=\Twiddle \def\And#1#2{#1{#2}\False} \def\Or#1#2{#1\True{#2}} \def\Lift#1#2#3#4{#1{#4}{#2}{#3}{#4}} \def\Lessthan#1#2{\TeXif{\ifnum#1<#2 }} \def\gobblefalse\else\gobbletrue\fi#1#2% {\fi#1} \def\gobbletrue\fi#1#2% {\fi#2} \def\TeXif#1% {#1\gobblefalse\else\gobbletrue\fi} \def\Nil#1#2{#2} \def\Cons#1#2#3#4{#3{#1}{#2}} \def\Stream#1{\Cons{#1}{\Stream{#1}}} \def\Singleton#1{\Cons{#1}\Nil} \def\Head#1{#1\First\Error} \def\Tail#1{#1\Second\Error} \def\Foldl#1#2#3% {#3{\Foldl@{#1}{#2}}{#2}} \def\Foldl@#1#2#3#4% {\Foldl{#1}{#1{#2}{#3}}{#4}} \def\Foldr#1#2#3% {#3{\Foldr@{#1}{#2}}{#2}} \def\Foldr@#1#2#3#4% {#1{#3}{\Foldr{#1}{#2}{#4}}} \def\Cat#1#2{\Foldr\Cons{#2}{#1}} \def\Reverse{\Foldl{\Twiddle\Cons}\Nil} \def\All#1{\Foldr{\Compose\And{#1}}\True} \def\Some#1{\Foldr{\Compose\Or{#1}}\False} \def\Isempty{\All{\First\False}} \def\Filter#1% {\Foldr{\Lift{#1}\Cons\Second}\Nil} \def\Map#1{\Foldr{\Compose\Cons{#1}}\Nil} \def\Insert#1#2#3% {#3{\Insert@{#1}{#2}}{\Singleton{#2}}} \def\Insert@#1#2#3#4% {#1{#2}{#3}% {\Cons{#2}{\Cons{#3}{#4}}}% {\Cons{#3}{\Insert{#1}{#2}{#4}}}} \def\Insertsort#1{\Foldr{\Insert{#1}}\Nil} \def\Unlistize#1{[#1\Unlistize@{}]} \def\Unlistize@#1{#1\Foldr\Commaize{}} \def\Commaize#1#2{, #1#2} \def\Listize[#1]% {\Listize@#1,\relax]} \def\Listize@#1,#2]% {\TeXif{\ifx\relax#2}% {\Singleton{#1}}% {\Cons{#1}{\Listize@#2]}}} \def\Show#1[#2]% {\Unlistize{#1{\Listize[#2]}}}