|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2018-2-MD-sequentes.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2018-2-MD-sequentes.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2018-2-MD-sequentes.pdf"))
% (defun e () (interactive) (find-LATEX "2018-2-MD-sequentes.tex"))
% (defun u () (interactive) (find-latex-upload-links "2018-2-MD-sequentes"))
% (find-xpdfpage "~/LATEX/2018-2-MD-sequentes.pdf")
% (find-sh0 "cp -v ~/LATEX/2018-2-MD-sequentes.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2018-2-MD-sequentes.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2018-2-MD-sequentes.pdf
% file:///tmp/2018-2-MD-sequentes.pdf
% file:///tmp/pen/2018-2-MD-sequentes.pdf
% http://angg.twu.net/LATEX/2018-2-MD-sequentes.pdf
% «.complicadas» (to "complicadas")
% «.by-cases» (to "by-cases")
% «.forall-easy» (to "forall-easy")
% «.forall-hard» (to "forall-hard")
% «.exist-easy» (to "exist-easy")
% «.exist-hard» (to "exist-hard")
% «.defs-recursivas» (to "defs-recursivas")
\documentclass[oneside]{article}
\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{lplfitch} % (find-es "tex" "lplfitch")
%\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
\catcode`\^^J=10 % (find-es "luatex" "spurious-omega")
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
\def\expr#1{\directlua{output(tostring(#1))}}
\def\eval#1{\directlua{#1}}
%
\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")
%
% (find-angg ".emacs.papers" "latexgeom")
% (find-latexgeomtext "total={6.5in,8.75in},")
\usepackage[%total={6.5in,4in},
%textwidth=4in, paperwidth=4.5in,
%textheight=5in, paperheight=4.5in,
a4paper,
top=1.5in, left=1.5in%, includefoot
]{geometry}
%
\begin{document}
\catcode`\^^J=10
\edrxcolors
\def\V{\mathbf{V}}
\def\F{\mathbf{F}}
\def\Par {\mathsf{par}}
\def\Impar{\mathsf{impar}}
\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
% (code-xpdf "wikiseq" "~/tmp/Sequent calculus - Wikipedia.pdf")
% (code-pdf-text "wikiseq" "~/tmp/Sequent calculus - Wikipedia.pdf")
% (find-wikiseqpage)
% (find-wikiseqpage 5)
% (find-wikiseqtext)
%: Δ⊢Γ Δ⊢Γ
%: -----(WL-) -----(WR-)
%: Δ,A⊢Γ Δ⊢Γ,A
%:
%: ^WL- ^WR-
%:
%: Δ,Γ⊢Σ Δ⊢Γ,Σ
%: -----(WL) -----(WR)
%: Δ,A,Γ⊢Σ Δ⊢Γ,A,Σ
%:
%: ^WL ^WR
%:
%: Δ,A,B,Γ⊢Σ Δ⊢Γ,A,B,Σ
%: ---------(PL) ---------(PR)
%: Δ,B,A,Γ⊢Σ Δ⊢Γ,B,A,Σ
%:
%: ^PL ^PR
%:
%: Δ,A,A⊢Γ Δ⊢Γ,A,A
%: -------(CL-) -------(CR-)
%: Δ,A⊢Γ Δ⊢Γ,A
%:
%: ^CL- ^CR-
%:
%: Δ,A,A,Γ⊢Σ Δ⊢Γ,A,A,Σ
%: -------(CL) -------(CR)
%: Δ,A,Γ⊢Σ Δ⊢Γ,A,Σ
%:
%: ^CL ^CR
%:
\pu
% (find-wikiseqpage 5)
%:
%: Γ⊢Δ,A∧B Γ⊢Δ,A∧B Γ,A∧B⊢Δ Γ⊢A,Δ Σ⊢B,Π
%: -------(R∧_1) -------(R∧_2) -------(L∧) -------------(R∧)
%: Γ⊢Δ,A Γ⊢Δ,B Γ,A,B⊢Δ Γ,Σ⊢A∧B,Δ,Π
%:
%: ^Rand1 ^Rand2 ^Land ^Rand
%:
%:
%: Γ,A∨B⊢Δ Γ,A∨B⊢Δ Γ⊢A∨B,Δ Γ,A⊢Δ Σ,B⊢Π
%: -------(L∨_1) -------(L∨_2) -------(R∨) -------------(L∨)
%: Γ,A⊢Δ Γ,B⊢Δ Γ⊢A,B,Δ Γ,Σ,A∨B⊢Δ,Π
%:
%: ^Lor1 ^Lor2 ^Ror ^Lor
%:
%:
\pu
%: Γ⊢Δ,A A,Σ⊢Π
%: ---(I) ------------(Cut)
%: A⊢A Γ,Σ⊢Δ,Π
%:
%: ^I ^Cut
%:
\pu
%:
%: Γ⊢A,Δ Σ,B⊢Π Γ⊢A,Δ Σ⊢B,Π
%: --------------(→L) -------------(→R)
%: Γ,Σ,A→B⊢Δ,Π Γ⊢A→B,Δ
%:
%: ^toL ^toR
%:
\pu
%:
%: Γ⊢A,Δ Γ,A⊢Δ
%: -----(¬L) -----(¬R)
%: Γ,¬A⊢Δ Γ⊢¬A,Δ
%:
%: ^notL ^notR
%:
\pu
% (find-wikiseqpage 8)
%:
%: Γ,P[y:=t]⊢Δ Γ⊢P,Δ
%: -----------(∀L) -----------(∀R)^*
%: Γ,∀y.P⊢Δ Γ⊢∀y.P,Δ
%:
%: ^faL ^faR
%:
%:
%: Γ,P⊢Δ Γ⊢P[y:=t],Δ
%: -----------(∃L)^* -----------(∃R)
%: Γ,∃y.P⊢Δ Γ⊢∃y.P,Δ
%:
%: ^exL ^exR
%:
\pu
\fbox{
\begin{tabular}{l}
Regras estruturais: \\
weakening, permutation, contraction \\
\\
$\begin{array}{ccc}
\ded{WL-} && \ded{WR-} \\ \\
\ded{WL} && \ded{WR} \\ \\
\ded{PL} && \ded{PR} \\ \\
\ded{CL-} && \ded{CR-} \\ \\
\ded{CL} && \ded{CR} \\ \\
\end{array}
$ \\
\end{tabular}
}
%
\fbox{
\begin{tabular}{l}
Identidade e cut:
\\
$\begin{array}{ccc}
\ded{I} \\ \\
\ded{Cut} \\
\end{array}
$ \\
\end{tabular}
}
\ssk
\fbox{
\begin{tabular}{l}
Regras lógicas pro $∧$: \\
\\
$\begin{array}{c}
\ded{Rand1} \\ \\
\ded{Rand2} \\ \\
\ded{Land} \\ \\
\ded{Rand} \\
\end{array}
$
\end{tabular}
}
%
%\quad
%
\fbox{
\begin{tabular}{l}
Regras lógicas pro $∨$: \\
\\
$\begin{array}{c}
\ded{Lor1} \\ \\
\ded{Lor2} \\ \\
\ded{Ror} \\ \\
\ded{Lor} \\
\end{array}
$
\end{tabular}
}
\ssk
\fbox{
\begin{tabular}{l}
Regras lógicas pro $→$: \\
\\
$\begin{array}{c}
\ded{toL} \\ \\
\ded{toR} \\
\end{array}
$
\end{tabular}
}
%
%\quad
%
\fbox{
\begin{tabular}{l}
Regras lógicas pro $¬$: \\
\\
$\begin{array}{c}
\ded{notL} \\ \\
\ded{notR} \\
\end{array}
$
\end{tabular}
}
\ssk
\fbox{
\begin{tabular}{l}
Regras lógicas para o $∀$: \\
\\
$\begin{array}{ccc}
\ded{faR} \\ \\
\ded{faL} \\
\end{array}
$ \\
\end{tabular}
}
\fbox{
\begin{tabular}{l}
Regras lógicas para o $∃$: \\
\\
$\begin{array}{ccc}
\ded{exR} \\ \\
\ded{exL} \\
\end{array}
$ \\
\end{tabular}
}
\ssk
Nas regras $(∀R)^*$ e $(∃L)^*$ o `${}^*$' quer dizer que o $y$ não
pode
aparecer como variável livre em $Γ$ ou $Δ$.
\newpage
%:
%:
%:
%:
%: A∧B⊢C A∧B⊢C
%: ===== = -----(L∧)
%: A,B⊢C A,B⊢C
%:
%: ^ex1a ^ex1asol
%:
%: -------(I)
%: A∧B⊢A∧B
%: -------(R∧_2)
%: A∧B⊢A A,B⊢C
%: -------(I) -------------------(Cut)
%: A∧B⊢A∧B A∧B,B⊢C
%: -------(R∧_2) -------(PL)
%: A∧B⊢B \b B,A∧B⊢C
%: -----------------------(Cut)
%: A∧B⊢C A∧B,A∧B⊢C
%: ===== = ---------(CL)
%: A,B⊢C A∧B⊢C
%:
%: ^ex1b ^ex1bsol
%:
%:
%:
%:
%:
%: A⊢B∨C A⊢B∨C
%: ===== = -----(R∨)
%: A⊢B,C A⊢B,C
%:
%: ^ex2a ^ex2asol
%:
%:
%: -------(I)
%: B∨C⊢B∨C
%: -------(L∨_2)
%: A⊢B,C C⊢B∨C
%: -------------------(Cut) -------(I)
%: A⊢B,B∨C B∨C⊢B∨C
%: -------(PR) -------(R∧_2)
%: A⊢B∨C,B B⊢B∨C
%: ------------------------------(Cut)
%: A⊢B,C A⊢B∨C,B∨C
%: ===== = ---------(CR)
%: A⊢B∨C A⊢B∨C
%:
%: ^ex2b ^ex2bsol
%:
\pu
\def\b{\hskip-6ex}
$\begin{array}{rcl}
\ded{ex1a} &=& \ded{ex1asol} \\
\ded{ex1b} &=& \ded{ex1bsol} \\
\\
\\
\ded{ex2a} &=& \ded{ex2asol} \\
\ded{ex2b} &=& \ded{ex2bsol} \\
\end{array}
$
% (find-es "tex" "lplfitch")
% (find-lplfitchpage)
% (find-lplfitchtext)
% \fitchprf{}{
% \subproof{\pline[1.]{\uni{x}{(Cube(x)\lif Small(x))}}}{
% \subproof{
% \pline[2.]{\exi{x}{Cube(x)}}
% }{
% \boxedsubproof[3.]{a}{Cube(a)}{
% \pline[4.]{Cube(a)\lif Small(a)}[\lalle{1}]\\
% \pline[5.]{Small(a)}[\life{4}{3}]\\
% \pline[6.]{\exi{x}{Small(x)}}[\lexii{5}]
% }
% \pline[7.]{\exi{x}{Small(x)}}[\lexie{2}{3--6}]
% }
% \pline[8.]{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}[\lifi{2--7}]
% }
% \pline[9.]{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{
% \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}[\lifi{1--8}]
% }
\newpage
% ____ _ _ _
% / ___|___ _ __ ___ _ __ | (_) ___ __ _ __| | __ _ ___
% | | / _ \| '_ ` _ \| '_ \| | |/ __/ _` |/ _` |/ _` / __|
% | |__| (_) | | | | | | |_) | | | (_| (_| | (_| | (_| \__ \
% \____\___/|_| |_| |_| .__/|_|_|\___\__,_|\__,_|\__,_|___/
% |_|
%
% «complicadas» (to ".complicadas")
\section{Cinco regras complicadas}
% (mdq182 58 "20181126" "Regras de dedução que faltam, estruturas algébricas")
% «by-cases» (to ".by-cases")
\subsection{Demonstrações por casos}
A regra básica é esta aqui, que é baseada na $(L∨)$:
%:
%: Γ,P∨Q,P⊢R Γ,P∨Q,Q⊢R
%: ---------------------(DC)
%: Γ,P∨Q⊢R
%:
%: ^casos
%:
%: Γ,P∨Q,P⊢R Γ,P∨Q,Q⊢R
%: ---------------------(L∨)
%: Γ,P∨Q,Γ,P∨Q,P∨Q⊢R
%: =================(PL)
%: Γ,Γ,P∨Q,P∨Q,P∨Q⊢R
%: =================(CL)
%: Γ,P∨Q⊢R
%:
%: ^casos-2
%:
\pu
$$\ded{casos}
\quad := \quad
\ded{casos-2}
$$
Um exemplo de uso:
%:
%: ======================== ==========================
%: a∈\Z,\Par(a)⊢\Par(a^2+a) a∈\Z,\Impar(a)⊢\Par(a^2+a)
%: ====================== ----------------------------------------------------(DC)
%: a∈\Z⊢\Par(a)∨\Impar(a) a∈\Z,\Par(a)∨\Impar(a)⊢\Par(a^2+a)
%: -----------------------------------------------------------------------(Cut)
%: a∈\Z⊢\Par(a^2+a)
%:
%: ^casos2
%:
\pu
$$\ded{casos2}$$
% (find-es "tex" "minipage")
\begin{minipage}[t]{15em}
\par 1) Suponha $Γ$
\par 2) (...)
\par 3) Suponha $P∨Q$
\par 4) Caso 1: Suponha $P$
\par 5) (...)
\par 6) Então $R$
\par 7) Caso 2: Suponha $Q$
\par 8) (...)
\par 9) Então $R$ \qquad (Fecha 7,4)
\end{minipage}!
%
\qquad
%
\begin{minipage}[t]{20em}
\par 1) Suponha $a∈\Z$
\par 2) (...)
\par 3) Suponha $\Par(a)∨\Impar(a)$
\par 4) Caso 1: Suponha $\Par(a)$
\par 5) (...)
\par 6) Então $\Par(a^2+a)$
\par 7) Caso 2: Suponha $\Impar(a)$
\par 8) (...)
\par 9) Então $\Par(a^2+a)$ \qquad (Fecha 7,4)
\end{minipage}
% (find-es "math" "provas-MD-naufel")
Ainda não consegui encontrar exemplos ou exercícios de demonstração
por casos no Scheinerman. A P1 do Fernando Naufel de 2012.2
(``md-122-p1-manha-gab.pdf'') para a turma da manhã tem vários
exemplos de provas por casos em Fitch.
% «forall-easy» (to ".forall-easy")
\subsection{A regra fácil para o `$∀$'}
A regra fácil para o `$∀$' {\sl escolhe um caso particular}: por
exemplo, a partir de $∀a∈\Z.\Par(a)∨\Impar(a)$ podemos provar
$\Par(3)∨\Impar(3)$ ou $\Par(2k+1)∨\Impar(2k+1)$. Ela é escrita como:
%:
%: ------------(∀FI) ------------------(∀F)
%: ∀x.P⊢P[x:=t] t∈B,∀b∈B.P⊢P[b:=t]
%:
%: ^fa-easy-u ^fa-easy-b
%:
$$\pu\ded{fa-easy-u} \qquad\text{ou}\qquad \ded{fa-easy-b}$$
%
Lembre que no curso nós quase só usamos quantificadores ``limitados'',
como ``$∀b∈B$'', porque os ``ilimitados'' como ``$∀x$'' são abstratos
demais, no sentido de que é difícil calcular expressões com eles;
aliás só usamos quantificadores ilimitados na aula de 8/outubro.
Em alguns lugares --- por exemplo, no artigo da Wikipedia --- algumas
letras, como $x$, sempre são usadas para {\sl variáveis}, e outras,
como $t$, sempre são usadas para ``termos''.
% «forall-hard» (to ".forall-hard")
\subsection{A regra difícil para o `$∀$'}
A regra difícil para o `$∀$' diz que se conseguimos provar $Q(x,y)$
num contexto que não impõe nenhuma restrição para o $y$ então podemos
provar $∀y.Q(x,y)$ a partir disto; a versão limitada dela diz que se
conseguimos provar $Q(x,y)$ num contexto em que a única restrição para
o $y$ seja $y∈B$ então podemos provar $∀y∈B.Q(x,y)$. Escrevendo estas
regras no estilo de LK elas viram:
%:
%: P(x)⊢Q(x,y) P(x)⊢Q(x,y)
%: --------------(∀DI) --------------------(∀D)
%: P(x)⊢∀y.Q(x,y) P(x),y∈B⊢∀y∈B.Q(x,y)
%:
%: ^fa-hard-u ^fa-hard-b
%:
$$\pu\ded{fa-hard-u} \qquad\text{ou}\qquad \ded{fa-hard-b}$$
Na wikipedia essa regra é exposta de um jeito bem mais abstrato:
%
$$\ded{faR}$$
%
onde ``a variável $y$ não aparece livre em $Γ$ ou $Δ$''.
Um exemplo de uso dela parecido com as coisas que estávamos provando
até a P1 é:
%:
%: a∈\Z⊢\Par(a)→\Impar(a+1)
%: --------------------------(∀D)
%: ⊢∀a∈\Z.\Par(a)→\Impar(a+1)
%:
%: ^fa-ex
%:
$$\pu\ded{fa-ex}$$
% «exist-easy» (to ".exist-easy")
\subsection{A regra fácil para o `$∃$'}
A regra fácil para o `$∃$' diz que se conseguimos provar $P(x,t)$ para
algum ``termo'' $t$, por exemplo $t:=3$, ou $t:=x^2$, então a partir
disto conseguimos provar que $∃y.P(x,y)$. Esta é a versão {\sl
ilimitada} da regra; a versão limitada é $(t∈B∧P(x,t))→∃y∈B.P(x,y)$.
No estilo do LK, temos:
%:
%: ------------(∃FI) ------------------(∃F)
%: P[y:=t]⊢∃y.P t∈B,P[y:=t]⊢∃y∈B.P
%:
%: ^ex-easy-u ^ex-easy-b
%:
%:
\pu
$$\ded{ex-easy-u} \qquad\text{ou}\qquad \ded{ex-easy-b}$$
Um exemplo de uso:
%:
%: ===== ------------------------------------(∃F)
%: ⊢5∈\Z 5∈\Z,\Impar(x)[x:=5]⊢∃x∈\Z.\Impar(x)
%: ---------------------------------------------(Cut)
%: Γ⊢\Impar(5) \Impar(x)[x:=5]⊢∃x∈\Z.\Impar(x)
%: -------------------------------------------------
%: Γ⊢∃x∈\Z.\Impar(x)
%:
%: ^ex-easy-ex
%:
%:
$$\pu\ded{ex-easy-ex}$$
% «exist-hard» (to ".exist-hard")
\subsection{A regra difícil para o `$∃$'}
A regra difícil para o `$∃$' é uma espécie de ``Cut'' --- mas ela usa
uma conclusão da forma $∃y∈B.P(y)$ para cortar duas hipótese: $y∈B$ e
$P(y)$. No sistema que nós vimos primeiro ela era assim:
\msk
\par 1) Suponha $Γ$
\par 2) (...)
\par 3) Então $∃y∈B.P(y)$
\par 4) Suponha $y∈B, P(y)$
\par 5) (...)
\par 6) Então $Q$ \qquad (Fecha 4)
\msk
% (mdq182 11 "20180827" "Contextos, suponhas abertos, erros comuns, fecha suponha")
Nós discutimos ``suponhas abertos'' e regras que ``fecham suponhas''
na aula de 27/ago/2018.
Em LK essa regra fica assim:
%:
%: Γ⊢∃y∈B.P(y) Γ,y∈B,P(y)⊢Q
%: --------------------------(∃D)
%: Γ⊢Q
%:
%: ^ex-D
%:
$$\pu\ded{ex-D}$$
A versão ilimitada dela é:
%:
%: Γ⊢∃y.P Γ,P⊢Q
%: --------------(∃DI)
%: Γ⊢Q
%:
%: ^ex-DI
%:
%:
%: Γ,P⊢Q
%: --------(∃L)^*
%: Γ⊢∃y.P Γ,∃y.P⊢Q
%: -----------------(Cut)
%: Γ⊢Q
%:
%: ^ex-DIe
%:
$$\pu
\ded{ex-DI}
\qquad := \qquad
\ded{ex-DIe}
$$
\newpage
% ____ _
% | _ \ ___ ___ _ _ _ __ ___(_)_ ____ _ ___
% | |_) / _ \/ __| | | | '__/ __| \ \ / / _` / __|
% | _ < __/ (__| |_| | | \__ \ |\ V / (_| \__ \
% |_| \_\___|\___|\__,_|_| |___/_| \_/ \__,_|___/
%
% «defs-recursivas» (to ".defs-recursivas")
\section{Definições recursivas}
Os livros de matemática e computação ``pra adultos'' às vezes fazem
umas definições ridiculamente curtas para sequências, funções e
conjuntos e aí supõem que o leitor vai entender essas definições. O
livro da Judith Gersting explica definições recursivas a partir da
p.67; vamos ver alguns exemplos extras mais difíceis e alguns truques
para entender estas definições.
\subsection{Fake binary}
Seja $B:\N→\N$ a função que obedece estas duas condições:
(BP) $∀n∈\N. B(2n)=10·B(n)$
(BI) $∀n∈\N. B(2n+1)=B(2n)+1$
Note que fazendo $n=0$ em (BP) obtemos que $B(0)=0$, e com $n=0$ em
(BI) obtemos $B(1)=1$. Usando $n=1$, $n-2$, etc em (BP) e (BI) obtemos
$B(2)$, $B(3)$, etc. Exercícios: 1) entenda o padrão da função $B$; 2)
descubra o valor de $B(34)$; mostre os passos necessários para
calcular $B(34)$.
\subsection{Módulo}
Seja $\N^+=\setofst{n∈\N}{0<n}$, e seja $M:\Z×\N^+→\N$ a função que
obedece estas duas condições:
(MB) Se $0≤a<b$ então $M(a,b)=a$,
(MM) $M(a+b,b)=M(a,b)$.
Repare que agora não estamos usando `$∀$' e nem dizendo em que
conjuntos os valores de $a$ e $b$ moram --- estamos copiando o que
muitos livros de matemática e computação fazem: estamos deixando tudo
implícito! Tanto em (MB) quanto em (MM) fica implícito que $a∈\Z$ e
$b∈\N^+$.
Exercícios: 1) Use (MB) para calcular $M(0,5), M(1,5), \dots, M(4,5)$;
2) Use (MM) para calcular $M(5,5), M(6,5), \dots$; 3) Use (MM) para
calcular $M(-1,5), M(-2,5), \dots$.
\subsection{Noves}
Seja $D:\N→\N$ a função que obedece estas três condições:
(DZ) $D(0)=0$
(DP) Se $D(n)=n$ então $D(n+1)=10D(n)+9$
(DC) Se $D(n)≠n$ então $D(n+1)=D(n)$
Exercícios: 1) Calcule $D(0), D(1), \dots, D(11)$. 2) Entenda o padrão
e descubra os valores de $D(99), D(100), D(101), \ldots, D(999),
D(1000), D(1001)$.
\subsection{Concatenação de números}
Seja $C:\N×\N→\N$ a função que obedece:
(CD) $C(a,b) = a·(D(b)+1)+b$
Exercícios: 1) Calcule $C(12,345)$; 2) Calcule $C(12,0)$; 3) Calcule
$C(0,12)$.
\subsection{Um conjunto de números}
Seja $S⊆\N$ o conjuntos que obedece:
(S0) $0∈S$,
(S2) Se $n∈S$ então $10n+2∈S$,
(S3) Se $n∈S$ então $10n+3∈S$.
Exercícios: 1) Prove que $23322∈S$; 2) Explique porque não dá pra
provar que $45∈S$.
\subsection{Strings}
\def\str#1{\ensuremath{\text{``{\tt#1}''}}}
\def\Ss#1#2{\mathsf{#1}_\mathsf{#2}}
\def\ED{\Ss ED}
\def\EN{\Ss EN}
\def\EB{\Ss EB}
\def\EM{\Ss EM}
\def\ES{\Ss ES}
O ``Exemplo 23'' na página 70 do livro da Judith define {\sl strings},
que às vezes são chamados de {\sl sequências de caracteres} ou de {\sl
cadeias de caracteres} --- ou só {\sl cadeias} --- em português.
Alguns exemplos de strings: \str{Hello}, \str{1+2}, \str{}, \str{)+}.
Vamos usar `..' (como em Lua) para a operação de concatenação de
strings. Exemplos:
$\str{Hello}..\str{1+2} = \str{Hello1+2}$
\str{}..\str{)+} $=$ \str{)+}
\subsection{Um conjunto de expressões}
Digamos que os conjuntos de strings $\ED$, $\EN$ e $\ES$
obedecem:
(ED) $\str0, \str1, \ldots, \str9 ∈ \ED$
(EN1) Se $d∈\ED$ então $d∈\EN$
(EN2) Se $n∈\EN$ e $d∈\ED$ então $n..d∈\EN$
(ES1) Se $n∈\EN$ então $n∈\ES$
(ES2) Se $s,t∈\ES$ então $s..\str+..t∈\ES$
(ESP) Se $s∈\ES$ então $\str(..s..\str)∈\EN$
Exercícios: 1) Prove que $\str{123}∈\EN$; 2) Prove que $\str{123}∈\ES$
e $\str{123+4+56}∈\ES$; 3) Prove que $\str{(123+4+56)}∈\EN$; 4) Prove
que $\str{(123+4+56)}∈\ES$; 5) Prove que $\str{(123+4+56)+78}∈\ES$.
\subsection{Outro conjunto de expressões}
Vamos {\sl reusar} os símbolos $\ED$, $\EN$ e $\ES$ do item anterior
--- com outro significado.
Digamos que os conjuntos de strings $\ED$, $\EN$, $\EB$, $\EM$ e $\ES$
obedecem:
(ED) $\str0, \str1, \ldots, \str9 ∈ \ED$
(EN1) $d∈\EN$
(EN2) $n..d∈\EN$
(EB1) $n∈\EB$
(EM1) $b∈\EM$
(EM2) $m..\str*..b∈\EM$
(ES1) $m∈\ES$
(ES2) $s..\str+..m∈\ES$
(EBP) $\str(..s..\str)∈\EB$
Agora estamos usando uma convenção no nome das variáveis para deixar a
especificação mais curta. A convenção é:
$d,d',d''∈\ED$
$n,n',n''∈\EN$
$b,b',b''∈\EB$
$m,m',m''∈\EM$
$s,s',s''∈\ES$
\noindent e os `$∀$'s ficam implícitos. Por exemplo, (EM2) por extenso
é:
$∀m∈\EM.∀b∈\EM.m..\str*..b∈\EM$.
Exercícios: 1) prove que $\str{123+4*56+78}∈\ES$; 2) prove que
$\str{(123+4)*56}∈\EM$.
\newpage
\subsection{Valores de expressões}
É fácil ver que os conjuntos $\ED$, $\EN$, $\EB$, $\EM$ e $\ES$ do
item anterior obedecem $\ED⊂\EN⊂\EB⊂\EM⊂\ES$. Vamos definir uma função
$V:\ES→\N$ da seguinte forma:
(VD) $V(\str0)=0, V(\str1)=1, \ldots, V(\str9)=9$
(VN2) $V(n..d)=10V(n)+V(d)$
(VM2) $V(m..\str*..b)=V(m)·V(b)$
(VS2) $V(s..\str+..m)=V(s)·V(m)$
(VP) $V(\str(..s..\str))=V(s)$
% (find-books "__discrete/__discrete.el" "gersting")
% (find-gerstingpage (+ 20 67) "Definições recursivas")
% (find-gerstingpage (+ 20 69) "Conjuntos recursivos")
\end{document}
% Local Variables:
% coding: utf-8-unix
% End: