|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (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: