Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2017-1-LA-material.tex") % (defun c () (interactive) (find-LATEXsh "lualatex -record 2017-1-LA-material.tex")) % (defun d () (interactive) (find-xpdfpage "~/LATEX/2017-1-LA-material.pdf")) % (defun e () (interactive) (find-LATEX "2017-1-LA-material.tex")) % (defun u () (interactive) (find-latex-upload-links "2017-1-LA-material")) % (find-xpdfpage "~/LATEX/2017-1-LA-material.pdf") % (find-sh0 "cp -v ~/LATEX/2017-1-LA-material.pdf /tmp/") % (find-sh0 "cp -v ~/LATEX/2017-1-LA-material.pdf /tmp/pen/") % file:///home/edrx/LATEX/2017-1-LA-material.pdf % file:///tmp/2017-1-LA-material.pdf % file:///tmp/pen/2017-1-LA-material.pdf % http://angg.twu.net/LATEX/2017-1-LA-material.pdf % Índice improvisado, com links pras páginas: % (find-LATEXsh "grep lam171p 2017-1-LA-material.tex") % (lam171i) % «.expressions-and-reductions» (to "expressions-and-reductions") % «.vars-and-algebra» (to "vars-and-algebra") % «.lambda» (to "lambda") % «.function-graphs» (to "function-graphs") % «.types» (to "types") % «.typed-L1-trees» (to "typed-L1-trees") % «.types-exercises» (to "types-exercises") % «.type-inference» (to "type-inference") % «.term-inference» (to "term-inference") % «.term-inference-answers» (to "term-inference-answers") % «.contexts» (to "contexts") % «.curry-howard-0» (to "curry-howard-0") % «.curry-howard-1» (to "curry-howard-1") % «.ZHAs-1» (to "ZHAs-1") % «.algebraic-structures» (to "algebraic-structures") % «.protocategories» (to "protocategories") \documentclass[oneside]{book} \usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref") %\usepackage[latin1]{inputenc} \usepackage{amsmath} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{pict2e} \usepackage{color} % (find-LATEX "edrx15.sty" "colors") \usepackage{colorweb} % (find-es "tex" "colorweb") %\usepackage{tikz} % % (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 % \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") \input edrxgac2.tex % (find-LATEX "edrxgac2.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()}} \directlua{dofile "edrxtikz.lua"} % (find-LATEX "edrxtikz.lua") \directlua{dofile "edrxpict.lua"} % (find-LATEX "edrxpict.lua") %L V.__tostring = function (v) return format("(%.3f,%.3f)", v[1], v[2]) end \def\tabl#1{\begin{tabular}{l}#1\end{tabular}} \def\tablt#1{\begin{tabular}[t]{l}#1\end{tabular}} \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\ren{\operatorname{ren}} \def\app{\operatorname{app}} \def\pair{\operatorname{pair}} \def\cur{\mathsf{cur}} \def\uncur{\mathsf{uncur}} \def\ren{\mathsf{ren}} \def\app{\mathsf{app}} \def\pair{\mathsf{pair}} \def∧{\&} \def\namedfunction#1#2#3#4#5{ \begin{array}{rrcl} #1: & #2 & → & #3 \\ & #4 & ↦ & #5 \\ \end{array} } \def\IPLai{\text{IPL}_{{∧}{→}}} \def\NDai {\text{ND} _{{∧}{→}}} % ____ _____ _ _ ____ % |___ \__ _|___ / _ | || |__ _| ___| % __) \ \/ / |_ \ _| |_ | || |\ \/ /___ \ % / __/ > < ___) | |_ _| |__ _> < ___) | % |_____/_/\_\____/ |_| |_|/_/\_\____/ % % «expressions-and-reductions» (to ".expressions-and-reductions") % (lam171p 1 "expressions-and-reductions") % (laq171 1) % (laq171 2) % \noindent {\bf Expressions (and reductions)} % $$\tablt{ The usual way to calculate an \\ expression, one step at a time, \\ with `$=$'s: \\ \\ $\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}$ \\ \\ Each `$=$' corresponds to a `$\diagxyto/->/$' \\ in the reduction diagram below. \\ } % \qquad % \tablt{ A notation for calculating the \\ value of an expression by \\ calculating the values of all \\ its subexpressions: \\ \\ $\mat{\und{\und{2·3}{6} + \und{4·5}{20}}{26}}$ \\ \\ Each `$=$' in the previous diagram \\ corresponds to applying one `$\subf{}{}$'. \\ } $$ \bsk \bsk A {\sl reduction diagram} for $2·3+4·5$: (See Hindley/Seldin, pages 14 and 17) % %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}$$ Note that when we can choose two subexpressions to calculate the `$↓$' evaluatess the leftmost one, and the `$→$' evaluates the rightmost one. \bsk \bsk The {\sl subexpressions} of $2·3+4·5$: $\subf{\subf{\subf{2}·\subf{3}} + \subf{\subf{4}·\subf{5}} } $ \bsk \msk Exercise: Do the same as above for these expressions: a) $2·(3+4)+5·6$ b) $2+3+4$ c) $2+3+4+5$ (Improvise when needed) \newpage % __ __ ___ _ _ % \ \ / /_ _ _ __ ___ ( _ ) __ _| | __ _ ___| |__ _ __ __ _ % \ \ / / _` | '__/ __| / _ \/\ / _` | |/ _` |/ _ \ '_ \| '__/ _` | % \ V / (_| | | \__ \ | (_> < | (_| | | (_| | __/ |_) | | | (_| | % \_/ \__,_|_| |___/ \___/\/ \__,_|_|\__, |\___|_.__/|_| \__,_| % |___/ % % «vars-and-algebra» (to ".vars-and-algebra") % (lam171p 2 "vars-and-algebra") % (lalp 2) {\bf Expressions with variables} \ssk $\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} $ \bsk \bsk \bsk A notation for (simultaneous) substitution: % % (phap 13 "logic-in-HAs") % (pha "logic-in-HAs") % (pha "logic-in-HAs" "simultaneous substitution") % $$((x+y)·z) \subst{ x:=a+y \\ y:=b+z \\ z:=c+x \\ } \;\;=\;\; ((a+y)+(b+z))·(c+x). $$ Note that $((a+b)·(a-b))\subst{a:=5 \\ b:=2 \\} = (5+2)·(5-2)$. \newpage % _ _ _ % | | __ _ _ __ ___ | |__ __| | __ _ % | | / _` | '_ ` _ \| '_ \ / _` |/ _` | % | |__| (_| | | | | | | |_) | (_| | (_| | % |_____\__,_|_| |_| |_|_.__/ \__,_|\__,_| % % «lambda» (to ".lambda") % (lam171p 3 "lambda") % (lalp 3) % (laq171 2) % (laq171 3) {\bf Lambda} \ssk 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 +40 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 CL ---> DL %D 2D | | %D 2D v | %D 2D +20 CS ---> DS %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 CL DL ==> (λa.\,a·a+4)(2+3) (λa.\,a·a+4)(5) %D ren CS DS ==> (a·a+4)[a:=2+3] (a·a+4)[a:=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 -> CS DS -> CL DL -> E F -> F H -> G H -> %D A CL -> CL CS -> CS E -> E G -> %D B DL -> DL DS -> DS 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") % (lam171p 4 "function-graphs") % (lalp 4) {\bf Functions as their graphs} \ssk 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 ($\uparrow$ remember Discrete Mathematics!) 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") % (lam171p 5 "types") % (lalp 5) {\bf Types (introduction)} \ssk 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") % (lam171p 6 "typed-L1-trees") % (lalp 6) {\bf Typed $λ$-calculus: trees} \ssk $\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)$. % %: %: (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}$$ \msk 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 of $p$, $f$ we know the type of $(λp:A×B.(πp,f(π'p)))$. %: %: (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") % (lam171p 7 "types-exercises") % (lalp 8) {\bf Types: exercises} \msk Let: $\begin{array}{l} A = \{1,2\} \\ B = \{3,4\} \\ C = \{30,40\} \\ D = \{10,20\} \\ f=\csm{(3,30),\\(4,40)} \\ g=\csm{(1,10),\\(2,20)} \\ \end{array} $ Note that $f:B→C$ and $g:A→D$. \msk a) Evaluate $A×B$. b) Evaluate $A→D$. c) Evaluate $(πp,f(π'p))$ for each of the four possible values of $p:A×B$. d) Evaluate $λp{:}A{×}B.(πp,f(π'p))$. e) Is this true? % $$(λp{:}A{×}B.(πp,f(π'p))) = \csm{ ((1,3),(1,30)), \\ ((1,4),(1,40)), \\ ((2,3),(2,30)), \\ ((2,4),(2,40)) \\ }$$ f) Let $p = (2,3)$. Evaluate $(g(πp),f(π'p))$. g) Check that if $p:A×B$ then $(g(πp),f(π'p)):D×C$. h) Check that $$(λp{:}A{×}B.(g(πp),f(π'p))):A×B→D×C.$$ i) Evaluate $(λp{:}A{×}B.(g(πp),f(π'p)))$. \newpage % _____ _ __ % |_ _| _ _ __ ___ (_)_ __ / _| ___ _ __ ___ _ __ ___ ___ % | || | | | '_ \ / _ \ | | '_ \| |_ / _ \ '__/ _ \ '_ \ / __/ _ \ % | || |_| | |_) | __/ | | | | | _| __/ | | __/ | | | (_| __/ % |_| \__, | .__/ \___| |_|_| |_|_| \___|_| \___|_| |_|\___\___| % |___/|_| % % «type-inference» (to ".type-inference") % (lam171p 8 "type-inference") {\bf Type inference} \ssk 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}$$ \bsk Exercise: Infer the type of each of the terms below (at the right of the `$:=$'). Use the two notations above. The types of $f$, $g$, $h$, $k$ are shown in the diagram below. $\begin{array}{rrcl} a) & ({×}C)f &:=& λp{:}A{×}C.(f(πp),π'p) \\ b) & h^♭ &:=& λq{:}B{×}C.(h(πq))(π'q) \\ c) & g^♯ &:=& λb{:}B.λc{:}C.g(b,c) \\ d) & (C{→})k &:=& λφ{:}C{→}D.λc{:}C.k(φc) \\ \end{array} $ \bsk %D diagram CCC-adj %D 2Dx 100 +40 %D 2D 100 AxC <--| A %D 2D | | %D 2D | <-| | %D 2D v v %D 2D +30 BxC <--| B %D 2D | | %D 2D | <-| | %D 2D | |-> | %D 2D v v %D 2D +30 D |--> C->D %D 2D | | %D 2D | |-> | %D 2D v v %D 2D +30 E |--> C->E %D 2D %D ren AxC BxC C->D C->E ==> A{×}C B{×}C C{→}D C{→}E %D 2D %D (( AxC A <-| %D BxC B <-| %D D C->D |-> %D E C->E |-> %D %D A B -> .plabel= r f %D AxC BxC -> .plabel= l ({×}C)f %D AxC B harrownodes nil 20 nil <-| %D %D BxC D -> .plabel= l \sm{h^\flat\\g} %D B C->D -> .plabel= r \sm{h\\g^\sharp} %D BxC C->D harrownodes nil 20 nil <-| sl^ %D BxC C->D harrownodes nil 20 nil |-> sl_ %D %D D E -> .plabel= l k %D C->D C->E -> .plabel= r (C{→})k %D D C->E harrownodes nil 20 nil |-> %D )) %D enddiagram %D \pu $$\diag{CCC-adj}$$ % https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus \newpage % _____ _ __ % |_ _|__ _ __ _ __ ___ (_)_ __ / _| ___ _ __ ___ _ __ ___ ___ % | |/ _ \ '__| '_ ` _ \ | | '_ \| |_ / _ \ '__/ _ \ '_ \ / __/ _ \ % | | __/ | | | | | | | | | | | | _| __/ | | __/ | | | (_| __/ % |_|\___|_| |_| |_| |_| |_|_| |_|_| \___|_| \___|_| |_|\___\___| % % «term-inference» (to ".term-inference") % (lam171p 9 "term-inference") {\bf Term inference} \ssk Exercises: \def\co#1#2{#1:#2} \def\cp#1#2{#1:#2} \def\cp#1#2{\phantom{#1}:#2} %: %: \co{p}{A×C} %: ----------π %: \cp{πp}{A} \co{f}{A→B} \co{p}{A×C} %: ------------------------\app ----------π' %: \cp{f(πp)}{B} \cp{π'p}{C} %: ------------------------------------\pair %: \cp{(f(πp),π'p)}{B×C} %: -------------------------------------λ %: \cp{λp{:}A{×}C.(f(πp),π'p)}{A×C→B×C} %: %: ^CCC-adj-f %: %: \co{q}{B×C} %: -----------π %: \co{q}{B×C} \cp{πq}{B} \co{h}{B→(C→D)} %: -----------π' ----------------------------\app %: \cp{π'q}{C} \cp{h(πq)}{C→D} %: -----------------------------------\app %: \cp{h(πq)(π'q)}{D} %: ----------------------------------λ %: \cp{λq{:}B{×C}.h(πq)(π'q)}{B×C→D} %: %: ^CCC-adj-h %: %: \co{b}{B} \co{c}{C} %: --------------------\pair %: \cp{(b,c)}{B×C} \co{g}{B×C→D} %: --------------------------------------\app %: \cp{g(b,c)}{D} %: ------------------------λ %: \cp{λc{:}C.g(b,c)}{C→D} %: -----------------------------------λ %: \cp{λb{:}B.λc{:}C.g(b,c)}{B→(C→D)} %: %: ^CCC-adj-g %: %: \co{c}{C} \co{φ}{C→D} %: ---------------------\app %: \cp{φc}{D} \co{k}{D→E} %: ---------------------------------\app %: \cp{k(φc)}{E} %: ------------------------λ %: \cp{λc{:}C.k(φc)}{(C→E)} %: --------------------------------------------λ %: \cp{φ{:}C{→}D.λc{:}C.k(φc)}{(C→D)→(C→E)} %: %: ^CCC-adj-k %: \pu $$\ded{CCC-adj-f}$$ $$\ded{CCC-adj-h}$$ $$\ded{CCC-adj-g}$$ $$\ded{CCC-adj-k}$$ \newpage % _____ _ __ ____ % |_ _|__ _ __ _ __ ___ (_)_ __ / _| ___ _ __ ___ _ __ ___ ___ |___ \ % | |/ _ \ '__| '_ ` _ \ | | '_ \| |_ / _ \ '__/ _ \ '_ \ / __/ _ \ __) | % | | __/ | | | | | | | | | | | | _| __/ | | __/ | | | (_| __/ / __/ % |_|\___|_| |_| |_| |_| |_|_| |_|_| \___|_| \___|_| |_|\___\___| |_____| % % «term-inference-answers» (to ".term-inference-answers") % (lam171p 10 "term-inference-answers") {\bf Term inference: answers} \def\co#1#2{#1:#2} \def\cp#1#2{\phantom{#1}:#2} \def\cp#1#2{#1:#2} $$\ded{CCC-adj-f}$$ $$\ded{CCC-adj-h}$$ $$\ded{CCC-adj-g}$$ $$\ded{CCC-adj-k}$$ \newpage % ____ _ _ % / ___|___ _ __ | |_ _____ _| |_ ___ % | | / _ \| '_ \| __/ _ \ \/ / __/ __| % | |__| (_) | | | | || __/> <| |_\__ \ % \____\___/|_| |_|\__\___/_/\_\\__|___/ % % «contexts» (to ".contexts") % (lam171p 11 "contexts") {\bf Contexts and `$⊢$'} \ssk Suppose that $A$, $B$, $C$ are known, and are sets. (Jargon: ``fix sets $A$, $B$, $C$''.) Then this % % (find-angg ".emacs" "laq162" "|-") % (laq162 14 "20161129" "Coproduct diagram, |-, regras") % $$\def\t#1{\text{#1}} \def\fooa{\sm{\t{``context'': a series of} \\ \t{declarations like} \\ var:type}} \def\foob{\sm{term:type}} \\ % \und{p:A×B,f:B→C}{\fooa} ⊢ \und{f(π'p):C}{\foob} $$ Means: ``In this context the expression $expr$ makes sense, is not \textsf{error}, and its result is of type $type$.'' \ssk Note that calculating $f(π'p)$ yields \textsf{error} if we do not know the values of $f$ or $p$. \msk What happens if we add contexts to each $term:type$ in a tree? The two bottom nodes in % $$\ded{idxf5}$$ would become: $$ f:B→C,p:A×B ⊢ (πp,f(π'p)) :A×C $$ $$ f:B→C ⊢ (λp:A×B.(πp,f(π'p))):A×B→A×C $$ After the rule `$λ$' the `$p$' is no longer needed! \msk If we add the contexts and omit the types, the tree becomes: % %: p⊢p %: -----π' %: p⊢p p⊢π'p f⊢f %: ------π ----------------\app %: p⊢πp f,p⊢f(π'p) %: ----------------------\pair %: f,p⊢(πp,f(π'p)) %: -----------------------------λ %: f⊢(λp{:}A{×}B.(πp,f(π'p))) %: %: ^cont1 %: %: [p⊢p]^1 %: -----π' %: [p⊢p]^1 p⊢π'p f⊢f %: ------π ----------------\app %: p⊢πp f,p⊢f(π'p) %: ----------------------\pair %: f,p⊢(πp,f(π'p)) %: -----------------------------λ;1 %: f⊢(λp{:}A{×}B.(πp,f(π'p))) %: %: ^cont2 %: %: [p]^1 %: -----π' %: [p]^1 π'p f %: ------π ----------\app %: πp f(π'p) %: ---------------------\pair %: (πp,f(π'p)) %: -----------------------------λ;1 %: (λp{:}A{×}B.(πp,f(π'p))) %: %: ^cont3 %: \pu $$\ded{cont1} \quad\squigto\qquad \ded{cont3}$$ Notational trick: below the bar `$λ;1$' the value of $p$ is no longer needed; we say that the $p$ is ``discharged'' (from the list of hypotheses) and we mark the `$p$' on the leaves of the tree with `$[·]^1$'; a `$[·]^1$' on a hypothesis means: ``below the bar `$λ;1$' I am no longer a hypothesis''. \newpage % ____ _ _ ___ % / ___| _ _ __ _ __ _ _ | | | | _____ __ / _ \ % | | | | | | '__| '__| | | |_____| |_| |/ _ \ \ /\ / / | | | | % | |__| |_| | | | | | |_| |_____| _ | (_) \ V V / | |_| | % \____\__,_|_| |_| \__, | |_| |_|\___/ \_/\_/ \___/ % |___/ % % «curry-howard-0» (to ".curry-howard-0") % (lam171p 12 "curry-howard-0") {\bf Curry-Howard: introduction} \ssk \par We are learning a system called \par ``the simply-typed $λ$-calculus (with binary products)'' --- \par system $λ1$, for short. \msk \par In $λ1$ in its fullest form, \par its objects are trees of `$\ldots⊢term:type$'s, \par but we saw (evidence) that we can: \par • reconstruct the full tree from just the `$term:type$'s, \par • write just `$:type$'s (except on the leaves, to get the var names), \par • reconstruct the full tree from just the bottom `$term:type$'... \msk For example, we can reconstruct the whole tree, {\sl with contexts}, from: % %: [p:A{×}B]^1 %: ---------π' %: [p:A{×}B]^1 :B f:B→C %: ------π ----------------\app %: :A :C %: ----------------------\pair %: :A{×}C %: ---------λ %: :A{×}B→A{×}C %: %: ^curryhow1 %: $$\pu\ded{curryhow1}$$ \par If we erase the terms and the `:'s and leave only the types, \par we get something that is strikingly similar to a tree in \par Natural Deduction, % %: [A{×}B]^1 %: ---------π' %: [A{×}B]^1 B B→C %: ------π --------------\app %: A C %: ------------------\pair %: A{×}C %: ---------λ %: A{×}B→A{×}C %: %: ^curryhow2 %: %: [P{∧}Q]^1 %: ---------∧E_2 %: [P{∧}Q]^1 Q Q{→}R %: ------∧E_1 -----------------→E %: P R %: ------------------∧I %: P{∧}Q %: ---------→I;1 %: P{∧}R→P{∧}Q %: %: ^curryhow3 %: \pu $$\ded{curryhow2}$$ $$\squigto \qquad \cded{curryhow3}$$ which talks about {\sl logic}. \newpage % ____ _ _ _ % / ___| _ _ __ _ __ _ _ | | | | _____ __ / | % | | | | | | '__| '__| | | |_____| |_| |/ _ \ \ /\ / / | | % | |__| |_| | | | | | |_| |_____| _ | (_) \ V V / | | % \____\__,_|_| |_| \__, | |_| |_|\___/ \_/\_/ |_| % |___/ % % «curry-howard-1» (to ".curry-howard-1") % (lam171p 13 "curry-howard-1") {\bf Curry-Howard: Natural Deduction} \ssk The tree %: [P{∧}Q]^1 %: ---------∧E_2 %: [P{∧}Q]^1 Q Q{→}R %: ------∧E_1 -----------------→E %: P R %: ------------------∧I %: P{∧}Q %: ---------→I;1 %: P{∧}R→P{∧}Q %: %: ^curryhow3 %: \pu $$\ded{curryhow3}$$ is in $\NDai$ (or in $\IPLai$), the fragment of Natural Deduction (or intuitionistic predicate logic) that only has the connectives $∧$ and $→$. \msk Its rules are: %: %: P Q P∧Q P∧Q %: ----∧I ----∧E_1 ---∧E_2 %: P∧Q P Q %: %: ^ndai ^ndae1 ^ndae2 %: %: P [Q]^1 %: :::::::: %: R P P→Q %: -------→I -------→E %: Q→R Q %: %: ^ndii ^ndie %: \pu $$\ded{ndai} \qquad \ded{ndae1} \qquad \ded{ndae2}$$ $$\ded{ndii} \qquad \ded{ndie}$$ \bsk New rules (for $⊤$, $⊥$, $∨$): (not yet --- see the whiteboard for 20170418) % (laq171 9 "20170418" "ND: provando certas coisas vindas de diagramas; regras") \newpage % ______ _ _ _ % |__ / | | | / \ ___ / | % / /| |_| | / _ \ / __| | | % / /_| _ |/ ___ \\__ \ | | % /____|_| |_/_/ \_\___/ |_| % % «ZHAs-1» (to ".ZHAs-1") % (lam171p 14 "ZHAs-1") % (laq171 11 "20170425" "Lógica em ZHAs") {\bf Planar Heyting Algebras} \ssk We read sections 1--7 of: \url{http://angg.twu.net/LATEX/2017planar-has.pdf} \msk %L local mp = mpnew({def="foo", scale="7pt", meta="s"}, "12321L") %L mp:addlrs():output() \pu Let $B=\foo$ . Exercises: Calculate and represent in positional notation when possible: \def\o#1{\mathop{\mathsf{#1}}} \def\o#1{\mathbin{\mathsf{#1}}} \par a) $λlr{:}B.l$ \par b) $λlr{:}B.r$ \par c) $λlr{:}B.(l≤1)$ \par d) $λlr{:}B.(r≥1)$ \par e) $λlr{:}B.lr≤11$ \par f) $λlr{:}B.lr∧12$ \par g) $λlr{:}B.\o{valid}(\ang{l+1,r})$ \par h) $λlr{:}B.lr \o{leftof} 11$ \par i) $λlr{:}B.lr \o{leftof} 12$ \par j) $λlr{:}B.lr \o{above} 11$ \par k) $λlr{:}B.\o{ne}(lr)$ \par l) $λlr{:}B.\o{nw}(lr)$ \par m) $20→11$ \par n) $02→11$ \par o) $22→11$ \par p) $00→11$ \par q) $λlr{:}B.¬lr$ \par r) $λlr{:}B.¬¬lr$ \par s) $λlr{:}B.lr=¬¬lr$ \newpage % _ _ _ _ % / \ | | __ _ ___| |_ _ __ _ _ ___| |_ ___ % / _ \ | |/ _` | / __| __| '__| | | |/ __| __/ __| % / ___ \| | (_| | \__ \ |_| | | |_| | (__| |_\__ \ % /_/ \_\_|\__, | |___/\__|_| \__,_|\___|\__|___/ % |___/ % % «algebraic-structures» (to ".algebraic-structures") % (lam171p 15 "algebraic-structures") {\bf Algebraic structures} \ssk A {\sl ring} is a 6-uple % $$(R, 0_R, 1_R, +_R, -_R, ·_R)$$ where $R, 0_R, \ldots, ·_R$ have the following types, \msk \par \quad $R$ is a set, \par \quad $0_R∈R$, \par \quad $1_R∈R$, \par \quad $+_R:R×R→R$, \par \quad $-_R:R→R$ (unary minus), \par \quad $·_R:R→R$, \msk and where the components obey these equations ($∀a,b,c∈R$): \msk \par \quad $a+0_R = 0_R+a = a$, \; $a+b=b+a$, \; $a+(b+c) = (a+b)+c$, \; $a+(-a) = 0$, \par \quad $a·1_R = 1_R·a = a$, \; $a·b=b·a$, \; $a·(b·c) = (a·b)·c$, \par \quad $a·(b+c) = a·b+a·c$. \msk A {\sl proto-ring} is a 6-uple $(R, 0_R, 1_R, +_R, -_R, ·_R)$ that obeys the typing conditions of a ring. A {\sl ring} is a proto-ring plus the assurance that it obeys the ring equations. \bsk % (ebsp 9 "HAs") % (ebs "HAs") A {\sl proto-Heyting Algebra} is a 7-uple $$H = (Ω,≤_H,⊤_H,⊥_H,∧_H,∨_H,→_H)$$ \msk in which: \msk \par \quad $Ω$ is a set (the ``set of truth values''), \par \quad $≤_H ⊂ Ω×Ω$ (partial order), \par \quad $⊤_H ∈ Ω$, \par \quad $⊥_H ∈ Ω$, \par \quad $∧_H:Ω×Ω→Ω$ \par \quad $∨_H:Ω×Ω→Ω$ \par \quad $→_H:Ω×Ω→Ω$ \msk Sometimes we add operations `$¬$' and $↔$ to a (proto-)HA $H$, % $$H = (Ω,≤_H,⊤_H,⊥_H,∧_H,∨_H,→_H,¬_H,↔_H)$$ by {\sl defining them} as $¬P:=P→⊥$ and $P↔Q:=(P→Q)∧(Q→P)$ (i.e., $¬_H P:=P →_H ⊥_H$ and $P ↔_H Q := (P →_H Q) ∧_H (Q →_H P)$). \bsk \bsk This abuse of language is very common: $R$ ``$=$'' $(R, 0_R, 1_R, +_R, -_R, ·_R)$. \newpage % ____ _ _ % | _ \ _ __ ___ | |_ ___ ___ __ _| |_ ___ % | |_) | '__/ _ \| __/ _ \ / __/ _` | __/ __| % | __/| | | (_) | || (_) | (_| (_| | |_\__ \ % |_| |_| \___/ \__\___/ \___\__,_|\__|___/ % % «protocategories» (to ".protocategories") % (lam171p 16 "protocategories") {\bf Protocategories} \ssk A {\sl protocategory} is a 4-uple % $$\catC = (\catC_0, \Hom_\catC, \id_\catC, ∘_\catC)$$ where \msk \par \quad $\catC_0$ is a set (more precisely a ``class''), \par \quad $\Hom_\catC : \catC_0×\catC_0 → \Sets$, \par \quad $\id_\catC(A) ∈ \Hom_\catC(A,A)$, \par \quad $(∘_\catC)_{ABC}: \Hom_\catC(B,C) × \Hom_\catC(A,B) → \Hom_\catC(A,C)$. \msk A {\sl categoru} is a protocategory plus the assurance that identities behave as expected and composition is associative. \msk Sometimes we add an operation `;' to a category, $$\catC = (\catC_0, \Hom_\catC, \id_\catC, ∘_\catC, ;_\catC)$$ where `;' is the composition in other order: $f∘g$ = $g;f$. % (find-books "__cats/__cats.el" "awodey") % (find-books "__cats/__cats.el" "maclane") \end{document} % Local Variables: % coding: utf-8-unix % ee-anchor-format: "«%s»" % End: