% (find-angg "LATEX/2016-1-LA-material.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2016-1-LA-material.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2016-1-LA-material.pdf"))
% (defun e () (interactive) (find-LATEX "2016-1-LA-material.tex"))
% (defun l () (interactive) (find-LATEX "2016-1-LA-material.lua"))
% (defun u () (interactive) (find-latex-upload-links "2016-1-LA-material"))
% (defun z () (interactive) (find-zsh "flsfiles-tgz 2016-1-LA-material.fls 2016-1-LA-material.tgz"))
% (find-xpdfpage "~/LATEX/2016-1-LA-material.pdf")
% (find-sh0 "cp -v  ~/LATEX/2016-1-LA-material.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2016-1-LA-material.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2016-1-LA-material.pdf
%               file:///tmp/2016-1-LA-material.pdf
%           file:///tmp/pen/2016-1-LA-material.pdf
% http://angg.twu.net/LATEX/2016-1-LA-material.pdf

% «.composition»		(to "composition")
% «.typed-L1-trees»		(to "typed-L1-trees")

% «.expressions-and-reductions»	(to "expressions-and-reductions")
% «.vars-and-algebra»		(to "vars-and-algebra")
% «.lambda»			(to "lambda")
% «.function-graphs»		(to "function-graphs")
% «.classical-logic»		(to "classical-logic")
% «.3-valued-logic»		(to "3-valued-logic")
% «.represente-graficamente»	(to "represente-graficamente")
% «.tautologies»		(to "tautologies")
% «.comprehension»		(to "comprehension")
% «.elika»			(to "elika")
% «.inj-sobre-bij»		(to "inj-sobre-bij")
% «.pict2evector»		(to "pict2evector")


\documentclass[oneside]{book}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
\usepackage{pict2e}               % (find-es "tex" "pict2e")
% (find-angg ".emacs.papers" "latexgeom")
% \usepackage[a4paper, top=1cm, left=1cm]{geometry} 
\usepackage[a4paper, hmargin=2cm, vmargin=3cm]{geometry}
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{tikz}
%
\usepackage{proof}   % For derivation trees ("%:" lines)
\input diagxy        % For 2D diagrams ("%D" lines)
\xyoption{curve}     % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx15}               % (find-angg "LATEX/edrx15.sty")
\input edrxaccents.tex            % (find-angg "LATEX/edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex           % (find-dn4ex "edrxheadfoot.tex")
%
\begin{document}

\catcode`\^^J=10
\directlua{dednat6dir = "dednat6/"}
\directlua{dofile(dednat6dir.."dednat6.lua")}
\directlua{texfile(tex.jobname)}
\directlua{verbose()}
\directlua{output(preamble1)}
\def\expr#1{\directlua{output(tostring(#1))}}
\def\eval#1{\directlua{#1}}
\def\pu{\directlua{pu()}}

\edrxcolors
\def\bhbox{\bicolorhbox}

\directlua{dofile "edrxtikz.lua"} % (find-LATEX "edrxtikz.lua")
%L V.__tostring = function (v) return format("(%.3f,%.3f)", v[1], v[2]) end

\def\und#1#2{\underbrace{#1}_{#2}}
\def\und#1#2{\underbrace{#1}_{\textstyle #2}}
\def\subf#1{\underbrace{#1}_{}}
\def\p{\phantom{(}}

\def\cur{\operatorname{cur}}
\def\uncur{\operatorname{uncur}}
\def\app{\operatorname{app}}
\def\ren{\operatorname{ren}}

\def∧{\&}

\def\namedfunction#1#2#3#4#5{
  \begin{array}{rrcl}
    #1: & #2 & → & #3 \\
        & #4 & ↦ & #5 \\
  \end{array}
  }




%                                      _ _   _             
%   ___ ___  _ __ ___  _ __   ___  ___(_) |_(_) ___  _ __  
%  / __/ _ \| '_ ` _ \| '_ \ / _ \/ __| | __| |/ _ \| '_ \ 
% | (_| (_) | | | | | | |_) | (_) \__ \ | |_| | (_) | | | |
%  \___\___/|_| |_| |_| .__/ \___/|___/_|\__|_|\___/|_| |_|
%                     |_|                                  
%
% «composition» (to ".composition")

Composition

(is associative)

%L mapstos_1 = function (str)
%L     local n, latex = 0, ""
%L     for d in str:gmatch("%d") do
%L       latex = latex .. format("%d \\mapsto %d \\\\\n", n, d)
%L       n = n + 1
%L     end
%L     return latex
%L   end
%L 
%L mapstos_2 = function (str)
%L     local latex = ""
%L     for a,b in str:gmatch("(%d)(%d)") do
%L       latex = latex .. format("%d \\mapsto %d \\\\\n", a, b)
%L     end
%L     return latex
%L   end
\pu

\def\mapsb #1{\sm{\expr{mapstos_1("#1")}}}
\def\mapsab#1{\sm{\expr{mapstos_2("#1")}}}

% \bsk

%D diagram ??
%D 2Dx     100   +35   +35  +35   +35   +35  
%D 2D  100 A --> B          a --> b          
%D 2D            |                |          
%D 2D            v                v          
%D 2D  +35       C --> D          c --> d    
%D 2D
%D ren  a b     ==>  \{1,2\} \{3,4\}
%D ren    c d   ==>          \{5,6\} \{7,8\} 
%D (( A B -> .plabel= a f
%D    B C -> .plabel= m g
%D    C D -> .plabel= b h
%D    A C -> .plabel= l (g∘f=)\;\;f;g
%D    B D -> .plabel= r g;h\;\;(=h∘g)
%D    
%D    a b -> .plabel= a \mapsab{13,24}
%D    b c -> .plabel= m \mapsab{36,45}
%D    c d -> .plabel= b \mapsab{57,67}
%D    a c ->  b d ->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

\bsk

%D diagram composition-1
%D 2Dx     100   +30   +30   +30
%D 2D  100 D <-- C <-- B <-- A
%D 2D
%D (( D A <- .plabel= a (h∘g)∘f .slide= 22pt
%D    D B <- .plabel= a  h∘g    .slide= 10pt
%D    D C <- .plabel= m h   C B <- .plabel= m g  B A <- .plabel= m f
%D    C A <- .plabel= b    g∘f  .slide= -10pt
%D    D A <- .plabel= b h∘(g∘f) .slide= -22pt
%D ))
%D enddiagram
%D
%
$$\begin{array}{rcl}
  ((h∘g)∘f)(a) &=& (h∘g)(f(a)) \\
               &=& h(g(f(a))) \\
               &=& h((g∘f)(a)) \\
               &=& (h∘(g∘f))(a) \\[5pt]
  ((h∘g)∘f)(a) &=& (h∘(g∘f))(a) \\[5pt]
  (h∘g)∘f &=& h∘(g∘f) \\
  \end{array}
  \qquad
  \Diag{composition-1}
$$


\bsk
\bsk

Identities:

If $f:A→B$ then $\id_A;f = f = f;\id_B$ 

%D diagram ??
%D 2Dx     100   +35   +35  +35   +35   +35  
%D 2D  100 A --> B          a --> b          
%D 2D            |                |          
%D 2D            v                v          
%D 2D  +35       C --> D          c --> d    
%D 2D
%D ren  A B     ==>  A  A
%D ren    C D   ==>     B  B
%D ren  a b     ==>  \{1,2\} \{1,2\}
%D ren    c d   ==>          \{3,4\} \{3,4\} 
%D (( A B -> .plabel= a \id_A
%D    B C -> .plabel= m f
%D    C D -> .plabel= b \id_B
%D    A C -> .plabel= l f\;=\;\id_A;f
%D    B D -> .plabel= r f;\id_B\;=\;f
%D    
%D    a b -> .plabel= a \mapsab{11,22}
%D    b c -> .plabel= m \mapsab{13,24}
%D    c d -> .plabel= b \mapsab{33,44}
%D    a c ->  b d ->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

\bsk
\bsk

A theorem about lateral inverses:

If $f;g = \id$ and $g;h=\id$ then $f=h$

%D diagram ??
%D 2Dx     100   +35   +35  +35   +35   +35  
%D 2D  100 A --> B          a --> b          
%D 2D            |                |          
%D 2D            v                v          
%D 2D  +35       C --> D          c --> d    
%D 2D
%D ren  A B     ==>  B  A
%D ren    C D   ==>     B  A
%D ren  a b     ==>  \{1,2\} \{1,2\}
%D ren    c d   ==>          \{3,4\} \{3,4\} 
%D (( A B -> .plabel= a f
%D    B C -> .plabel= m g
%D    C D -> .plabel= b h
%D    A C -> .plabel= l \id_B\;=\;f;g
%D    B D -> .plabel= r \id_A\;=\;g;h
%D    
%D #   a b -> .plabel= a \mapsab{11,22}
%D #   b c -> .plabel= m \mapsab{13,24}
%D #   c d -> .plabel= b \mapsab{33,44}
%D #   a c ->  b d ->
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
  \qquad
  \begin{array}{rcl}
  \multicolumn {3}{c} {(f;g);h = \id_B;h = h} \\
  \multicolumn {3}{c} {f;(g;h) = f;\id_A = f} \\[5pt]
  f &=& f;\id_A \\
    &=& f;(g;h) \\
    &=& (f;g);h \\
    &=& \id_B;h \\
    &=& h
  \end{array}
$$



\newpage

Multiple inverses

%L forths["->>"] = function () pusharrow("->>") end

%D diagram ??
%D 2Dx     100   +35   +35   +35
%D 2D  100 A --> B     D
%D 2D            |     |
%D 2D            v     v
%D 2D  +35       C     E --> F
%D 2D
%D ren  A B  D     ==> \{1,2\} \{3,4,5\}   \{5,6\}
%D ren    C  E F   ==>          \{1,2\}   \{7,8,9\} \{5,6\}
%D (( A B >-> sl^ .plabel= a ?  A B >-> sl_ .plabel= b ?
%D    B C ->> .plabel= r \mapsab{31,42,52}
%D    A C  -> .plabel= l \id
%D
%D    D E ->> .plabel= l \mapsab{57,68}
%D    E F >-> sl^ .plabel= a ? E F >-> sl_ .plabel= b ?
%D    D F  -> .plabel= r \id
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

\bsk
\bsk

\def\frown{=(}

No inverses

%D diagram ??
%D 2Dx     100   +35   +35  +10   +35   +35
%D 2D  100 A --> B          E --> F
%D 2D            |                |
%D 2D            v                v
%D 2D  +35       C --> D          G --> H
%D 2D
%D ren  A B    E F     ==> \{3,4,5\} \{1,2\}           \{8,9\} \{5,6,7\}
%D ren    C D    G H   ==>          \{3,4,5\} \{1,2\}           \{8,9\} \{5,6,7\}
%D (( A B  -> .plabel= a \frown
%D    B C >-> .plabel= m \mapsab{13,24}
%D    A C  -> .plabel= l \id
%D    C D ->> sl^ C D ->> sl_
%D    B D -> .plabel= r \id
%D
%D    E G  -> .plabel= l \id
%D    E F >-> sl^ E F >-> sl_
%D    F G ->> .plabel= m \mapsab{58,69,79}
%D    G H  -> .plabel= b \frown
%D    F H  -> .plabel= r \id
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$

%D diagram ??
%D 2Dx     100   +35   +35
%D 2D  100 A --> B
%D 2D            |
%D 2D            v
%D 2D  +35       C --> D
%D 2D
%D ren  A B     ==> \{4,5,6\} \{1,2,3\}
%D ren    C D   ==>           \{4,5,6\} \{1,2,3\} 
%D (( A B -> .plabel= a \frown
%D    B C -> .plabel= m \mapsab{14,25,35}
%D    C D -> .plabel= r \frown
%D    A C -> .plabel= l \id
%D    B D -> .plabel= r \id
%D ))
%D enddiagram
%D
$$\pu
  \diag{??}
$$


\bsk
\bsk
\bsk

{\bf Products}

Property: $∀f,g.∃!h.(f=h;π\;∧\;g=h;π')$

Solution: $h=λa:A.(f(a),g(a))$

Bijection: $(f,g)↔h$

$(→)$: $λ(f,g).(λa:A.(f(a),g(a)))$

$(←)$: $λh.((h;π),(h;π'))$

\bsk


%D diagram product-ABC
%D 2Dx     100    +45    +45
%D 2D  100        A
%D 2D             |
%D 2D             v
%D 2D  +45 B <-- BxC --> C
%D 2D
%D ren    A      ==>    A
%D ren B BxC C   ==> B B×C C
%D
%D (( A  B  -> .plabel= l f
%D    A BxC -> .plabel= m h
%D    A  C  -> .plabel= r g
%D    B BxC <- .plabel= b π\mathstrut
%D    BxC C -> .plabel= b π'
%D ))
%D enddiagram
%D
%D diagram product-explicit
%D 2Dx     100    +45    +45
%D 2D  100        A
%D 2D             |
%D 2D             v
%D 2D  +45 B <-- BxC --> C
%D 2D
%D ren    A      ==>                      \{1,2\}
%D ren B BxC C   ==> \{3,4\}  \csm{(3,5),(3,6),\\(4,5),(4,6)}  \{5,6\} 
%D
%D (( A  B  -> .plabel= l \mapsab{13,24}
%D    A BxC -> .plabel= m \midmap
%D    A  C  -> .plabel= r \mapsab{15,26}
%D    B BxC <- .plabel= b π\mathstrut
%D    BxC C -> .plabel= b π'
%D ))
%D enddiagram
%D
$$\pu
  \def\midmap{\sm{1↦(3,5)\\2↦(4,6)}}
  %
  \diag{product-ABC}
  \qquad
  \diag{product-explicit}
$$




\newpage

{\bf Exponentials}

Bijection: $f↔g$

$(→)$ (``currying''): $g := \cur f := λa:A.λb:B.f(a,b)$

$(←)$ (``uncurrying''): $f := \uncur g := λ(a,b):A×B.((g(a))(b))$

\bsk

%D diagram exponentials-ABC
%D 2Dx      100     +45
%D 2D  100 AxB <--| A
%D 2D       |       |
%D 2D       |  <->  |
%D 2D       v       v
%D 2D  +50  C |--> B->C
%D 2D
%D ren AxB A    ==>  A×B  A
%D ren C B->C   ==>   C  B{→}C
%D (( AxB A  <-| .plabel= a λA.(A×B)
%D    C B->C |-> .plabel= b λC.(B{→}C)
%D    AxB C   -> .plabel= l f
%D    A B->C  -> .plabel= r g
%D    A C  harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
%D diagram exponentials-explicit
%D 2Dx      100     +60
%D 2D  100 AxB <--| A
%D 2D       |       |
%D 2D       |  <->  |
%D 2D       v       v
%D 2D  +50  C |--> B->C
%D 2D
%D ren AxB A    ==> \csm{(1,3),(1,4)\\(2,3),(2,4)}  \{1,2\}
%D ren C B->C   ==> \{5,6\} \csm{\fu55,\fu56,\\\fu65,\fu66}
%D (( AxB A <-|
%D    C B->C |->
%D    AxB C   -> .plabel= l \sm{(1,3)↦5\\(1,4)↦6\\(2,3)↦6\\(2,4)↦5}
%D    A B->C  -> .plabel= r \sm{1↦\fu56\\2↦\fu65}
%D    A C  harrownodes nil 20 nil <->
%D ))
%D enddiagram
%D
$$\pu
  \def\fu#1#2{\csm{(3,#1),\\(4,#2)}}
  \diag{exponentials-ABC}
  \diag{exponentials-explicit}
$$


\bsk
\bsk

Properties: $\cur \uncur f = f$, \; $\uncur \cur g = g$

where: $f×f' := \ang{π;f,\,π';f'}$, \; $\uncur g := (g×\id);\ev$

solving type equations:

\bsk

%:" 
%:
%:
%:  π   f    π'  f'     π:A×?→A   f:A→B     π':?×A'→A'  f':A'→B' 
%:  -----    ------    ------ ------------    ---------------------
%:   π;f     π';f'      π;f:A×?→B                π';f':?×A'→B'     
%:  ----------------     ---------------------------------------- 
%:  \ang{π;f,\,π';f'}        \ang{π;f,\,π';f'}:A×A'→B×B'
%:  ------------------\ren    ----------------------------\ren
%:       f×f'                      f×f':A×A'→B×B'
%:
%:       ^fxf'_1                    ^fxf'_2
%:
%:
%:  g  \id           g:A→(B{→}C)  \id:?→?     
%:  ------           ----------------------     
%:  g×\id   \ev      g×\id:A×?→(B{→}C)×?    \ev:(B{→}C)×B→C
%:  -----------      -----------------------------------------
%:  (g×\id);\ev                (g×\id);\ev:A×?→C
%:  -----------\ren            ------------------
%:    \uncur"g                     \uncur"g:A×?→C
%:
%:    ^uncur_g_1                   ^uncur_g_2
%:
\pu
$$\ded{fxf'_1} \qquad \ded{fxf'_2}$$

$$\ded{uncur_g_1} \qquad \ded{uncur_g_2}$$



\newpage



%  _                 _         _         _                      
% | | __ _ _ __ ___ | |__   __| | __ _  | |_ _ __ ___  ___  ___ 
% | |/ _` | '_ ` _ \| '_ \ / _` |/ _` | | __| '__/ _ \/ _ \/ __|
% | | (_| | | | | | | |_) | (_| | (_| | | |_| | |  __/  __/\__ \
% |_|\__,_|_| |_| |_|_.__/ \__,_|\__,_|  \__|_|  \___|\___||___/
%                                                               
% «typed-L1-trees» (to ".typed-L1-trees")

Typed $λ$-calculus: trees

\msk

$\begin{array}{l}
A = \{1,2\} \\
B = \{3,4\} \\
C = \{30,40\} \\
A×B = \cmat{(1,3),(1,4),\\(2,3),(2,4)} \\
B→C = \cmat{
  \csm{(3,30),\\(4,30)},
  \csm{(3,30),\\(4,40)},
  \csm{(3,40),\\(4,30)},
  \csm{(3,40),\\(4,40)}\\
} \\
\end{array}
$

\bsk

%:
%:            (a,b)                   (2,3)
%:            -----π'                 -----π'
%:   (a,b)      b      f       (2,3)    3      \cmat{(3,30),(4,40)}
%:   -----π    --------app     -----π  --------------------------app
%:     a         f(b)            2              30
%:     --------------pair        -----------------pair
%:        (a,f(b))                  (2,30)
%:
%:        ^idxf1                    ^idxf2
%:
\pu
$$\ded{idxf1} \qquad \ded{idxf2}$$

%:
%:               (a,b):A×B                             p:A×B               
%:               ---------π'                           -----π'             
%:   (a,b):A×B      b:B       f:B→C        p:A×B       π'p:B       f:B→C      
%:   ---------π     ---------------app     ------π     ----------------app   
%:       a:A             f(b):C              πp:A            f(π'p):C          
%:       ----------------------pair          ----------------------pair      
%:              (a,f(b)):A×C                      (πp,f(π'p)):A×C             
%:                                                                             
%:              ^idxf3                             ^idxf4                     
%:
%:
%:              p:A×B                  
%:              -----π'                
%:  p:A×B       π'p:B       f:B→C      
%:  ------π     ----------------app    
%:    πp:A            f(π'p):C         
%:    ----------------------pair       
%:         (πp,f(π'p)):A×C 
%:      -----------------------
%:      (λp:A×B.(πp,f(π'p))):A×B→A×C 
%:                                     
%:          ^idxf5                    
\pu
% $$\ded{idxf3} \qquad \ded{idxf4}$$

$$\ded{idxf3}$$

$$\ded{idxf4}$$

$$\ded{idxf5}$$

\bsk

$(λp:A×B.(πp,f(π'p))) = \csm{
  ((1,3),(1,30)), \\
  ((1,4),(1,40)), \\
  ((2,3),(2,30)), \\
  ((2,4),(2,40)) \\
}$

\bsk

Exercícios:

Sejam $D = \{10,20\}$, $g = \csm{(1,20),\\(2,20)}$ (obs: $g:A→D$).

a) Seja $p = (2,3)$. Calcule $(g(πp),f(π'p))$.

b) Verifique que $(g(πp),f(π'p)):D×C$.

c) Calcule $(λp:A×B.(g(πp),f(π'p))):A×B→D×C$.



\newpage



%  ____       _____           _  _       ____  
% |___ \__  _|___ /     _    | || |__  _| ___| 
%   __) \ \/ / |_ \   _| |_  | || |\ \/ /___ \ 
%  / __/ >  < ___) | |_   _| |__   _>  < ___) |
% |_____/_/\_\____/    |_|      |_|/_/\_\____/ 
%                                              
% «expressions-and-reductions» (to ".expressions-and-reductions")

Expressions (and reductions)

\bsk

% Ways of calculating $2·3+4·5$

%D diagram 2x4+4x5
%D 2Dx     100  +50  +40
%D 2D  100 A    B
%D 2D
%D 2D  +30 C    D    E
%D 2D
%D ren  A  B      ==>   2·3+4·5   2·3+20
%D ren  C  D  E   ==>     6+4·5     6+20  26
%D (( A B ->   A C -> B D ->
%D    C D ->   D E ->
%D ))
%D enddiagram
%D
\pu
$$\diag{2x4+4x5}$$
\bsk
$$\mat{\und{\und{2·3}{6} + \und{4·5}{20}}{26}}
  \qquad
  \qquad
  \begin{array}[c]{rclcrcl}
  2·3+4·5 &=& 2·3+20 \\
          &=& 6+20   \\
          &=& 26     \\
                     \\
  2·3+4·5 &=& 6+4·5  \\
          &=& 6+20   \\
          &=& 26     \\
  \end{array}
$$

\bsk

Subexpressions:

$% \subf{2·3}+\subf{4·5}
 % \qquad
 \subf{\subf{\subf{2}·\subf{3}} +
       \subf{\subf{4}·\subf{5}}
      }
$

% \bsk
\newpage


% __     __                ___           _            _               
% \ \   / /_ _ _ __ ___   ( _ )     __ _| | __ _  ___| |__  _ __ __ _ 
%  \ \ / / _` | '__/ __|  / _ \/\  / _` | |/ _` |/ _ \ '_ \| '__/ _` |
%   \ V / (_| | |  \__ \ | (_>  < | (_| | | (_| |  __/ |_) | | | (_| |
%    \_/ \__,_|_|  |___/  \___/\/  \__,_|_|\__, |\___|_.__/|_|  \__,_|
%                                          |___/                      
%
% «vars-and-algebra» (to ".vars-and-algebra")

Expressions with variables:

\msk

$\begin{array}{l}
    \text{If $a=5$ and $b=2$, then:} \\[5pt]
    \und{(\und{\und{a}{5} + \und{b}{2}}{7}) ·
         (\und{\und{a}{5} - \und{b}{2}}{3} )
         }{21} \\
  \end{array}
  %
  \qquad
  %
  \begin{array}{l}
    \text{If $a=10$ and $b=1$, then:} \\[5pt]
    \und{(\und{\und{a}{10} + \und{b}{1}}{11}) ·
         (\und{\und{a}{10} - \und{b}{1}}{9} )
         }{99} \\
  \end{array}
$

\bsk
\bsk

We know -- by algebra, which is not for (tiny) children --

that $(a+b)·(a-b) = a·a - b·b$ is true for all $a,b∈\R$

We know -- without algebra -- how to test

``$(a+b)·(a-b) = a·a - b·b$''

for specific values of $a$ and $b$...

\bsk

$\begin{array}{l}
    \text{If $a=5$ and $b=2$, then:} \\[5pt]
    \und{
      \und{(\und{\und{a}{5} + \und{b}{2}}{7}) ·
           (\und{\und{a}{5} - \und{b}{2}}{3})
           }{21}
      =
      \und{\und{\und{a}{5} · \und{a}{5}}{25} -
           \und{\und{b}{2} · \und{b}{2}}{4}
          }{21}
    }{\text{true}} \\
  \end{array}
$

\msk

$\begin{array}{l}
    \text{If $a=10$ and $b=1$, then:} \\[5pt]
    \und{
      \und{(\und{\und{a}{10} + \und{b}{1}}{11}) ·
           (\und{\und{a}{10} - \und{b}{1}} {9})
           }{99}
      =
      \und{\und{\und{a}{10} · \und{a}{10}}{100} -
           \und{\und{b}{1} · \und{b}{1}}{1}
          }{99}
    }{\text{true}} \\
  \end{array}
$

\newpage

%  _                    _         _       
% | |    __ _ _ __ ___ | |__   __| | __ _ 
% | |   / _` | '_ ` _ \| '_ \ / _` |/ _` |
% | |__| (_| | | | | | | |_) | (_| | (_| |
% |_____\__,_|_| |_| |_|_.__/ \__,_|\__,_|
%                                         
% «lambda» (to ".lambda")

% \bsk


A named function: $g(a) = a·a+4$

An unnamed function: $λa.\,a·a+4$

Let $h = λa.\,a·a+4$.

Then:



%D diagram reduce-g
%D 2Dx     100 +30 +30
%D 2D  100 A ----> B
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 C ----> D
%D 2D      |       |
%D 2D      v       |
%D 2D  +20 E       |
%D 2D      | \     |
%D 2D      |  v    |
%D 2D  +20 |   F   |
%D 2D      |    \  |
%D 2D      v     v v
%D 2D  +20 G ----> H
%D 2D              |
%D 2D              v
%D 2D  +20         I
%D 2D              |
%D 2D              v
%D 2D  +20         J
%D 2D
%D ren  A  B  ==>  g(2+3)       g(5)
%D ren  E  F  ==>  (2+3)·(2+3)+4  (2+3)·5+4
%D ren  G  H  ==>  5·(2+3)+4       5·5+4
%D ren  I  J  ==>  25+4            29
%D (( A B ->   E F -> F H ->   G H ->
%D    A E -> E G ->            B H -> H I -> I J ->
%D ))
%D enddiagram
%D
% $$\Diag{reduce-g}$$

%D diagram reduce-h
%D 2Dx     100 +35 +35
%D 2D  100 A ----> B
%D 2D      |       |
%D 2D      v       v
%D 2D  +20 C ----> D
%D 2D      |       |
%D 2D      v       |
%D 2D  +20 E       |
%D 2D      | \     |
%D 2D      |  v    |
%D 2D  +20 |   F   |
%D 2D      |    \  |
%D 2D      v     v v
%D 2D  +20 G ----> H
%D 2D              |
%D 2D              v
%D 2D  +20         I
%D 2D              |
%D 2D              v
%D 2D  +20         J
%D 2D
%D ren  A  B  ==>  h(2+3)       h(5)
%D ren  C  D  ==>  (λa.\,a·a+4)(2+3) (λa.\,a·a+4)(5)
%D ren  E  F  ==>  (2+3)·(2+3)+4  (2+3)·5+4
%D ren  G  H  ==>  5·(2+3)+4       5·5+4
%D ren  I  J  ==>  25+4            29
%D (( A B ->   C D ->   E F -> F H ->   G H ->
%D    A C ->   C E -> E G ->     B D -> D H -> H I -> I J ->
%D ))
%D enddiagram
%D
$$\Diag{reduce-g}
  \qquad
  \Diag{reduce-h}$$


\bsk

% TODO
% (find-istfile "1.org" "Defining named functions")
% (find-istfile "1.org" "defining unnamed functions")

The usual notation for defining functions is like this:

$$\begin{array}{rrcl}
 f: & \N & → & \R \\
    & n & ↦ & 2+\sqrt{n} \\
 \end{array}
$$


$$\def\t#1{\text{(#1)}}
 \begin{array}{rrcl}
 \t{name}: & \t{domain} & → & \t{codomain} \\
           & \t{variable} & ↦ & \t{expression} \\
 \end{array}
$$

It creates {\sl named} functions

(with domains and codomains).

\msk

The usual notation for creating named functions

without specifying their domains and codomains

is just $f(n) = 2+\sqrt{n}$.

\newpage



%   __                  _   _                                     _         
%  / _|_   _ _ __   ___| |_(_) ___  _ __     __ _ _ __ __ _ _ __ | |__  ___ 
% | |_| | | | '_ \ / __| __| |/ _ \| '_ \   / _` | '__/ _` | '_ \| '_ \/ __|
% |  _| |_| | | | | (__| |_| | (_) | | | | | (_| | | | (_| | |_) | | | \__ \
% |_|  \__,_|_| |_|\___|\__|_|\___/|_| |_|  \__, |_|  \__,_| .__/|_| |_|___/
%                                           |___/          |_|              
%
% «function-graphs» (to ".function-graphs")

The {\sl graph} of

$$\begin{array}{rrcl}
 h: & \{-2,-1,0,1,2\} & → & \{0,1,2,3,4\} \\
    & k & ↦ & k^2 \\
 \end{array}
$$

is $\{(-2,4),(-1,1),(0,0),(1,1),(2,4)\}$.

\bsk

We will think that a function {\sl is} its graph.

Then $h = \{(-2,4),(-1,1),(0,0),(1,1),(2,4)\}$

and $h(-2) = \{(-2,4),(-1,1),(0,0),(1,1),(2,4)\}(-2) = 4.$

\bsk

Let $h := (λk:\{-2,-1,0,1,2\}.k^2)$.

We have:

%D diagram reduce-k2-with-domain
%D 2Dx     100    +70   +70
%D 2D  100 A ---> B --> C 
%D 2D             |     |
%D 2D             v     v
%D 2D  +35        D --> E
%D 2D             |     |
%D 2D             v     v
%D 2D  +45        F --> G
%D 2D
%D ren  A  B  C   ==>   h(-2)   (λk:\{-2,-1,0,1,2\}.k^2)(-2)    ?
%D ren     D  E   ==>                     \grapha             (-2)^2
%D ren     F  G   ==>                     \graphb              4
%D (( A B -> B E ->
%D           B D -> # C E ->
%D           D E ->
%D           D F -> E G ->
%D           F G ->
%D ))
%D enddiagram
%D
\pu
$$\def\grapha{\csm{(-2,(-2)^2),\\(-1,(-1)^2),\\(0,0^2),\\(1,1^2),\\(2,2^2)}(-2)}
  \def\graphb{\csm{(-2,4),\\(-1,1),\\(0,0),\\(1,1),\\(2,4)}(-2)}
  \diag{reduce-k2-with-domain}
$$





% \end{document}

% The usual notation for defining functions is like this:
% 
%   f: N -> R                      (*)
%      n |-> 2+sqrt(n)
% 
%   name: domain -> codomain
%         variable |-> expression
% 
% It creates _named_ functions.
% 
% To use this notation we have to fill up five slots,
% and use a ":", an "->" and a "|->" in the right places.
% 
% After stating (*) we can "reduce" expressions with f, like this:
% 
%   f(4+5) ---> 2+sqrt(4+5)
%     :            :
%     :            :
%     v            v
%    f(9) ---> 2+sqrt(9) ---> 2+3 ---> 5
% 
% ** DONE $λ$-calculus: defining unnamed functions
% 
% Now compare
% 
%   name: domain -> codomain
%         variable |-> expression   name = \variable.expression
% 
%   g: N  -> R
%      a |-> a*a+4                    h = \a.a*a+4
% 
%   g(2+3) -----------> g(5)   h(2+3) ------------> h(5)
%     |                   |      |                   |
%     |                   |      v                   v
%     |                   |  (\a.a*a+4)(2+3) ---> (\a.a*a+4)(5)
%     |                   |      |                   |
%     v                   |      v                   |
%   (2+3)*(2+3)+4         |    (2+3)*(2+3)+4         |
%         |    \          |          |    \          |
%         |     v         |          |     v         |
%         |   (2+3)*5+4   |          |   (2+3)*5+4   |
%         |          \    |          |          \    |
%         v           v   v          v           v   v
%     5*(2+3)+4 -----> 5*5+4     5*(2+3)+4 -----> 5*5+4
% 





\newpage


%  ____                 _                _   _             _      
% |___ \    __   ____ _| |_   _  ___  __| | | | ___   __ _(_) ___ 
%   __) |___\ \ / / _` | | | | |/ _ \/ _` | | |/ _ \ / _` | |/ __|
%  / __/_____\ V / (_| | | |_| |  __/ (_| | | | (_) | (_| | | (__ 
% |_____|     \_/ \__,_|_|\__,_|\___|\__,_| |_|\___/ \__, |_|\___|
%                                                    |___/        
%
% «classical-logic» (to ".classical-logic")

Classical logic:

\msk

Idea:

0 means ``false''

1 means ``true''

\msk

Operations:

\ssk

$\begin{array}[t]{ccllll}
  P & Q & P∧Q   & P∨Q   & P→Q   & P↔Q   \\ \hline
  0 & 0 & 0∧0=0 & 0∨0=0 & 0→0=1 & 0↔0=1 \\
  0 & 1 & 0∧1=0 & 0∨1=1 & 0→1=1 & 0↔1=0 \\
  1 & 0 & 1∧0=0 & 1∨0=1 & 1→0=0 & 1↔0=0 \\
  1 & 1 & 1∧1=1 & 1∨1=1 & 1→1=1 & 1↔1=1 \\
  \end{array}
  %
  \qquad
  %
  \begin{array}[t]{ll}
  P & ¬P \\ \hline
  0 & ¬0=1 \\
  1 & ¬1=0 \\
  \end{array}
$

\msk

We will use a more compact form.

\ssk

If $P=1$ and $Q=0$, then

$\und{\und P 1 → \und Q 0} 0$

So:

\msk

$\begin{array}[t]{ccccccc}
  P & Q & P∧Q & P∨Q & P→Q & P↔Q \\ \hline
  0 & 0 &  0   &  0  &  1   &  1  \\
  0 & 1 &  0   &  1  &  1   &  0  \\
  1 & 0 &  0   &  1  &  0   &  0  \\
  1 & 1 &  1   &  1  &  1   &  1  \\
  \end{array}
  %
  \qquad
  %
  \begin{array}[t]{ccccccc}
  P & ¬P \\ \hline
  0 & 1 \\
  1 & 0 \\
  \end{array}
$

\msk

Constants:

$⊤ = 1$

$⊥ = 0$



\newpage

%  _____                 _                _   _             _      
% |___ /     __   ____ _| |_   _  ___  __| | | | ___   __ _(_) ___ 
%   |_ \ ____\ \ / / _` | | | | |/ _ \/ _` | | |/ _ \ / _` | |/ __|
%  ___) |_____\ V / (_| | | |_| |  __/ (_| | | | (_) | (_| | | (__ 
% |____/       \_/ \__,_|_|\__,_|\___|\__,_| |_|\___/ \__, |_|\___|
%                                                     |___/        
%
% «3-valued-logic» (to ".3-valued-logic")

Our first non-classical logic:

\msk

Idea:

00 means ``false''

11 means ``true''

01 is something intermediate between true and false

\msk

Operations:

\ssk

$\begin{array}[t]{ccccccc}
  P  & Q  & P∧Q & P∨Q & P→Q & P↔Q \\ \hline
  00 & 00 &  00 &  00  &  11  &  11  \\
  00 & 01 &  00 &  01  &  11  &  00  \\
  00 & 11 &  00 &  11  &  11  &  00  \\
  01 & 00 &  00 &  01  &  00  &  00  \\
  01 & 01 &  01 &  01  &  11  &  11  \\
  01 & 11 &  01 &  11  &  11  &  01  \\
  11 & 00 &  00 &  11  &  00  &  00  \\
  11 & 01 &  01 &  11  &  01  &  01  \\
  11 & 11 &  11 &  11  &  11  &  11  \\
  \end{array}
  %
  \qquad
  %
  \begin{array}[t]{ccccccc}
  P  & ¬P \\ \hline
  00 & 11 \\
  01 & 00 \\
  11 & 00 \\
  \end{array}
$

\msk

Constants:

$⊤ = 11$

$⊥ = 00$







\newpage

%  ____                                     _       
% |  _ \ ___ _ __  _ __ ___  ___  ___ _ __ | |_ ___ 
% | |_) / _ \ '_ \| '__/ _ \/ __|/ _ \ '_ \| __/ _ \
% |  _ <  __/ |_) | | |  __/\__ \  __/ | | | ||  __/
% |_| \_\___| .__/|_|  \___||___/\___|_| |_|\__\___|
%           |_|                                     
%
% «represente-graficamente» (to ".represente-graficamente")

Represente graficamente:

$A := \{(1,4), (2,4), (1,3)\}$

$B := \{(1,3), (1,4), (2,4)\}$

$C := \{(1,3), (1,4), (2,4), (2,4)\}$

$D := \{(1,3), (1,4), (2,3), (2,4)\}$

$h := \{(0,3), (1,2), (2,1), (3,0)\}$

$k := \{x:\{0,1,2,3\}; (x,3-x)\}$

$m := \{y:\{0,1,2,3\}; (3-y, y)\}$

\msk

$f := (λx:\{0,1,2\}.\,x·x)$

$g := (λa:\{0,1,2\}.\,3·a)$

$q := (λa:\{0,1,2\}.\,(x+1)^2-2x-1)$



\bsk

Tudo isto aqui a gente pode calcular com tabelas:

$∀x:\{0,1,2,3\}. x < 2$

$∀x:\{0,1,2,3\}. x^2 ≤ 5$

$∀x:\{0,1,2,3\}. x^2 < 10$

$∀x:\{0,1,2,3\}. x≥2$

$∃x:\{0,1,2,3\}. x^2≥5$

$\{x:\{0,1,2,3\}; x^2\}$

$\{x:\{0,1,2,3\}, x≥2; x\}$

$Σx:\{0,1,2,3\}.x^2$

$Πx:\{0,1,2,3\}.x+1$

$λx:\{0,1,2,3\}.5-x$

\bsk

$\begin{array}{lll}
∀x:\{0,1,2\}. P(x)  & = & P(0)∧P(1)∧P(2) \\
∃x:\{0,1,2\}. P(x)  & = & P(0)∨P(1)∨P(2) \\
\{x:\{0,1,2\}; f(x)\} & = & \{f(0), f(1), f(2)\}\\
Σx:\{0,1,2\}.f(x)    & = & f(0)+f(1)+f(2) \\
Πx:\{0,1,2\}.f(x)    & = & f(0)·f(1)·f(2) \\
λx:\{0,1,2\}.f(x)    & = & \{(0,f(0)), (1,f(1)), (2,f(2))\}\\
\end{array}
$

\bsk

Obs:

$\begin{array}{llll}
Σx:\{0,1,2,2,3\}.x^2 & → & f(0)+f(1)+f(1)+f(2) & (?) \\
Πx:\{0,1,2,2,3\}.x+1 & → & f(0)·f(1)·f(1)·f(2) & (?) \\
\end{array}
$



If $P(x) = (x<2)$ then


%D diagram reduce-fa
%D 2Dx     100 +80
%D 2D  100 A   B
%D 2D
%D 2D  +20 C   D
%D 2D
%D 2D  +20     E
%D 2D
%D ren  A  ==> ∀x:\{0,1,2\}.P(x)
%D ren  B  ==> P(0)∧P(1)∧P(2)
%D ren  C  ==> ∀x:\{0,1,2\}.x<2
%D ren  D  ==> (0<2)∧(1<2)∧(2<2)
%D ren  E  ==> 1∧1∧0
%D (( A B ->   A C -> B D ->   C D ->  D E ->
%D
%D ))
%D enddiagram
%D
$$\Diag{reduce-fa}$$




\newpage




%  _____           _        _             _           
% |_   _|_ _ _   _| |_ ___ | | ___   __ _(_) ___  ___ 
%   | |/ _` | | | | __/ _ \| |/ _ \ / _` | |/ _ \/ __|
%   | | (_| | |_| | || (_) | | (_) | (_| | |  __/\__ \
%   |_|\__,_|\__,_|\__\___/|_|\___/ \__, |_|\___||___/
%                                   |___/             
%
% «tautologies» (to ".tautologies")

We can calculate the result of $¬¬P→P$

when $P=0$ (left) and

when $P=1$ (right) with:

\msk

$\und {{\und {¬ {\und {¬ \und P 0} 1}} 0} → {\und P 0}} 1
 \qquad
 \und {{\und {¬ {\und {¬ \und P 1} 0}} 1} → {\und P 1}} 1
$

\bsk

The {\it subformulas} of $¬¬P→P$ are:

\msk

$\subf{\subf{¬ \subf{¬ \subf P}} → {\subf P}}$

\bsk

If we write the result of each subformula

under its central connective we get:

\msk

\def\f#1{\framebox{1}}
 
$\begin{array}{ccccc}
 ¬ & ¬ & P & → & P \\ \hline
   &   & 0 &    & 0 \\[-7pt]
   & 1 &   &    &   \\[-7pt]
 0 &   &   &    &   \\[-7pt]
   &   &   & \f{1} &   \\
 \end{array}
 \qquad
 \begin{array}{ccccc}
 ¬ & ¬ & P & → & P \\ \hline
   &   & 1 &    & 1 \\[-7pt]
   & 0 &   &    &   \\[-7pt]
 1 &   &   &    &   \\[-7pt]
   &   &   & \f{1} &   \\
 \end{array}
$

\msk

We can write all results in the same line...

We get something more compact but harder to read,

\msk

$\begin{array}{ccccc}
 ¬ & ¬ & P & → & P \\ \hline
 0 & 1 & 0 & \f1 & 0 \\
 \end{array}
 \qquad
 \begin{array}{ccccc}
 ¬ & ¬ & P & → & P \\ \hline
 1 & 0 & 1 & \f1 & 1 \\
 \end{array}
$


\bsk

We can put each case in a single line.

Here we also add a column at the left with the values of $P$.

\msk


$\begin{array}{ccccccc}
 P & & ¬ & ¬ & P & → & P \\ \hline
 % (¬\p & (¬\p & \p\p P)) & → & P \\ \hline
 0 & & 0 & 1 & 0 & \f1 & 0 \\
 0 & & 1 & 0 & 1 & \f1 & 1 \\
 \end{array}
$


\msk

\newpage

%   ____                               _                    _             
%  / ___|___  _ __ ___  _ __  _ __ ___| |__   ___ _ __  ___(_) ___  _ __  
% | |   / _ \| '_ ` _ \| '_ \| '__/ _ \ '_ \ / _ \ '_ \/ __| |/ _ \| '_ \ 
% | |__| (_) | | | | | | |_) | | |  __/ | | |  __/ | | \__ \ | (_) | | | |
%  \____\___/|_| |_| |_| .__/|_|  \___|_| |_|\___|_| |_|___/_|\___/|_| |_|
%                      |_|                                                
%
% «comprehension» (to ".comprehension")

Let

$A = \{x:\{-1,...,4\}; x^2\}$ and

$B = \{x:\{-1,...,4\}; x^2≤5; x\}$.

Then $A$ and $B$ can be calculated by:

\msk

$\begin{array}{cc}
 x & x^2 \\ \hline
 -1 & 1 \\
  0 & 0 \\
  1 & 1 \\
  2 & 4 \\
  3 & 9 \\
  4 & 16 \\
 \end{array}
 \qquad
 \begin{array}{cccc}
 x & x^2 & x^2≤5 & x \\ \hline
 -1 &  1 & 1 & -1 \\
  0 &  0 & 1 & 0 \\
  1 &  1 & 1 & 1 \\
  2 &  4 & 1 & 2 \\
  3 &  9 & 0 & \\
  4 & 16 & 0 & \\
  \end{array}
$

\msk

We get:

$A = \{1,0,1,4,9,16\}$,

$B = \{-1,0,1,2\}$.


\bsk

Let

$A = \{x:\{1,...,5\}, y:\{1,...,x\}, x+y≤6; (x,y)\}$ and

$B = \{y:\{1,...,5\}, x:\{y,...,5\}, x+y≤6; (x,y)\}$.

Then $A$ and $B$ can be calculated by:

\msk

$\begin{array}{ccccc}
 x & y & x+y & x+y≤6 & (x,y) \\ \hline
 1 & 1 &  2  &   1   & (1,1) \\
 2 & 1 &  3  &   1   & (2,1) \\
   & 2 &  4  &   1   & (2,2) \\
 3 & 1 &  4  &   1   & (3,1) \\
   & 2 &  5  &   1   & (3,2) \\
   & 3 &  6  &   1   & (3,3) \\
 4 & 1 &  5  &   1   & (4,1) \\
   & 2 &  6  &   1   & (4,2) \\
   & 3 &  7  &   0   &       \\
   & 4 &  8  &   0   &       \\
 5 & 1 &  6  &   1   & (5,1) \\
   & 2 &  7  &   1   &       \\
   & 3 &  8  &   0   &       \\
   & 4 &  9  &   0   &       \\
   & 5 & 10  &   0   &       \\
 \end{array}
 \qquad
 \begin{array}{ccccc}
 y & x & x+y & x+y≤6 & (x,y) \\ \hline
 1 & 1 &  2  &   1   & (1,1) \\
   & 2 &  3  &   1   & (2,1) \\
   & 3 &  4  &   1   & (3,1) \\
   & 4 &  5  &   1   & (4,1) \\
   & 5 &  6  &   1   & (5,1) \\
 2 & 2 &  4  &   1   & (2,2) \\
   & 3 &  5  &   1   & (3,2) \\
   & 4 &  6  &   1   & (4,2) \\
   & 5 &  7  &   0   &       \\
 3 & 3 &  6  &   1   & (3,3) \\
   & 4 &  7  &   0   &       \\
   & 5 &  8  &   0   &       \\
 4 & 4 &  8  &   0   &       \\
   & 5 &  9  &   0   &       \\
 5 & 5 & 10  &   0   &       \\
 \end{array}
$

\msk

We get:

$A = \{ (1,1), (2,1), (2,2), (3,1), (3,2), (3,3), (4,1), (4,2), (5,1)\}$ and

$B = \{ (1,1), (2,1), (3,1), (4,1), (5,1), (2,2), (3,2), (4,2), (3,3)\}$.



\newpage

%  _____ _ _ _         
% | ____| (_) | ____ _ 
% |  _| | | | |/ / _` |
% | |___| | |   < (_| |
% |_____|_|_|_|\_\__,_|
%                      
% «elika» (to ".elika")

Há quatro anos, tivemos no CEFET/RJ nossos primeiros alunos cotistas.
Para entrar lá, os jovens fazem uma prova de seleção. Naquele ano,
50\% das vagas foram destinadas para alunos negros, de escolas
públicas e com renda baixa.

Lembro-me que levei um susto ao entrar em sala. Havia negros e alunos
extremamente diferentes na forma de se expressar. Eu simplesmente não
sabia como lidar. Pensei em escrever uma carta para Dilma reclamando.
Se esse governo quer colocar cotistas em sala, que ao menos nos dê uma
certa infra-estrutura para recebê-los! Psicólogos, pedagogos,
assistentes sociais... cadê esse time para nos ajudar? Nada? Como
assim?

Da mesma forma que sempre fazia com a minha turma, eu mandava o meu
aluno estudar. Dizia que se ele não fizesse a parte dele, não passaria
porque bababá bububú... muitos alunos cotistas não mexiam o dedo mesmo
eu repetindo o discurso: você tem que estudar! Você tem que estudar!!!

Percebi que muitos não sabiam o que era ``estudar`` porque, meodeos,
nunca haviam estudado. Era como eu virar para qualquer outro na rua
que nunca, por exemplo, estudou música e falar: você tem que treinar
piano! Você tem que treinar piano! O cara ia sentar em frente ao piano
e fazer o quê? Não saberia nem por onde começar! Quando percebi isso
entrei em desespero porque o problema era muito maior do que
pensava...

O que fazer? Desistir? Deixar que todos repetissem? Mas seriam muitos!
O desespero une os seres humanos que estão sob o mesmo inferno. Nós,
professores, fomos conversando e juntamente com parte da equipe
pedagógica, criando subsídios para esses alunos.

A ficha caiu quando um menino de boné e cordão prata veio até mim e
falou: ``Professora, você fala que eu tenho que estudar. O que seria
exatamente isso? Eu não quero perder essa oportunidade. Me ajuda...``

Esse menino mal sabia pegar no lápis por falta de hábito...

Tivemos que lidar também com tensões e preconceitos que existiam entre
eles. Por exemplo, alguns alunos que vieram de escolas particulares
com família bem estruturada não entendiam por quê o colega não fazia o
trabalho direito. Inicialmente, houve, em algumas turmas, segregação.
No jogo de xadrez, por exemplo, onde temos peças pretas e brancas,
eles perguntavam quem seria os cotistas e os não-cotistas...

Sei que criamos aulas de atendimento... preparamos nossos monitores
para atender a esse novo perfil de aluno. Ensinei a aluno segurar no
lápis e organizar o raciocínio para aprender física e fazer problemas
de IME e ITA como fazia em todos os outros anos e dá-lhe conversas com
todos os demais privilegiados para entender que não é excluindo que
incluímos ninguém. Não é fazendo o mal que faremos um bem...

O que nenhum professor do CEFET admitia era baixar o nível de nossa
instituição. Eles, os alunos cotistas, teriam que alcançar os demais.
Foi preciso muita dedicação, hora extra, mais avaliações para o aluno
ter oportunidade de recuperar a nota - dentre outras coisas maiores
como, por exemplo, amor ao próximo e empatia à causa - para que o
equilíbrio, enfim, fosse alcançado.

Foi preciso muito mais trabalho...

Fizemos um forte levantamento sobre o rendimento desses alunos. Quanta
emoção ver as notas deles no segundo semestre se igualando aos demais
colegas que tiveram muito mais oportunidades e condições para estudar.
Quanta emoção... conseguimos, gente, conseguimos... estamos
conseguindo...

Percebi claramente que falta de base nada tem a ver com capacidade
intelectual e me surpreendi muito quando vi minha cara se esfarelando
e a poesia sambando na cara do meu preconceito ou melhor, do meu
desespero - no sentido, aqui, de negar a esperança.

Este ano (como em outros nas minhas turmas do primeiro ano), minha
primeira avaliação foi coletiva e não individual. Os alunos tinham que
fazer um grupo, estudar entre eles e, no dia da prova, eu faria uma
pergunta em que somente um deles, sorteado por mim na hora, resolveria
no quadro a questão por mim colocada. A nota do aluno escolhido seria
a nota de todos os demais componentes daquele grupo. Essa foi uma
forma que encontrei de forçar os alunos privilegiados a me ajudarem a
ajudar os menos privilegiados.

Para um jovem de 15 anos, isso beirou o absurdo das injustiças. Uma
aluna veio falar comigo: ``professora, eu vou ter que convencer o outro
a estudar como? Eu tô chamando e ele, quando vem, nada fala!``

Com muito amor e já mais experiente e segura, expliquei a ela que
estávamos lidando com uma pessoa que vinha de uma realidade
completamente diferente e que a forma de incluí-la não seria fazendo
um chamado comum porque esse ser já tinha sofrido na pele o diabo da
exclusão social e se sentia amedrontado perante os demais. ``Você vai
ser o diferencial na vida dele. Dependendo da forma em que se chegue a
ele, você pode despertar um artista, um sábio, um colega pensante ou
minar qualquer coisa boa que possa emergir.'' A menina de 15 anos me
olhou assustada. Nunca talvez ninguém havia lhe dado tanta
responsabilidade. Continuei: ``Sim. Temos que, acima de tudo, cuidar
uns dos outros sempre. Isso se aprende também na escola.''

A prova foi ontem. Sem querer, escolhi o aluno com maior dificuldade.
Ele foi ao quadro e falou com certa timidez natural, mas com uma
segurança que eu mesma não esperava.

Ao final da aula, a aluna veio emocionada falar comigo: ``Professora,
fiz o que a senhora falou. Chamei o menino de outra forma e com
jeitinho fui tirando dele o que ele sabia e mostrando a ele como agir.
Estudamos a tarde toda. Você viu como ele falou bem?''. Havia o
orgulho e a felicidade em ter ajudado o próximo e incluir um que, em
outra época, seria completamente jogado às margens da nossa sociedade
sendo o que chamamos de ``marginal'' em sua essência.

Escrevo isso sob uma emoção ainda muito forte. Quando vejo a primeira
turma de cotistas se formando com louvor sem nada mais ter do que se
envergonhar em termos de conhecimento em relação aos seus colegas, eu
devo agradecer por essa oportunidade que esse governo me deu de fazer
com que eu fosse uma verdadeira educadora. Devo agradecer pela
oportunidade de me fazer unir e dialogar com os colegas e crescermos
todos como um verdadeiro centro de ensino. Devo agradecer por ter me
feito um ser humano infinitamente mais sensível e melhor.

Reclama da política das cotas quem nunca sentiu na pele e testemunhou
o desabrochar da dignidade de um cidadão...

\msk

Elika Takimoto - 30/abril/2016

\url{https://www.facebook.com/elika.takimoto/posts/1197552476921840}


\newpage



%  _        _      _   _                       _       
% (_)_ __  (_) ___| |_(_)_   ____ _ ___    ___| |_ ___ 
% | | '_ \ | |/ _ \ __| \ \ / / _` / __|  / _ \ __/ __|
% | | | | || |  __/ |_| |\ V / (_| \__ \ |  __/ || (__ 
% |_|_| |_|/ |\___|\__|_| \_/ \__,_|___/  \___|\__\___|
%        |__/                                          
%
% «inj-sobre-bij» (to ".inj-sobre-bij")

$\und{\und{\und{\und{P(2)} 1 ∧ \und{P(3)} 1} 1 ∧ \und{\und{P(4)} 1 ∧ \und{P(5)} 1} 1} 1 ∧
      \und{\und{\und{P(6)} 1 ∧ \und{P(7)} 0} 0 ∧ \und{\und{P(8)} 1 ∧ \und{P(9)} 1} 1} 0
     } 0
$

\msk

$P(a) := (a ≠ 7)$

$P := λa. a ≠ 7$

\msk

$∀a:\{2,...,9\}.P(a)$

$→ (...∧P(7)∧...)$

$→ (...∧0∧...)$

$→ 0$

\bsk

\def\Uniq{\operatorname{Uniq}}
\def\Uniq{\operatorname{\mathsf{Uniq}}}
\def\vtab#1{\vbox{\begin{tabbing}#1\end{tabbing}}}
\def\vtab#1{\hbox{\vbox{\begin{tabbing}#1\end{tabbing}}}}
\def\ftab#1{\framebox{\vtab{#1}}}
% (find-es "tex" "tabbing")

\ftab{
$f:A→B$ \\
se \= $f⊆A×B$ \\
   \> $∧ ∀a{:}A.\,∃!b{:}B.\,(a,b)∈f$
}

\ftab{$f:A→B$ \a'e sobrejetiva \\
se \= $f:A→B$ \\
   \> $∧ ∀b{:}B.\,∃a{:}A.\,f(a)=b$
}
\ftab{$f:A→B$ \a'e injetiva \\
se \= $f:A→B$ \\
   \> $∧ ∀b{:}B.\,\Uniq a{:}A.\,f(a)=b$
}
\ftab{$f:A→B$ \a'e bijetiva \\
se \= $f:A→B$ \\
   \> $∧ ∀b{:}B.\,∃!a{:}A.\,f(a)=b$
}


\bsk

% (find-es "tex" "overset-and-underset")
$P \underset{M}{≤} Q$






% \end{document}
\newpage


%        _      _   ____                     _             
%  _ __ (_) ___| |_|___ \ _____   _____  ___| |_ ___  _ __ 
% | '_ \| |/ __| __| __) / _ \ \ / / _ \/ __| __/ _ \| '__|
% | |_) | | (__| |_ / __/  __/\ V /  __/ (__| || (_) | |   
% | .__/|_|\___|\__|_____\___| \_/ \___|\___|\__\___/|_|   
% |_|                                                      
%
% «pict2evector» (to ".pict2evector")
% Obsolete! See:
%   (find-dn6 "picture.lua" "pict2e")
%   (find-dn6 "picture.lua" "pict2e" "pict2evector =")



% (find-angg "LUA/integrate-2015.lua")
% (find-angg "LUA/integrate-2015.lua" "local ai = function")
% (find-dn6 "picture.lua" "LPicture")

%L pict2evector = function (x0, y0, x1, y1)
%L     local dx, dy = x1 - x0, y1 - y0
%L     local f = function (dx, dy, len)
%L         return format("\\put(%.3f,%.3f){\\vector(%.3f,%.3f){%.3f}}",
%L           x0, y0, dx, dy, len)
%L       end
%L     if dx > 0 then return f(1, dy/dx, dx) end
%L     if dx < 0 then return f(-1, dy/dx, -dx) end
%L     if dx == 0 and dy > 1 then return f(0, 1, dy) end
%L     if dx == 0 and dy < 1 then return f(0, -1, -dy) end
%L     error()
%L   end

%L polyF = function (F, a, b, n)   -- F(t) returns a point
%L     local ai = function (i) return a + (b-a)*i/n end
%L     local latex = ""
%L     for i=0,n do latex = latex .. tostring(F(ai(i))) end
%L     return latex
%L   end
%L polyf = function (f, a, b, n)   -- f(x) returns y
%L     local F = function (t) return V{t,f(t)} end
%L     return polyF(F, a, b, n)
%L   end
%L polylineF = function (F, a, b, n) return "  \\polyline"..polyF(F, a, b, n) end
%L polylinef = function (f, a, b, n) return "  \\polyline"..polyf(f, a, b, n) end

%L LPicture.__index.polyF = function (lp, F, a, b, n)   -- F(t) returns a point
%L     local ai = function (i) return a + (b-a)*i/n end
%L     local latex = ""
%L     for i=0,n do latex = latex .. tostring(F(ai(i))) end
%L     return latex
%L   end
%L LPicture.__index.polyf = function (lp, f, a, b, n)   -- f(x) returns y
%L     local F = function (t) return V{t,f(t)} end
%L     return lp:polylineF(F, a, b, n)
%L   end
%L LPicture.__index.polylineF = function (lp, F, a, b, n)
%L     lp.latex = lp.latex.."  \\polyline"..lp:polyF(F, a, b, n).."\n"
%L     return lp
%L   end
%L LPicture.__index.polylinef = function (lp, f, a, b, n)
%L     lp.latex = lp.latex.."  \\polyline"..lp:polyF(F, a, b, n).."\n"
%L     return lp
%L   end

%L lp = LPicture.new{}
%L print(polyf(math.sin, 0, math.pi, 10))

\def\Vector(#1,#2)(#3,#4){\expr{pict2evector(#1, #2, #3, #4)}}
\pu

\pu


% (find-angg ".emacs.papers" "pict2e")
% (find-es "tex" "pict2e")
% (find-es "tex" "pict2e-example")
% (find-es "tex" "pict2e-vector")
% (find-LATEX "edrx15.sty" "picture-cells")
\def\putb(#1,#2){\put(#1,#2){\cell{\bullet}}}
\def\putx#1{\put(#1,-1){\cell{#1}}}
\def\puty#1{\put(-1,#1){\cell{#1}}}

\celllower=5pt
\celllower=2.5pt

\setlength{\unitlength}{10pt}
\begin{picture}(10,10)
  % \put(0,2){\oval(20,4)[r]}
  \Line(0,0)(4,0)
  \Line(0.5,0)(0.5,4)
  \put(0,0){\vector(0,4){1}}
  \put(1,0){\vector(0,1){2}}
  \put(2,0){\vector(2,3){1}}
  \put(3,0){\vector(2,3){4}}
  % \put(3,2){\cell{$\bullet$}}
  \put(0,2){\cell{\bullet}}
  \put(3,2){\cell{\bullet}}
  \put(3,0){\cell{\bullet}}
\end{picture}%
%


\begin{picture}(10,10)
  \Vector(0,-2)(0,2)
  \Vector(-4,0)(4,0)
  \expr{polylinef(math.sin, -math.pi, math.pi, 40)}
  \put(0,-1){\cell{0}}
  \put(1,-1){\cell{1}}
  \put(2,-1){\cell{2}}
  \put(3,-1){\cell{3}}
  \put(-1,0){\cell{0}}
  \put(-1,1){\cell{1}}
  \put(3,2){\cell{\bullet}}
  \put(3,0){\cell{\bullet}}
  \put(-1,-1){\cell{\bullet}}
\end{picture}%

\def\putx#1{\put(#1,-1){\cell{#1}}}
\def\puty#1{\put(-1,#1){\cell{#1}}}
\def\putx#1{\put(#1,-0.5){\cell{#1}}}
\def\puty#1{\put(-0.5,#1){\cell{#1}}}

\begin{picture}(10,10)
  \Vector(0,-2)(0,2)
  \Vector(-4,0)(4,0)
  \expr{polylinef(math.sin, -math.pi, math.pi, 40)}
  \puty0 \puty1
  \putx0 \putx1 \putx2 \putx3
  \putb(3,2)
  \putb(3,0)
  \putb(-1,-1)
\end{picture}%





\begin{picture}(10,10)
  \Vector(0,0)(0,5)
  \Vector(0,0)(3,4)
  \Vector(0,0)(4,3)
  \Vector(0,0)(5,0)
  \Vector(0,0)(4,-3)
  \Vector(0,0)(3,-4)
  \Vector(0,0)(0,-5)
  \Vector(0,0)(-3,-4)
  \Vector(0,0)(-4,-3)
  \Vector(0,0)(-5,0)
  \Vector(0,0)(-4,3)
  \Vector(0,0)(-3,4)
\end{picture}%


$
 \celllower=2.5pt
 \bhbox{\cell{\bullet}}
 \celllower=5pt
 \bhbox{\cell{\bullet}}
 \qquad
 \bhbox{Hello}
 \celllower=2.5pt
 \cell{\bullet}
$


\end{document}














\end{document}

% Local Variables:
% coding: utf-8-unix
% ee-anchor-format:     "«%s»"
% End:
