|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "dednat6/extra-modules.tex")
% (defun c () (interactive) (find-dednat6sh "lualatex -record extra-modules.tex"))
% (defun d () (interactive) (find-pdf-page "~/dednat6/extra-modules.pdf"))
% (defun e () (interactive) (find-dednat6 "extra-modules.tex"))
% (defun u () (interactive) (find-latex-upload-links "extra-modules"))
% (find-pdf-page "~/dednat6/extra-modules.pdf")
% (find-sh0 "cp -v ~/dednat6/extra-modules.pdf /tmp/")
% (find-sh0 "cp -v ~/dednat6/extra-modules.pdf /tmp/pen/")
% file:///home/edrx/dednat6/extra-modules.pdf
% file:///tmp/extra-modules.pdf
% file:///tmp/pen/extra-modules.pdf
% http://angg.twu.net/dednat6/extra-modules.pdf
%
% «.defs-co» (to "defs-co")
% «.defs-zha-tcg-ub» (to "defs-zha-tcg-ub")
% «.defs-squigbij» (to "defs-squigbij")
%
% «.LPicture» (to "LPicture")
% «.zfunctions» (to "zfunctions")
% «.ZHAs» (to "ZHAs")
% «.cuts» (to "cuts")
% «.TCGs» (to "TCGs")
% «.underbrace2d» (to "underbrace2d")
% «.luarects» (to "luarects")
%
\documentclass[oneside]{article}
\usepackage[colorlinks,urlcolor=DarkRed,citecolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage{graphicx}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%
% (find-dn6 "preamble6.lua" "preamble0")
\usepackage{proof} % For derivation trees ("%:" lines)
\input diagxy % For 2D diagrams ("%D" lines)
\xyoption{curve} % For the ".curve=" feature in 2D diagrams
%
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
% «defs-co» (to ".defs-co")
% \co: a low-level way to typeset code; a poor man's "\verb".
\def\co#1{{%
\def\%{\char37}%
\def\\{\char92}%
\def\^{\char94}%
\def\~{\char126}%
\tt#1%
}}
\def\qco#1{`\co{#1}'}
\def\qqco#1{``\co{#1}''}
\def\bsk{\bigskip}
\def\msk{\medskip}
\def\ssk{\smallskip}
% «defs-zha-tcg-ub» (to ".defs-zha-tcg-ub")
% From: (find-LATEX "2017planar-has-defs.tex" "defzha-and-deftcg")
\def\defzha#1#2{\expandafter\def\csname zha-#1\endcsname{#2}}
\def\ifzhaundefined#1{\expandafter\ifx\csname zha-#1\endcsname\relax}
\def\zha#1{\ifzhaundefined{#1}
\errmessage{UNDEFINED ZHA: #1}
\else
\csname zha-#1\endcsname
\fi
}
\def\deftcg#1#2{\expandafter\def\csname tcg-#1\endcsname{#2}}
\def\iftcgundefined#1{\expandafter\ifx\csname tcg-#1\endcsname\relax}
\def\tcg#1{\iftcgundefined{#1}
\errmessage{UNDEFINED TCG: #1}
\else
\csname tcg-#1\endcsname
\fi
}
\def\defub#1#2{\expandafter\def\csname ub-#1\endcsname{#2}}
\def\ifubundefined#1{\expandafter\ifx\csname ub-#1\endcsname\relax}
\def\ub#1{\ifubundefined{#1}
\errmessage{UNDEFINED UB: #1}
\else
\csname ub-#1\endcsname
\fi
}
\def\und#1#2{\underbrace{#1}_{#2}}
% «defs-squigbij» (to ".defs-squigbij")
% \squigbij: a nice "<--/\/\/\/-->" arrow drawn with pict2e.
% From: (find-LATEX "2017planar-has-defs.tex" "squigbij")
%
\def\squigbij{\newsquigbij}
\def\newsquigbij{\;\; \squigbijbody \;\;}
\def\squigbijy{-1.2}
\def\squigbijbody{\squigbijbodywithparams{1.5pt}{0.3pt}{1.0}}
\def\squigbijtriangle(#1,#2)#3{\polygon*(#1,0)(#2,#3)(#2,-#3)}
\def\squigbijbodywithparams#1#2#3{{%
\unitlength=#1
\linethickness{#2}
\begin{picture}(22.4,2.4)(-5.2,\squigbijy)%
\polyline(-3,0)(0,0)(1,1)(3,-1)(5,1)(7,-1)(9,1)(11,-1)(12,0)(14,0)
\squigbijtriangle(-5,-2){#3}
\squigbijtriangle(17,14){#3}
\end{picture}%
}}
% _____ _ _ _
% |_ _(_) |_| | ___
% | | | | __| |/ _ \
% | | | | |_| | __/
% |_| |_|\__|_|\___|
%
\title{Dednat6: extra modules}
\author{Eduardo Ochs}
\maketitle
% See:
% http://angg.twu.net/dednat6/extra-modules.txt.html
% http://angg.twu.net/dednat6/extra-modules.txt
% (find-dednat6 "extra-modules.txt")
% (find-dn6 "dednat6.lua")
% (find-dn6 "dednat6.lua" "requires" "picture")
% (find-dn6 "picture.lua")
% (find-dn6 "zhas.lua")
% (find-dn6 "zhas.lua" "MixedPicture")
The code of Dednat6 --- inside the directory \co{dednat6/} --- is made
of several \co{.lua} files that are {\sl all} loaded by
\co{dednat6.lua}; there is no provision yet for loading only the
modules that are used in a given \co{.tex} file. This means that some
modules that are only useful to the author of Dednat6 (Eduardo Ochs,
a.k.a. ``me'') are always loaded. Here is the part of the code of
\co{dednat6/dednat6.lua} that loads them:
\begin{verbatim}
-- Code for handling and drawing ZHAs:
require "picture" -- (find-dn6 "picture.lua")
require "zhas" -- (find-dn6 "zhas.lua")
require "zhaspecs" -- (find-dn6 "zhaspecs.lua")
require "tcgs" -- (find-dn6 "tcgs.lua")
require "luarects" -- (find-dn6 "luarects.lua")
\end{verbatim}
Most of these extra modules were written to handle the objects
described in my series of papers about ``Planar Heyting Algebras for
Children'', at:
\msk
\url{http://angg.twu.net/math-b.html#zhas-for-children-2}
\msk
Even though these modules are not useful to other people some ideas
and techniques in them may be. I am preparing a video to explain them
--- it will be based on the ``executable notes'' here:
\msk
\url{http://angg.twu.net/dednat6/extra-modules.txt}
\msk
I am preparing the ``script'' and rehearsing the video but I haven't
started recording yet. This PDF {\sl complements} the notes and the
video.
\msk
% _ ____ _ _
% | | | _ \(_) ___| |_ _ _ _ __ ___
% | | | |_) | |/ __| __| | | | '__/ _ \
% | |___| __/| | (__| |_| |_| | | | __/
% |_____|_| |_|\___|\__|\__,_|_| \___|
%
% «LPicture» (to ".LPicture")
% (find-dednat6 "dednat6/picture.lua" "makepicture")
% (find-dednat6 "dednat6/picture.lua" "LPicture")
% _________ _ __________ _ _
% |__ / ___| ___| |_ ___ |__ / ___| _ _ __ ___| |_(_) ___ _ __ ___
% / /\___ \ / _ \ __/ __| / /| |_ | | | | '_ \ / __| __| |/ _ \| '_ \/ __|
% / /_ ___) | __/ |_\__ \_ / /_| _|| |_| | | | | (__| |_| | (_) | | | \__ \
% /____|____/ \___|\__|___( ) /____|_| \__,_|_| |_|\___|\__|_|\___/|_| |_|___/
% |/
%
% «zfunctions» (to ".zfunctions")
% (find-LATEX "2017planar-has-1.tex" "positional")
% (find-LATEX "2017planar-has-1.tex" "positional" "house =")
\section{ZSets and ZFunctions}
% ______ _ _
% |__ / | | | / \ ___
% / /| |_| | / _ \ / __|
% / /_| _ |/ ___ \\__ \
% /____|_| |_/_/ \_\___/
%
% «ZHAs» (to ".ZHAs")
% (dnep 1 "ZHAs")
% (dne "ZHAs")
% (find-dednat6 "dednat6/zhas.lua" "ZHA-tests")
\section{ZHAs}
% ____ _
% / ___| _| |_ ___
% | | | | | | __/ __|
% | |__| |_| | |_\__ \
% \____\__,_|\__|___/
%
% «cuts» (to ".cuts")
% (find-dednat6 "dednat6/zhas.lua" "Cuts-tests")
\section{Cuts}
% _____ ____ ____
% |_ _/ ___/ ___|___
% | || | | | _/ __|
% | || |__| |_| \__ \
% |_| \____\____|___/
%
% «TCGs» (to ".TCGs")
% (dnep 1 "TCGs")
% (dne "TCGs")
% (find-dednat6 "dednat6/tcgs.lua")
\section{TCGs}
The file \co{tcgs.lua} defines classes for drawing the 2-column graphs
of [PH1] and [PH2] with or without question marks, and for converting
these 2CGs and 2CGQs into ZHAs and ZHAs with cuts. Here's an example
of what they produce:
%
%L tdims = TCGDims {qrh=5, q=15, crh=12, h=60, v=25, crv=7}
%L tspec_PA = TCGSpec.new("46; 11 22 34 45, 25")
%L tspec_PAQ = TCGSpec.new("46; 11 22 34 45, 25", ".???", "???.?.")
%L
%L -- Define $\tcg{(P,A)}$
%L -- and $\tcg{(P,A),Q}$.
%L -- The :tcgq() method uses the global variable tdims.
%L --
%L tspec_PA :tcgq({tdef="(P,A)", meta="1pt p"}, "lr q h v ap") :output()
%L tspec_PAQ:tcgq({tdef="(P,A),Q", meta="1pt p"}, "lr q h v ap") :output()
%L
%L -- Define $\zha{O_A(P)}$
%L -- and $\zha{O_A(P),J}$.
%L -- The :mp() method returns a MixedPicture object.
%L --
%L tspec_PA :mp ({zdef="O_A(P)"}) :addlrs():print() :output()
%L tspec_PAQ:mp ({zdef="O_A(P),J"}):addlrs():print() :output()
%L
\pu
$$
\begin{array}{ccc}
\tcg{(P,A)} &\squigbij& \zha{O_A(P)} \\ \\
\tcg{(P,A),Q} &\squigbij& \zha{O_A(P),J} \\
\end{array}
$$
Here's a figure showing how the dimension parameters in a TCGDims
object work.
\newpage
%L tspec = TCGSpec.new("23; 21, 13", "?.","..?")
%L
%L f = function (dims, name, actions)
%L tdims = TCGDims(dims)
%L TCGQ.newdsoa(tdims, tspec, {tdef=name, meta="1pt p"}, actions):output()
%L end
%L
%L f({h=20, v=20, q=20, crh=5, crv=5, qrh=5}, "A1", "B QB v h")
%L f({h=40, v=20, q=20, crh=5, crv=5, qrh=5}, "A2", "B QB v h")
%L f({h=40, v=20, q=40, crh=5, crv=5, qrh=5}, "A3", "B QB v h")
%L f({h=40, v=20, q=40, crh=10, crv=5, qrh=5}, "A4", "B QB v h")
%L f({h=40, v=20, q=40, crh=10, crv=5, qrh=10}, "A5", "B QB v h")
%L f({h=40, v=40, q=40, crh=10, crv=5, qrh=10}, "A6", "B QB v h")
%L f({h=40, v=40, q=40, crh=10, crv=10, qrh=10}, "A7", "B QB v h")
%L
%L tspec = TCGSpec.new("23; 21, 13")
%L f({h=40, v=40, q=40, crh=10, crv=10, qrh=10}, "A8", "B v h")
\pu
$$\def\T#1#2{
\begin{tabular}{l}
\{ #1, \\
\;\;\;#2\} \\
\end{tabular}
}
\scalebox{0.8}{$
\begin{array}{ccc}
\T{h=20, v=20, q=20} { crh=5, crv=5, qrh=5} &⇒& \tcg{A1} \\ \\
\T{h=40, v=20, q=20} { crh=5, crv=5, qrh=5} &⇒& \tcg{A2} \\ \\
\T{h=40, v=20, q=40} { crh=5, crv=5, qrh=5} &⇒& \tcg{A3} \\ \\
\T{h=40, v=20, q=40} {crh=10, crv=5, qrh=5} &⇒& \tcg{A4} \\ \\
\T{h=40, v=20, q=40} {crh=10, crv=5, qrh=10} &⇒& \tcg{A5} \\ \\
\T{h=40, v=40, q=40} {crh=10, crv=5, qrh=10} &⇒& \tcg{A6} \\ \\
\T{h=40, v=40, q=40} {crh=10, crv=10, qrh=10} &⇒& \tcg{A7} \\ \\
\T{h=40, v=40, q=40} {crh=10, crv=10, qrh=10} &⇒& \tcg{A8} \\
\end{array}
$}
$$
% _ _ _ _
% | | | |_ __ __| | ___ _ __| |__ _ __ __ _ ___ ___
% | | | | '_ \ / _` |/ _ \ '__| '_ \| '__/ _` |/ __/ _ \
% | |_| | | | | (_| | __/ | | |_) | | | (_| | (_| __/
% \___/|_| |_|\__,_|\___|_| |_.__/|_| \__,_|\___\___|
%
% «underbrace2d» (to ".underbrace2d")
% (find-LATEX "2019seminario-hermann.tex" "values-of-subexpressions-S4")
% Moved to: (find-dednat6 "demo-underbrace.tex")
\section{Underbrace2d}
%UB P \lor Q \to P \land Q
%UB - - - -
%UB 0 1 0 1
%UB -------- ---------
%UB 1 0
%UB ---------------------
%UB 0
%L
%L defub "PvQ -> PaQ"
$$\pu \ub{PvQ -> PaQ}
$$
% _ _
% | | _ _ __ _ _ __ ___ ___| |_ ___
% | | | | | |/ _` | '__/ _ \/ __| __/ __|
% | |__| |_| | (_| | | | __/ (__| |_\__ \
% |_____\__,_|\__,_|_| \___|\___|\__|___/
%
% «luarects» (to ".luarects")
% (find-LATEX "2019seminario-hermann.tex" "lattice-non-planar")
\section{Luarects}
% (find-dn6 "luarects.lua")
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-tla: "dnz"
% End: