% (find-angg "LATEX/2016-2-LA-lambda.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2016-2-LA-lambda.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2016-2-LA-lambda.pdf"))
% (defun e () (interactive) (find-LATEX "2016-2-LA-lambda.tex"))
% (defun u () (interactive) (find-latex-upload-links "2016-2-LA-lambda"))
% (find-xpdfpage "~/LATEX/2016-2-LA-lambda.pdf")
% (find-sh0 "cp -v  ~/LATEX/2016-2-LA-lambda.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2016-2-LA-lambda.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2016-2-LA-lambda.pdf
%               file:///tmp/2016-2-LA-lambda.pdf
%           file:///tmp/pen/2016-2-LA-lambda.pdf
% http://angg.twu.net/LATEX/2016-2-LA-lambda.pdf

% «.expressions-and-reductions»	(to "expressions-and-reductions")
% «.vars-and-algebra»		(to "vars-and-algebra")
% «.lambda»			(to "lambda")
% «.types»			(to "types")
% «.function-graphs»		(to "function-graphs")
% «.typed-L1-trees»		(to "typed-L1-trees")
% «.types-exercises»		(to "types-exercises")
% «.represente-graficamente»	(to "represente-graficamente")


\documentclass[oneside]{book}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
%\usepackage{tikz}
%
\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")
%
\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{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()}}

% \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}
  }





%  ____       _____           _  _       ____  
% |___ \__  _|___ /     _    | || |__  _| ___| 
%   __) \ \/ / |_ \   _| |_  | || |\ \/ /___ \ 
%  / __/ >  < ___) | |_   _| |__   _>  < ___) |
% |_____/_/\_\____/    |_|      |_|/_/\_\____/ 
%                                              
% «expressions-and-reductions» (to ".expressions-and-reductions")
% (lal162p 1 "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")
% (lal162p 2 "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")
% (lal162p 3 "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}$.

\ssk

Note that this is:
%
$$\def\t#1{\text{(#1)}}
  \begin{array}{cccc}
         f & (\,n\,)            & = & 2+\sqrt{n} \\[5pt]
  \t{name} & (\,\t{variable}\,) & = & \t{expression} \\
  \end{array}
$$

\newpage



%   __                  _   _                                     _         
%  / _|_   _ _ __   ___| |_(_) ___  _ __     __ _ _ __ __ _ _ __ | |__  ___ 
% | |_| | | | '_ \ / __| __| |/ _ \| '_ \   / _` | '__/ _` | '_ \| '_ \/ __|
% |  _| |_| | | | | (__| |_| | (_) | | | | | (_| | | | (_| | |_) | | | \__ \
% |_|  \__,_|_| |_|\___|\__|_|\___/|_| |_|  \__, |_|  \__,_| .__/|_| |_|___/
%                                           |___/          |_|              
%
% «function-graphs» (to ".function-graphs")
% (lal162p 4 "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 can think that a function {\sl is} its graph,

and that a lambda-expression (with domain) reduces to a 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    +90   +70
%D 2D  100        A
%D 2D             |
%D 2D             v
%D 2D  +20 b      B --> C 
%D 2D      |      |     |
%D 2D      v      v     v
%D 2D  +35 d      D --> E
%D 2D      |      |     |
%D 2D      v      v     v
%D 2D  +45 f      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)^2
%D ren     F  G   ==>                     \graphb(-2)              4
%D ren  b  d  f   ==>   (λk:\{-2,-1,0,1,2\}.k^2)  \grapha  \graphb
%D (( A B -> B E ->
%D           B D -> # C E ->
%D           D E ->
%D           D F -> E G ->
%D           F G ->
%D    b d -> d f ->
%D ))
%D enddiagram
%D
\pu
$$\def\grapha{\csm{(-2,(-2)^2),\\(-1,(-1)^2),\\(0,0^2),\\(1,1^2),\\(2,2^2)}}
  \def\graphb{\csm{(-2,4),\\(-1,1),\\(0,0),\\(1,1),\\(2,4)}}
  \diag{reduce-k2-with-domain}
$$

\bsk

Note:

the graph of $(λn:\N.n^2)$ has infinite points,

the graph of $(λn:\N.n^2)$ is an infinite set,

the graph of $(λn:\N.n^2)$ can't be written down {\sl explicitly} without `...'s...

\msk

Mathematicians love infinite sets.

Computers hate infinite sets.

For mathematicians a function {\sl is} its graph.

For computer scientists a function {\sl is} is a finite program.

Computer scientists love `$λ$'s!

\msk

{\sl I} love things like this: $\csm{(3,30),\\(4,40)}(3) = 30$


% \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

%  _____                      
% |_   _|   _ _ __   ___  ___ 
%   | || | | | '_ \ / _ \/ __|
%   | || |_| | |_) |  __/\__ \
%   |_| \__, | .__/ \___||___/
%       |___/|_|              
%
% «types» (to ".types")
% (lal162p 5 "types")

Types (introduction)

\bsk

Let:

$\begin{array}{l}
 A = \{1,2\} \\
 B = \{30,40\}. \\
 \end{array}
$

\ssk

If $f:A→B$, then $f$ is one of these

four functions: 
%
$${\def\f#1 #2 {\sm{1↦#1\\2↦#2}}
 \f 30 30 , \f 30 40 , \f 40 30 , \f 40 40
}
$$

or, in other notation,
%
$${\def\f#1 #2 {\csm{(1,#1)\\(2,#2)}}
 \f 30 30 , \f 30 40 , \f 40 30 , \f 40 40
}
$$

which means that:
%
$$\def\f#1 #2 {\csm{(1,#1)\\(2,#2)}}
  f ∈ \csm{ \f 30 30 , \f 30 40 , \f 40 30 , \f 40 40 }
$$

Let's use the notation ``$A→B$'' for

``the set of all functions from $A$ to $B$''.

\msk

Then $(A→B) =
  \def\f#1 #2 {\csm{(1,#1)\\(2,#2)}}
  \csm{ \f 30 30 , \f 30 40 , \f 40 30 , \f 40 40 }
$

and $f:A→B$

means $f∈(A→B)$.

\msk

In Type Theory and $λ$-calculus ``$a:A$''

is pronounced ``$a$ is of type $A$'', and the meaning

of this is {\sl roughly} ``$a∈B$''.

(We'll see the differences between `$∈$' and `$:$' (much) later).

\msk

Note that:

1. if $f:A→B$ and $a:A$ then $f(a):B$

2. if $a:A$ and $b:B$ then $(a,b):A×B$

3. if $p:A×B$ then $πp:A$ and $π'p:B$, where

`$π$' means `first projection' and

`$π'$' means `second projection';

if $p=(2,30)$ then $πp=2$, $π'p=30$.

\msk

If $p:A×B$ and $g:B→C$, then:
%
\def\und#1#2{\underbrace{#1}_{#2}}
%
$$\und{(\und{π\und{p}{:A×B}}{:A},\;\;
        \und{\und{g}{:B→C}(\und{π'\und{p}{:A×B}}{:B})}{:C})}{:A×C})
$$





\newpage


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

Typed $λ$-calculus: trees

\msk

$\begin{array}{l}
A = \{1,2\} \\
B = \{3,4\} \\
C = \{30,40\} \\
D = \{10,20\} \\
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

If we know [the values of] $a$, $b$, $f$

then we know [the value of] $(a,f(b))$.

If $(a,b)=(2,3)$ and $f=\csm{(3,30),\\(4,40)}$

then $(a,f(b))=(2,30)$.

If we know the {\sl types} of $a$, $b$, $f$

we know the type of $(a,f(b))$.

If we know the types of $p$, $f$

we know the type of $(πp,f(π'p))$.

If we know the types $p$, $f$

we know the type of $(λp:A×B.(πp,f(π'p)))$.



%:
%:            (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

\newpage

%  _____                                        
% |_   _|   _ _ __   ___  ___ _    _____  _____ 
%   | || | | | '_ \ / _ \/ __(_)  / _ \ \/ / __|
%   | || |_| | |_) |  __/\__ \_  |  __/>  <\__ \
%   |_| \__, | .__/ \___||___(_)  \___/_/\_\___/
%       |___/|_|                                
%
% «types-exercises» (to ".types-exercises")
% (lal162p 7 "types-exercises")

Exercises

\msk

Let:

$\begin{array}{l}
A = \{1,2\} \\
B = \{3,4\} \\
C = \{30,40\} \\
D = \{10,20\} \\
f=\csm{(3,30),\\(4,40)}, \; f:B→C \\
g=\csm{(1,10),\\(2,30)}, \; g:A→D \\
\end{array}
$

\msk

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

b) Let $p = (2,3)$. Evaluate $(g(πp),f(π'p))$.

c) Check that $(g(πp),f(π'p)):D×C$.

d) Suppose that $p:A×B$. Check that
$$(λp:A×B.(g(πp),f(π'p))):A×B→D×C.$$

e) Evaluate $(λp:A×B.(g(πp),f(π'p)))$.


\bsk
\bsk
\bsk

Here is another notation for checking types:
%
\def\und#1#2{\underbrace{#1}_{#2}}
%
$$\und{(λ\und{p}{:A×B}:A×B.\;\;
       \und{(\und{π\und{p}{:A×B}}{:A},\;\;
             \und{\und{f}{:B→C}(\und{π'\und{p}{:A×B}}{:B})}{:C})}{:A×C})
  }{:A×B→A×C}
$$

Compare it with:
%
$$\ded{idxf5}$$









\newpage


%  ____                                     _       
% |  _ \ ___ _ __  _ __ ___  ___  ___ _ __ | |_ ___ 
% | |_) / _ \ '_ \| '__/ _ \/ __|/ _ \ '_ \| __/ _ \
% |  _ <  __/ |_) | | |  __/\__ \  __/ | | | ||  __/
% |_| \_\___| .__/|_|  \___||___/\___|_| |_|\__\___|
%           |_|                                     
%
% «represente-graficamente» (to ".represente-graficamente")
% (lal162p 8 "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}$$











\end{document}

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