\documentclass[10pt,a4paper]{article}

% Packages
\usepackage{fancyhdr}           % For header and footer
\usepackage{multicol}           % Allows multicols in tables
\usepackage{tabularx}           % Intelligent column widths
\usepackage{tabulary}           % Used in header and footer
\usepackage{hhline}             % Border under tables
\usepackage{graphicx}           % For images
\usepackage{xcolor}             % For hex colours
%\usepackage[utf8x]{inputenc}    % For unicode character support
\usepackage[T1]{fontenc}        % Without this we get weird character replacements
\usepackage{colortbl}           % For coloured tables
\usepackage{setspace}           % For line height
\usepackage{lastpage}           % Needed for total page number
\usepackage{seqsplit}           % Splits long words.
%\usepackage{opensans}          % Can't make this work so far. Shame. Would be lovely.
\usepackage[normalem]{ulem}     % For underlining links
% Most of the following are not required for the majority
% of cheat sheets but are needed for some symbol support.
\usepackage{amsmath}            % Symbols
\usepackage{MnSymbol}           % Symbols
\usepackage{wasysym}            % Symbols
%\usepackage[english,german,french,spanish,italian]{babel}              % Languages

% Document Info
\author{andreea2823}
\pdfinfo{
  /Title (flp-partial.pdf)
  /Creator (Cheatography)
  /Author (andreea2823)
  /Subject (FLP\_partial Cheat Sheet)
}

% Lengths and widths
\addtolength{\textwidth}{6cm}
\addtolength{\textheight}{-1cm}
\addtolength{\hoffset}{-3cm}
\addtolength{\voffset}{-2cm}
\setlength{\tabcolsep}{0.2cm} % Space between columns
\setlength{\headsep}{-12pt} % Reduce space between header and content
\setlength{\headheight}{85pt} % If less, LaTeX automatically increases it
\renewcommand{\footrulewidth}{0pt} % Remove footer line
\renewcommand{\headrulewidth}{0pt} % Remove header line
\renewcommand{\seqinsert}{\ifmmode\allowbreak\else\-\fi} % Hyphens in seqsplit
% This two commands together give roughly
% the right line height in the tables
\renewcommand{\arraystretch}{1.3}
\onehalfspacing

% Commands
\newcommand{\SetRowColor}[1]{\noalign{\gdef\RowColorName{#1}}\rowcolor{\RowColorName}} % Shortcut for row colour
\newcommand{\mymulticolumn}[3]{\multicolumn{#1}{>{\columncolor{\RowColorName}}#2}{#3}} % For coloured multi-cols
\newcolumntype{x}[1]{>{\raggedright}p{#1}} % New column types for ragged-right paragraph columns
\newcommand{\tn}{\tabularnewline} % Required as custom column type in use

% Font and Colours
\definecolor{HeadBackground}{HTML}{333333}
\definecolor{FootBackground}{HTML}{666666}
\definecolor{TextColor}{HTML}{333333}
\definecolor{DarkBackground}{HTML}{14755F}
\definecolor{LightBackground}{HTML}{F0F6F5}
\renewcommand{\familydefault}{\sfdefault}
\color{TextColor}

% Header and Footer
\pagestyle{fancy}
\fancyhead{} % Set header to blank
\fancyfoot{} % Set footer to blank
\fancyhead[L]{
\noindent
\begin{multicols}{3}
\begin{tabulary}{5.8cm}{C}
    \SetRowColor{DarkBackground}
    \vspace{-7pt}
    {\parbox{\dimexpr\textwidth-2\fboxsep\relax}{\noindent
        \hspace*{-6pt}\includegraphics[width=5.8cm]{/web/www.cheatography.com/public/images/cheatography_logo.pdf}}
    }
\end{tabulary}
\columnbreak
\begin{tabulary}{11cm}{L}
    \vspace{-2pt}\large{\bf{\textcolor{DarkBackground}{\textrm{FLP\_partial Cheat Sheet}}}} \\
    \normalsize{by \textcolor{DarkBackground}{andreea2823} via \textcolor{DarkBackground}{\uline{cheatography.com/182534/cs/38008/}}}
\end{tabulary}
\end{multicols}}

\fancyfoot[L]{ \footnotesize
\noindent
\begin{multicols}{3}
\begin{tabulary}{5.8cm}{LL}
  \SetRowColor{FootBackground}
  \mymulticolumn{2}{p{5.377cm}}{\bf\textcolor{white}{Cheatographer}}  \\
  \vspace{-2pt}andreea2823 \\
  \uline{cheatography.com/andreea2823} \\
  \end{tabulary}
\vfill
\columnbreak
\begin{tabulary}{5.8cm}{L}
  \SetRowColor{FootBackground}
  \mymulticolumn{1}{p{5.377cm}}{\bf\textcolor{white}{Cheat Sheet}}  \\
   \vspace{-2pt}Not Yet Published.\\
   Updated 1st April, 2023.\\
   Page {\thepage} of \pageref{LastPage}.
\end{tabulary}
\vfill
\columnbreak
\begin{tabulary}{5.8cm}{L}
  \SetRowColor{FootBackground}
  \mymulticolumn{1}{p{5.377cm}}{\bf\textcolor{white}{Sponsor}}  \\
  \SetRowColor{white}
  \vspace{-5pt}
  %\includegraphics[width=48px,height=48px]{dave.jpeg}
  Measure your website readability!\\
  www.readability-score.com
\end{tabulary}
\end{multicols}}




\begin{document}
\raggedright
\raggedcolumns

% Set font size to small. Switch to any value
% from this page to resize cheat sheet text:
% www.emerson.emory.edu/services/latex/latex_169.html
\footnotesize % Small font.

\begin{multicols*}{2}

\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{Prerequisites}}  \tn
\SetRowColor{LightBackground}
\mymulticolumn{1}{p{8.4cm}}{\vspace{1px}\centerline{\includegraphics[width=5.1cm]{/web/www.cheatography.com/public/uploads/andreea2823_1680210338_alfabet.png}}} \tn 
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{2.1}}  \tn
\SetRowColor{LightBackground}
\mymulticolumn{1}{p{8.4cm}}{\vspace{1px}\centerline{\includegraphics[width=5.1cm]{/web/www.cheatography.com/public/uploads/andreea2823_1680210308_1.2.png}}} \tn 
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{2.2}}  \tn
\SetRowColor{LightBackground}
\mymulticolumn{1}{p{8.4cm}}{\vspace{1px}\centerline{\includegraphics[width=5.1cm]{/web/www.cheatography.com/public/uploads/andreea2823_1680211016_2.2.png}}} \tn 
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{3.1}}  \tn
\SetRowColor{LightBackground}
\mymulticolumn{1}{p{8.4cm}}{\vspace{1px}\centerline{\includegraphics[width=5.1cm]{/web/www.cheatography.com/public/uploads/andreea2823_1680214587_3.1.png}}} \tn 
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{3.2}}  \tn
\SetRowColor{LightBackground}
\mymulticolumn{1}{p{8.4cm}}{\vspace{1px}\centerline{\includegraphics[width=5.1cm]{/web/www.cheatography.com/public/uploads/andreea2823_1680215733_3.2.png}}} \tn 
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{5.1}}  \tn
\SetRowColor{LightBackground}
\mymulticolumn{1}{p{8.4cm}}{\vspace{1px}\centerline{\includegraphics[width=5.1cm]{/web/www.cheatography.com/public/uploads/andreea2823_1680222993_5.1.png}}} \tn 
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{6.1}}  \tn
\SetRowColor{LightBackground}
\mymulticolumn{1}{p{8.4cm}}{\vspace{1px}\centerline{\includegraphics[width=5.1cm]{/web/www.cheatography.com/public/uploads/andreea2823_1680369619_6.1.png}}} \tn 
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{6.2}}  \tn
\SetRowColor{LightBackground}
\mymulticolumn{1}{p{8.4cm}}{\vspace{1px}\centerline{\includegraphics[width=5.1cm]{/web/www.cheatography.com/public/uploads/andreea2823_1680369726_6.2.png}}} \tn 
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{Quiz-uri}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{1.1. Care ar fi cea mai apropiata scriere in lambda calcul pentru A, unde f(x) = x$^{\textrm{2}}$ + 1 si A = f(2)?} \tn 
\mymulticolumn{1}{x{8.4cm}}{\hspace*{6 px}\rule{2px}{6px}\hspace*{6 px}5 \{\{nl\}\} (x$^{\textrm{2}}$ + 1)(2) \{\{nl\}\}2$^{\textrm{2}}$ + 1\{\{nl\}\} {\bf{(λ x. x$^{\textrm{2}}$ + 1)(2)}}} \tn 
% Row Count 5 (+ 5)
% Row 1
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{1.2. Care din conceptele de mai jos nu este un model de calculabilitate?} \tn 
\mymulticolumn{1}{x{8.4cm}}{\hspace*{6 px}\rule{2px}{6px}\hspace*{6 px}masinile Turing \{\{nl\}\} {\bf{punctele fixe}} \{\{nl\}\}funcțiile recursive \{\{nl\}\}lambda calcul} \tn 
% Row Count 9 (+ 4)
% Row 2
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{1.3. In lambda calcul fara tipuri} \tn 
\mymulticolumn{1}{x{8.4cm}}{\hspace*{6 px}\rule{2px}{6px}\hspace*{6 px}trebuie sa specificam mereu tipul oricarei expresii \{\{nl\}\} sunt eliminate expresiile de forma f(f) \{\{nl\}\} {\bf{nu specificam domeniul/codomeniul functiilor}} \{\{nl\}\}putem avea efecte laterale} \tn 
% Row Count 14 (+ 5)
% Row 3
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{2.1. Care din lambda termenii de mai jos nu este închis?} \tn 
\mymulticolumn{1}{x{8.4cm}}{\hspace*{6 px}\rule{2px}{6px}\hspace*{6 px}λxyz.xxy \{\{nl\}\} λxy.xxy  \{\{nl\}\}{\bf{ λx.xxy}}  \{\{nl\}\} λx.xx} \tn 
% Row Count 18 (+ 4)
% Row 4
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{2.2. Care sunt variabilele libere din termenul λx.xxy?} \tn 
\mymulticolumn{1}{x{8.4cm}}{\hspace*{6 px}\rule{2px}{6px}\hspace*{6 px}termenul nu are variabile libere  \{\{nl\}\} x \{\{nl\}\}{\bf{ y}}  \{\{nl\}\} x și y} \tn 
% Row Count 22 (+ 4)
% Row 5
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{2.3. Care din următoarele afirmații este adevărată?} \tn 
\mymulticolumn{1}{x{8.4cm}}{\hspace*{6 px}\rule{2px}{6px}\hspace*{6 px}un combinator este orice lambda termen \{\{nl\}\} {\bf{un combinator este un lambda termen fără variabile libere (închis) }}\{\{nl\}\} un combinator este un lambda termen cu variabile libere \{\{nl\}\} un combinator este un lambda termen care are și variabile libere, și variabile legate} \tn 
% Row Count 30 (+ 8)
\end{tabularx}
\par\addvspace{1.3em}

\vfill
\columnbreak
\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{Quiz-uri (cont)}}  \tn
% Row 6
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{3.1. Ce este un β-redex?} \tn 
\mymulticolumn{1}{x{8.4cm}}{\hspace*{6 px}\rule{2px}{6px}\hspace*{6 px}un λ-termen de forma M{[}N/x{]} \{\{nl\}\} {\bf{un λ-termen de forma (λx.M)N}} \{\{nl\}\} un λ-termen de forma  (λx.M) \{\{nl\}\} un λ-termen de forma x} \tn 
% Row Count 4 (+ 4)
% Row 7
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{3.2. Ce este o formă normală pentru un λ-termen?} \tn 
\mymulticolumn{1}{x{8.4cm}}{\hspace*{6 px}\rule{2px}{6px}\hspace*{6 px}un λ-redex \{\{nl\}\} cea mai mică β-reducție \{\{nl\}\} o α-echivalență \{\{nl\}\} {\bf{un λ-termen fără redex-uri}}} \tn 
% Row Count 9 (+ 5)
% Row 8
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{3.3. În ce constă strategia normală de evaluare pentru λ-termeni?} \tn 
\mymulticolumn{1}{x{8.4cm}}{\hspace*{6 px}\rule{2px}{6px}\hspace*{6 px}{\bf{alegerea redex-ului cel mai din stânga și apoi cel mai din exterior }} \{\{nl\}\} alegerea redex-ului cel mai din stânga și apoi cel mai din interior \{\{nl\}\} aplicarea unei reduceri în corpul unei abstractizări \{\{nl\}\} nu este definită} \tn 
% Row Count 17 (+ 8)
% Row 9
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{4.1. O codare în lambda calcul pentru constanta booleana true este:} \tn 
\mymulticolumn{1}{x{8.4cm}}{\hspace*{6 px}\rule{2px}{6px}\hspace*{6 px}{\bf{λxy.x}} \{\{nl\}\} λxy.xy\{\{nl\}\} λx.x \{\{nl\}\} nu se poate coda în lambda calcul} \tn 
% Row Count 21 (+ 4)
% Row 10
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{4.2. Codarea numerelor naturale în lambda calcul se mai numește și:} \tn 
\mymulticolumn{1}{x{8.4cm}}{\hspace*{6 px}\rule{2px}{6px}\hspace*{6 px}mașina Turing universală \{\{nl\}\} numerele naturale nu se pot coda în lambda calcul  \{\{nl\}\} {\bf{numeralii Church}} \{\{nl\}\} redex} \tn 
% Row Count 26 (+ 5)
% Row 11
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{4.3. Un lambda termen M este punct fix al unui lambda termen F dacă} \tn 
\mymulticolumn{1}{x{8.4cm}}{\hspace*{6 px}\rule{2px}{6px}\hspace*{6 px}F =ᵦ M \{\{nl\}\} {\bf{F M =ᵦ M}} \{\{nl\}\} M F =ᵦ M \{\{nl\}\} F M =ᵦ F} \tn 
% Row Count 30 (+ 4)
\end{tabularx}
\par\addvspace{1.3em}

\vfill
\columnbreak
\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{Quiz-uri (cont)}}  \tn
% Row 12
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{5.1. Ce înseamnă că un termen M este typable?} \tn 
\mymulticolumn{1}{x{8.4cm}}{\hspace*{6 px}\rule{2px}{6px}\hspace*{6 px}{\bf{există un tip σ astfel încât M să aibă tipul σ }} \{\{nl\}\} există o derivare a lui M \{\{nl\}\} M are o formă normală \{\{nl\}\} M este o abstractizare} \tn 
% Row Count 5 (+ 5)
% Row 13
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{5.2. Care din următorii termeni este typable?} \tn 
\mymulticolumn{1}{x{8.4cm}}{\hspace*{6 px}\rule{2px}{6px}\hspace*{6 px}xx \{\{nl\}\} xxy \{\{nl\}\} {\bf{x(xy)}} \{\{nl\}\} niciunul din termenii de mai sus} \tn 
% Row Count 8 (+ 3)
% Row 14
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{5.3. Ce este o judecată în calculul λ→?} \tn 
\mymulticolumn{1}{x{8.4cm}}{\hspace*{6 px}\rule{2px}{6px}\hspace*{6 px}o expresie de forma M:σ \{\{nl\}\}o expresie de forma x:σ \{\{nl\}\} {\bf{o expresie de forma Γ⊢M:σ}} \{\{nl\}\} o abstractizare} \tn 
% Row Count 12 (+ 4)
% Row 15
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{6.1. Ce înseamnă type checking?} \tn 
\mymulticolumn{1}{x{8.4cm}}{\hspace*{6 px}\rule{2px}{6px}\hspace*{6 px}pentru un termen dat, constă în găsirea unui tip pentru un termen \{\{nl\}\} pentru un termen dat, constă în găsirea unui context pentru un termen \{\{nl\}\} {\bf{pentru un context, termen și tip date, constă în verificarea faptului că termenul poate avea tipul în contextul dat}} \{\{nl\}\} pentru un context și un tip date, constă în găsirea unui tip pentru termen în contextul dat} \tn 
% Row Count 22 (+ 10)
% Row 16
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{6.2.Care din problemele de mai jos nu este decidabilă pentru lambda calcul cu tipuri simple?} \tn 
\mymulticolumn{1}{x{8.4cm}}{\hspace*{6 px}\rule{2px}{6px}\hspace*{6 px}inhabitation \{\{nl\}\} typability \{\{nl\}\} type checking \{\{nl\}\} {\bf{toate de mai sus sunt probleme decidabile}}} \tn 
% Row Count 27 (+ 5)
% Row 17
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{6.3. Care din afirmațiile de mai jos este adevărată pentru tipul Void?} \tn 
\mymulticolumn{1}{x{8.4cm}}{\hspace*{6 px}\rule{2px}{6px}\hspace*{6 px}are un inhabitant numit void \{\{nl\}\}nu poate exista un astfel de tip \{\{nl\}\} {\bf{nu are niciun inhabitant}} \{\{nl\}\} orice termen poate avea tipul Void} \tn 
% Row Count 33 (+ 6)
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{Curs 4}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Expresivitatea λ-calculului}}}}} \tn 
% Row Count 1 (+ 1)
% Row 1
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{Deși lambda calculul constă doar în λ-termeni, putem reprezenta și manipula tipuri de date comune.} \tn 
% Row Count 4 (+ 3)
% Row 2
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Booleeni}}}}} \tn 
% Row Count 5 (+ 1)
% Row 3
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{•T ≜ λxy.x (dintre cele doua alternative o alege pe prima) \{\{nl\}\} •F ≜ λxy.y (dintre cele doua alternative o alege pe a doua) \{\{nl\}\} {\bf{if}} = λbtf.t , if b = true \{\{nl\}\} ~ ~ ~ ~ λbtf.f, if b = false \{\{nl\}\} altfel spus, {\bf{if ≜ λbtf.b t f}} \{\{nl\}\} {\bf{and ≜ λb1b2.if b1 b2}} (sau λb1b2.b2 b1 b2 sau λb1b2.b1 b2 F) \{\{nl\}\} {\bf{or ≜ λb1b2.if b1 T b2}} \{\{nl\}\} {\bf{not ≜ λb1.if b1 F T}} F \{\{nl\}\} Operațiile lucrează corect doar dacă primesc ca argumente valori booleene. Folosind lambda calcul fară tipuri, avem garbage in, garbage out.} \tn 
% Row Count 17 (+ 12)
% Row 4
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Numere naturale}}}}} \tn 
% Row Count 18 (+ 1)
% Row 5
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{Numeralul Church pentru numărul n ∈ N este notat n(bar). \{\{nl\}\} Numeralul Church n(bar) este λ-termenul λfx.f\textasciicircum{}n\textasciicircum{}x, unde f\textasciicircum{}n\textasciicircum{} reprezintă compunerea lui f cu ea însăși de n ori. Avem deci {\bf{n ≜ λfx.f\textasciicircum{}n\textasciicircum{}x}}. \{\{nl\}\} Definim {\bf{Succ ≜ λnfx.f (n f x)}} \{\{nl\}\}  ~ ~ ~ ~{\bf{add ≜ λmnfx.m f (n f x)}} \{\{nl\}\}  ~ ~ ~ ~{\bf{add′ ≜ λmn.m {\emph{Succ}} n}} \{\{nl\}\}  ~ ~ ~ ~{\bf{mul ≜ λmn.m (add n) 0(bar)}} \{\{nl\}\}  ~ ~ ~ ~{\bf{exp ≜ λmn.m (mul n) 1(bar)}} \{\{nl\}\}  ~ ~ ~ ~{\bf{isZero ≜ λnxy.n (λz.y) x}}} \tn 
% Row Count 30 (+ 12)
\end{tabularx}
\par\addvspace{1.3em}

\vfill
\columnbreak
\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{Curs 4 (cont)}}  \tn
% Row 6
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Puncte fixe în lambda-calcul}}}}} \tn 
% Row Count 1 (+ 1)
% Row 7
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{Dacă F și M sunt λ-termeni, spunem că M este un {\emph{punct fix}} al lui F dacă F M =β M. \{\{nl\}\} {\bf{{\emph{Thm:}} În lambda calculul fără tipuri, orice termen are un punct fix.}}} \tn 
% Row Count 5 (+ 4)
% Row 8
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Combinatori de punct fix}}}}} \tn 
% Row Count 6 (+ 1)
% Row 9
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{= termeni închiși care „construiesc" un punct fix pentru un termen arbitrar. \{\{nl\}\} {\emph{Exemple:}} \{\{nl\}\} {\emph{Combinatorul de punct fix al lui Curry:}} {\bf{Y ≜ λy.(λx.y (x x)) (λx.y (x x))}} (YF punct fix al lui F, pt orice teremn F, deoarece {\bf{{\emph{Y}}F ↠β F ({\bf{Y}} F)}}) \{\{nl\}\} {\emph{Combinatorul de punct fix al lui Turing:}} {\bf{Θ ≜ (λxy.y (x x y)) (λxy.y (x x y))}} (ΘF punct fix al lui F, pt orice termen F, deoarece{\emph{ΘF ↠β F (Θ F)}})} \tn 
% Row Count 15 (+ 9)
% Row 10
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Rezolvarea de ecuații în lambda calcul}}}}} \tn 
% Row Count 16 (+ 1)
% Row 11
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{{\emph{fact n = if(isZero n) (1) (mul n (fact(pred n)) )}} \{\{nl\}\} {\emph{fact = λn.if(isZero n) (1) (mul n (fact(pred n)) )}} \{\{nl\}\} {\emph{fact = (λfn.if(isZero n) (1) (mul n (f(pred n)) ))fact}} \{\{nl\}\} Notăm F = {\emph{λfn.if(isZero n) (1) (mul n (f(pred n)) )}} \{\{nl\}\} Ultima ecuat,  ie devine{\bf{ fact = F fact}}, o ecuație de punct fix. \{\{nl\}\} Luăm deci {\bf{fact ≜ Y F}}, adică {\bf{fact ≜ Y (λfn.if(isZero n) (1) (mul n (f(pred n)) ))}}} \tn 
% Row Count 25 (+ 9)
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{Curs 1}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{Ce este o funcție în matematică?}} \{\{bb=1\}\}} \tn 
% Row Count 1 (+ 1)
% Row 1
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{extensional}}}}: „funcții prin grafice", clasă mai largă de funcții, cuprinde și funcții care nu pot fi definite prin formule \{\{nl\}\}~~~(domeniu și codomeniu fixate, funcția e o mulțime de perechi -\textgreater{} duce intrări în ieșiri)\{\{nl\}\}~~{\emph{funcții extensional egale}} = pentru aceeași intrare obțin aceeași ieșire ({\emph{f(x) = g(x), ∀x∈ X}}) \{\{nl\}\}  {\bf{{\emph{intensional}}}}: „funcții ca formule" (nu e mereu necesar să știm domeniul și codomeniul; paradigmă utilă în informatică-\textgreater{}un program = o fcț de la intrări la ieșiri) \{\{nl\}\} ~~ {\emph{funcții intensional egale}}: definite prin acceași formulă (eventual prelucrată)\{\{nl\}\} \{\{bb=1\}\}} \tn 
% Row Count 15 (+ 14)
% Row 2
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{Lambda calcul}} \{\{bb=1\}\}} \tn 
% Row Count 16 (+ 1)
% Row 3
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{lambda calcul}}}} = teorie a {\emph{funcțiilor ca formule}} \{\{nl\}\}{\emph{Exemplu}}: λx.x\textasciicircum{}2\textasciicircum{} = x-\textgreater{}x\textasciicircum{}2\textasciicircum{} (e expresie, nu instrucțiune/declarație)\{\{nl\}\} ~~~Variabila {\bf{x}} este {\emph{locală/legată}} în termenul λx.x\textasciicircum{}2\textasciicircum{} \{\{nl\}\}{\emph{Exemplu}}: {\emph{f◦f}} = λx.f(f(x)) \{\{nl\}\}~~~~~~~~~~~~~~ {\emph{f→f◦f}} = λf.λx.f(f(x)) \{\{nl\}\}~~~~~~~~~~~~~~((λf.λx.f(f(x)))(λy.y\textasciicircum{}2\textasciicircum{}))(5) = 625 \{\{nl\}\} Funcția identitate f = λx.x are tipul X-\textgreater{}X, unde X poate să fie orice mulțime \{\{nl\}\} Funcția g = λf.λx.f(f(x)) are tipul (X-\textgreater{}X)-\textgreater{}(X-\textgreater{}X)\{\{nl\}\}f(f) ≃ (λx.x)(λx.x) ≃ λx.x ≃ f \{\{nl\}\} Combinatorul ω = λx.xx care reprezintă funcția care aplică x lui x\{\{nl\}\} ~~ω(λy.y) ≃ (λx.xx)(λy.y) ≃ (λy.y)(λy.y) ≃ (λy.y) \{\{nl\}\} ω =λx.x(x), ω(ω) = ? \{\{nl\}\} ω(f) = f(f), for any f that belongs to its domain. So ω(ω) = ω(ω) and cannot be further evaluated \{\{bb=1\}\}} \tn 
% Row Count 37 (+ 21)
\end{tabularx}
\par\addvspace{1.3em}

\vfill
\columnbreak
\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{Curs 1 (cont)}}  \tn
% Row 4
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{Lambda calcul fără tipuri:}} \{\{nl\}\}} \tn 
% Row Count 1 (+ 1)
% Row 5
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{-{}- nu specificăm tipul niciunei expresii \{\{nl\}\} -{}- nu specificăm domeniul/codomeniul funcțiilor \{\{nl\}\} -{}- flexibilitate maximă, dar riscant deoarece putem ajunge în situații în care încercăm să aplicăm o funcție unui argument pe care nu îl poate procesa \{\{bb=1\}\}} \tn 
% Row Count 7 (+ 6)
% Row 6
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{Lambda calcul cu tipuri simple}} \{\{nl\}\}} \tn 
% Row Count 8 (+ 1)
% Row 7
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{-{}- specificăm mereu tipul oricărei expersii \{\{nl\}\} -{}- nu putem aplica funcții unui argument care are alt tip față de denumirea funcției \{\{nl\}\} -{}- expresii de forma {\emph{f(f)}} sunt eliminate, chiar dacă f e funția identitate\{\{bb=1\}\}} \tn 
% Row Count 13 (+ 5)
% Row 8
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{Lambda calcul cu tipuri polimorfice}}\{\{nl\}\}} \tn 
% Row Count 14 (+ 1)
% Row 9
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{-{}- o situație intermediară între cele două de mai sus \{\{nl\}\} -{}- putem specifica că o expresie are tipul X-\textgreater{}X, dar fără a specifica cine este X\{\{bb=1\}\}} \tn 
% Row Count 18 (+ 4)
% Row 10
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{Calculabilitate}}} \tn 
% Row Count 19 (+ 1)
% Row 11
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{{\emph{informal}}: o funcție este calculabilă dacă există o metodă „pen-and-paper" care permite calcularea lui {\emph{f(n)}}, pentru orice n \{\{nl\}\}{\bf{{\emph{Turing}}}} - a definit un calculator ideal numit {\emph{mașina Turing}} și a postulat că o funcție este calculabilă ddacă poate fi calculată de o astfel de mașină \{\{nl\}\}{\bf{{\emph{Godel}}}} - a definit clasa {\emph{funcțiilor recursive}} și a postualt că o funcție este calculabilă ddacă este o funcție recursivă \{\{nl\}\}{\bf{{\emph{Church}}}} - a definit un limbaj de programare ideal numit {\emph{lambda calcul}} și a postulat că o funcție este calculabilă ddacă poate fi scrisă ca un labda termen \{\{nl\}\} {\bf{Teza Church-Turing}} - cele 3 metode sunt echivalente și coincid cu noțiunea intuitivă de calculabilitate} \tn 
% Row Count 34 (+ 15)
\end{tabularx}
\par\addvspace{1.3em}

\vfill
\columnbreak
\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{Curs 1 (cont)}}  \tn
% Row 12
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Ce este o demonstrație?}}}}} \tn 
% Row Count 1 (+ 1)
% Row 13
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{{\emph{Logica clasică}}: plecând de la niște presupuneri, este suficient să ajungi la o contradicție \{\{nl\}\} {\emph{Logica constructivă}}: pentru a arăta că un obiect există, trebuie să îl construim explicit \{\{nl\}\} - legătura dintre lambda calcul și logica constructivă este dată de paradigma „proof-as-programs" (o demonstrație trebuie să fie o construcție, un program; lambda calculul este o notație pentru un astfel de program)} \tn 
% Row Count 10 (+ 9)
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{Curs 2}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Lambda Calcul}}}}} \tn 
% Row Count 1 (+ 1)
% Row 1
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{•Un model de calculabilitate \{\{nl\}\}•Limbajele de programare funcțională sunt extensii ale sale \{\{nl\}\}•Un limbaj formal \{\{nl\}\} •Expresiile din acest limbaj se numesc {\emph{lambda termeni}} \{\{nl\}\}} \tn 
% Row Count 5 (+ 4)
% Row 2
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Lambda termeni}}}}} \tn 
% Row Count 6 (+ 1)
% Row 3
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{Fie V o mulțime infinită de variabile, notate {\emph{x, y, z,...}}. \{\{nl\}\} Mulțimea {\emph{lambda termenilor}} este dată de următoarea formă BNF: \{\{nl\}\} ~ ~ {\bf{lambda termen = variabilă | aplicare | abstractizare }} \{\{nl\}\} ~ ~{\emph{M, N ::= x | (M N) | (λx.M)}} \{\{nl\}\} {\emph{Definiție alternativă:}} \{\{nl\}\} Fie V o mulțime infinită de variabile, notate {\emph{x, y, z, ...}}. \{\{nl\}\} Fie A un alfabet format din elementele din V și simboluri speciale {\emph{(, ), λ, .}}. \{\{nl\}\} Fie A{\emph{ mulțimea tuturor cuvintelor finite pentru alfabetul A. \{\{nl\}\} Mulțimea {\bf{lambda termenilor}} este cea mai mică submulțime Λ ⊆ A}} astfel încât: \{\{nl\}\} ~ ~ {\emph{{[}Variabila{]}}} V ⊆ Λ \{\{nl\}\} ~ ~ {\emph{{[}Aplicare{]}}} dacă M, N ∈ Λ atunci (M N) ∈ Λ \{\{nl\}\} ~ ~ {\emph{{[}Abstractizare{]}}} dacă x ∈ V și M ∈ Λ atunci (λx.M) ∈ Λ} \tn 
% Row Count 23 (+ 17)
% Row 4
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Convenții}}}}} \tn 
% Row Count 24 (+ 1)
% Row 5
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{•Se elimină parantezele exterioare. \{\{nl\}\} • Aplicarea este asociativa la stânga ({\emph{M N P = (M N P)}}, {\emph{f x y z = ((f x) y) z}}) \{\{nl\}\} • Corpul abstractizării (partea de după punct) se extinde la dreapta cât se poate ({\emph{λx.M N}} = {\emph{λx.(M N)}}, nu {\emph{(λx.M) N}}) \{\{nl\}\} • Mai mulți λ pot fi comprimați ({\emph{λxyz.M = λx.λy.λz.M}}) \{\{nl\}\} {\emph{Exemple:}} \{\{nl\}\} ~ ~ {\emph{(λx.(λy.(λz.((x z)(y z))))) = λxyz.x z (y z)}} \{\{nl\}\} ~ ~ {\emph{(((a b) (c d)) ((e f) (g h))) = a b (c d) (e f (g h))}} \{\{nl\}\} ~ ~ {\emph{x x x x = (((x x) x) x)}} \{\{nl\}\} ~ ~ {\emph{λx.x λy.y = (λx.(x (λy.y)))}}} \tn 
% Row Count 37 (+ 13)
\end{tabularx}
\par\addvspace{1.3em}

\vfill
\columnbreak
\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{Curs 2 (cont)}}  \tn
% Row 6
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Variabile libere și variabile legate}}}}} \tn 
% Row Count 1 (+ 1)
% Row 7
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{{\bf{λx.N}}, unde \{\{nl\}\} ~ ~ λ\_.\_ = operator de legare (binder) \{\{nl\}\} ~ ~ x (din λx.\_) = variabilă de legare (binding) \{\{nl\}\} ~ ~ N = domeniul (scope) de legare a lui x \{\{nl\}\} •toate aparițiile lui x în N sunt legate. \{\{nl\}\} • o apariție care nu este legată se numește {\emph{liberă}} \{\{nl\}\} •un termen fără variabile libere se numește închis (combinator). \{\{nl\}\}{\emph{Exemplu:}} M ≡ (λx.xy) (λy.yz) \{\{nl\}\} ~ ~ x este legată \{\{nl\}\} ~ ~ z este liberă, \{\{nl\}\} ~ ~ y are o apariție legată și una liberă \{\{nl\}\} ~ ~ mulțimea variabilelor libere ale lui M este \{y, z\}.} \tn 
% Row Count 14 (+ 13)
% Row 8
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Variabile libere}}}}} \tn 
% Row Count 15 (+ 1)
% Row 9
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{Mulțimea {\emph{variabilelor libere}} dintr-un termen M este notată {\emph{FV(M)}} și este definită prin:\{\{nl\}\} ~ ~ FV(x) = \{x\} \{\{nl\}\} ~ ~ FV(M N) = FV(M) ∪ FV(N), \{\{nl\}\} ~ ~FV(λx.M) = FV(M)\textbackslash{}\{x\}} \tn 
% Row Count 20 (+ 5)
% Row 10
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Redenumire de variabile}}}}} \tn 
% Row Count 21 (+ 1)
% Row 11
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{Dacă x, y sunt variabile și M este un termen, M\textless{}y/x\textgreater{} este rezultatul obținut după redenumirea lui x cu y în M. \{\{nl\}\} ~ ~ x\textless{}y/x\textgreater{}≡ y, z\textless{}y/x\textgreater{}≡ z, dacă x != z  \{\{nl\}\} ~ ~ (M N)\textless{}y/x\textgreater{} ≡ (M\textless{}y/x\textgreater{}) (N\textless{}y/x\textgreater{}),  \{\{nl\}\} ~ ~ (λx.M)\textless{}y/x\textgreater{} ≡ λy.(M\textless{}y/x\textgreater{}),  \{\{nl\}\} ~ ~ (λz.M)\textless{}y/x\textgreater{} ≡ λz.(M\textless{}y/x\textgreater{}), dacă x != z} \tn 
% Row Count 28 (+ 7)
% Row 12
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{α-echivalență}}}}} \tn 
% Row Count 29 (+ 1)
% Row 13
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{α-echivalența = cea mai mică relație de congruenșă  =α pe mulțimea lambda termenilor, aî pentru orice termen M și orice variabilă y care nu apare în M, avem λx.M =α λy.(M\textless{}y/x\textgreater{}) \{\{nl\}\} -{}- cea mai mică relație pe lambda termeni care satisface regulile: \{\{nl\}\}~ \&nbsp {\emph{vezi poza din cardul 2.1}} \{\{nl\}\} {\emph{Convenția Barendregt:}} variabilele legate sunt redenumite pt a fi distincte.} \tn 
% Row Count 37 (+ 8)
\end{tabularx}
\par\addvspace{1.3em}

\vfill
\columnbreak
\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{Curs 2 (cont)}}  \tn
% Row 14
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Substituții}}}} (card 2.2)} \tn 
% Row Count 1 (+ 1)
% Row 15
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{M{[}N/x{]} este rezultatul obținut dupa înlocuirea lui  x cu N în M. \{\{nl\}\}{\emph{Cazuri speciale:}} \{\{nl\}\} 1. Înlocuim doar variabile libere: x (λxy.x){[}N/x{]} = N (λxy.x), nu N (λxy.N) sau N (λNy.N). \{\{nl\}\} 2.Nu vrem sa legăm variabile libere neintenționat:M ≡ λx.y x, N ≡ λz.x z (x legată în M și lilberă în N). {\emph{Redenumim variabilele legate înainte de substituție!}} \{\{nl\}\} ~M{[}N/y{]} = (λx'.y x'){[}N/y{]} = λx'.N x'= λx'.(λz.x z) x'} \tn 
% Row Count 10 (+ 9)
% Row 16
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Exemple}}}}} \tn 
% Row Count 11 (+ 1)
% Row 17
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{(λz.x){[}y/x{]} = λz.y \{\{nl\}\} (λy.x){[}y/x{]} = λy'.y, nu λy.y, \{\{nl\}\}(λy.x){[}(λz.z w)/x{]} = λyz.zw} \tn 
% Row Count 13 (+ 2)
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{Curs 3}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{β-reducții}}}} (card 3.1)} \tn 
% Row Count 1 (+ 1)
% Row 1
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{{\emph{Convenție:}} M=N (2 termeni egali) dacă sunt α-echivalenți. \{\{nl\}\} {\bf{β-reducție}} = procesul de a evalua lambda termeni prin „pasarea de argumente funcțiilor" \{\{nl\}\} {\bf{β-redex}} = un termen de forma (λx.M) N \{\{nl\}\} {\bf{redusul}} unui redex (λx.M) N este M{[}N/x{]} \{\{nl\}\} Reducem lambda termeni prin găsirea unui subtermen care este redex și apoi înlocuirea acelui redex cu redusul său; repetăm acest proces până nu mai sunt redexuri \{\{nl\}\} {\bf{forma normală}} = un lambda termen fără redexuri \{\{nl\}\} {\emph{Observații:}} \{\{nl\}\} ~ ~•reducerea unui redex poate crea noi redex-uri/șterge alte redex-uri \{\{nl\}\} ~ ~ • numărul de pași necesari pâna a atinge o fn poate varia, în funcție de ordinea în care sunt reduse redex-urile, iar rezultatul final nu depinde de alegerea redex-urilor \{\{nl\}\} ~ ~ •lungimea unui termen nu trebuie să scadă în procesul de β-reducție; poate crește sau rămâne neschimbat.} \tn 
% Row Count 21 (+ 20)
% Row 2
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{β-forma normală}}}}} \tn 
% Row Count 22 (+ 1)
% Row 3
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{{\emph{(λx.x x) (λx.x x)}} nu poate fi redus la o β-formă normală (evaluarea nu se termină) \{\{nl\}\} Există lambda termeni care deși pot fi reduși la o formă norală, pot să nu o atingă niciodată (contează {\emph{strategia de evaluare}}). \{\{nl\}\} Notăm cu M -»β M' faptul că M poate fi β-redus până în M' în 0 sau mai mulți pași ({\emph{închiderea reflexivă și tranzitivă a relației →β}}) \{\{nl\}\} Notăm cu {\emph{M =β M′}} faptul că M poate fi transformat în M′ în 0 sau mai mulți pași de β-reducție, transformare în care pașii de reducție pot fi și întorși. \{\{nl\}\} =β este închiderea reflexivă, simetrică și tranzitivă a relației →β. \{\{nl\}\} M este {\bf{slab normalizabil}} (weakly normalising) dacă există N în forma normală aî M -»β N. \{\{nl\}\} M este {\bf{puternic normalizabil}} (strong normalising) dacă nu există reduceri infinite care încep din M. \{\{nl\}\} puternic normalizabil =\textgreater{} slab normalizabil \{\{nl\}\}{\emph{Exemple:}} \{\{nl\}\} ~ ~ (λx.y) ((λz.zz ) (λw.w)) - puternic normalizabil.\{\{nl\}\} ~ ~(λxy.y) ((λx.x x) (λx.x x)) (λz.z) - slab normalizabil, dar nu puternic normalizabil.} \tn 
% Row Count 45 (+ 23)
\end{tabularx}
\par\addvspace{1.3em}

\vfill
\columnbreak
\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{Curs 3 (cont)}}  \tn
% Row 4
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Confluența β-reducției. Teorema Church-Rosser}}}}} \tn 
% Row Count 2 (+ 2)
% Row 5
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{Card 3.2} \tn 
% Row Count 3 (+ 1)
% Row 6
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\emph{*}}Exemple} \tn 
% Row Count 4 (+ 1)
% Row 7
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{(λx.x) M -»β M \{\{nl\}\} (λxy.x) M N -»β M \{\{nl\}\} (λx.x x) (λy.y y y) -»β (λy.y y y) (λy.y y y) (λy.y y y). . .} \tn 
% Row Count 7 (+ 3)
% Row 8
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Strategii de evaluare}}}}} \tn 
% Row Count 8 (+ 1)
% Row 9
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{Lambda calculul nu specifică o strategie de evaluare, fiind {\emph{nedeterminist}} \{\{nl\}\} {\bf{Strategia normală = leftmost-outermost}} (alegem redex-ul cel mai din stânga și apoi cel mai din exterior) \{\{nl\}\} ~ dacă M1 și M2 sunt redex-uri și M1 este un subtermen al lui M2, atunci M1 nu va fi um redex ales. \{\{nl\}\} ~ printre redex-urile care nu sunt subtermeni ai altor redex-uri (și sunt incompatibili față de relația de subtermen), îl alegem pe cel mai din stânga. \{\{nl\}\} {\emph{Dacă un termen are o formă normală, atunci strategia normală va converge la ea.}} \{\{nl\}\} {\bf{Strategia aplicativă = leftmost-innermost}} (alegem redex-ul cel mai din stânga și apoi cel mai din interior) \{\{nl\}\} ~ dacă M1 și M2 sunt redex-uri și M1 este un subtermen al lui M2, atunci M2 nu va fi următorul redex ales \{\{nl\}\} ~ printre redex-urile care nu sunt subtermeni ai altor redex-uri (și sunt incompatibili față de relația de subtermen), îl alegem pe cel mai din stânga.} \tn 
% Row Count 28 (+ 20)
% Row 10
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Strategii în programare funcțională}}}}} \tn 
% Row Count 29 (+ 1)
% Row 11
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Call-by-Name (CBN)}}}} = strategia normală fără a face reduceri în corpul unei λ-abstractizări. \{\{nl\}\} {\bf{Call-by-Value (CBV)}} = strategia aplicativă fără a face reduceri în corpul unei λ-abstractizări (folosit în general de limbajele de progr funcțională, excepție Haskell, e o formă de evaluare leneșă). \{\{nl\}\} O {\emph{valoare}} este un λ-term pt care nu există  β-reducții date de strategia de evaluare considerată.} \tn 
% Row Count 38 (+ 9)
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{Curs 5}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Tipuri simple}}}}} \tn 
% Row Count 1 (+ 1)
% Row 1
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{Fie V = \{α, β, γ, ...\} o mulțime infinită de {\emph{tipuri variabilă}}. \{\{nl\}\} Mulțimea tuturor {\emph{tipurilor simple}} T este definită prin:\{\{nl\}\} ~ ~{\bf{T = V | T → T}} \{\{nl\}\} • ({\emph{Tipul variabilă}})  Dacă α ∈ V, atunci α ∈ T. \{\{nl\}\} • ({\emph{Tipul săgeată}})  Dacă σ, τ ∈ T, atunci (σ → τ) ∈ T. \{\{nl\}\} Tipurile săgeată reprezintă {\emph{tipuri pentru funcții}} cum ar fi {\emph{Nat-\textgreater{}Real}} (fct de la nr nat la nr reale) sau {\emph{(Nat -\textgreater{}Int)-\textgreater{}(Int-\textgreater{}Nat)}} (fcț care au ca intrare o fcț de la nr nat la nr întregi li produce o fcț de la întregi la nat) \{\{nl\}\} {\emph{Parantezele în tipurile săgeată sunt asociative la dreapta.}}} \tn 
% Row Count 14 (+ 13)
% Row 2
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Termeni și tipuri}}}}} \tn 
% Row Count 15 (+ 1)
% Row 3
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{M are tip σ: {\emph{M :σ}} \{\{nl\}\} {\bf{Variabilă}} x :σ. Pp că orice var din M are tip unic (Dacă x :σ și x : τ, atunci σ ≡ τ) \{\{nl\}\} {\bf{Aplicare}}: Dacă M :σ → τ și N:σ, atunci M N : τ. \{\{nl\}\} {\bf{Abstractizare}} Dacă x :σ și M : τ, atunci λx. M :σ → τ. \{\{nl\}\} M {\emph{are tip}} (este typeable) daca există un tip σ astfel încât M :σ. \{\{nl\}\}} \tn 
% Row Count 23 (+ 8)
% Row 4
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Metode de a asocia tipuri variabilelelor}}}}} \tn 
% Row Count 24 (+ 1)
% Row 5
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{{\emph{Asocierea explicită (Church-typing)}}: \{\{nl\}\} ~ ~ •constă în prescierea unui unic tip pt fiecare variabilă, la introducerea acesteia (tipuri stabilite explicit) \{\{nl\}\} {\emph{Asocierea implicită (Curry-typing)}}: \{\{nl\}\}~ ~ • constă în a nu prescrie un tip pt fiecare variabilă, ci în a le lăsa „deschise" (teremenii typeable sunt descoperiți printr-un proces de căutare).} \tn 
% Row Count 33 (+ 9)
\end{tabularx}
\par\addvspace{1.3em}

\vfill
\columnbreak
\begin{tabularx}{8.4cm}{X}
\SetRowColor{DarkBackground}
\mymulticolumn{1}{x{8.4cm}}{\bf\textcolor{white}{Curs 5 (cont)}}  \tn
% Row 6
\SetRowColor{LightBackground}
\mymulticolumn{1}{x{8.4cm}}{{\bf{{\emph{Sistem de deducție pentru Church λ→}}}} (card 5.1)} \tn 
% Row Count 2 (+ 2)
% Row 7
\SetRowColor{white}
\mymulticolumn{1}{x{8.4cm}}{Mulțimea {\bf{λ-termenilor cu pre-tipuri ΛT}} este: {\emph{ΛT = x | ΛT ΛT | λx : T. ΛT. \{\{nl\}\} O {\bf{afirmație}} este o expresie de forma M :σ, unde M ∈ ΛT și σ ∈ T (M = }}subiect{\emph{, σ =}}tip{\emph{). \{\{nl\}\} O {\bf{declarație}} este o afirmație în care subiectul e variabilă (}}x :σ*). \{\{nl\}\} Un {\bf{context}} este o listă de declarații cu subiecți diferiți. \{\{nl\}\} O {\bf{judecată}} este o expresie de forma Γ ⊢ M :σ, unde Γ este context și M :σ este o afirmație.} \tn 
% Row Count 12 (+ 10)
\hhline{>{\arrayrulecolor{DarkBackground}}-}
\end{tabularx}
\par\addvspace{1.3em}

\begin{tabularx}{8.4cm}{x{4 cm} x{4 cm} }
\SetRowColor{DarkBackground}
\mymulticolumn{2}{x{8.4cm}}{\bf\textcolor{white}{Curs 6}}  \tn
% Row 0
\SetRowColor{LightBackground}
\mymulticolumn{2}{x{8.4cm}}{{\bf{{\emph{Ce probleme putem să rezolvăm în teoria tipurilor? }}}}} \tn 
% Row Count 2 (+ 2)
% Row 1
\SetRowColor{white}
\mymulticolumn{2}{x{8.4cm}}{{\emph{Type Checking}} \{\{nl\}\} Se reduce la a verifica că putem găsi o derivare pentru \{\{nl\}\} ~ ~ {\emph{context ⊢ term : type}} \{\{nl\}\}{\emph{Well-typedness (Typability):}} \{\{nl\}\} Se reduce la a verifica dacă un termen e legal. \{\{nl\}\} ~ ~ {\emph{? ⊢ term : ?}} \{\{nl\}\}  O variațiune a problemei este {\emph{Type Assignment}} în care este dat contextul și trebuie găsit tipul. \{\{nl\}\} ~~ context ⊢ term : ? \{\{nl\}\} {\emph{Term Finding (Inhabitation)}} \{\{nl\}\} Dându-se un context și un tip, să se stabilească dacă există un termen cu ac tip, în contextul dat \{\{nl\}\} ~~ context ⊢ ? : type \{\{nl\}\} {\emph{!Toate aceste probleme sunt decidabile pentru calculul Church λ→!}}} \tn 
% Row Count 16 (+ 14)
% Row 2
\SetRowColor{LightBackground}
\mymulticolumn{2}{x{8.4cm}}{{\bf{{\emph{Limitări ale lambda-calculului cu tipuri simple}}}}} \tn 
% Row Count 18 (+ 2)
% Row 3
\SetRowColor{white}
\mymulticolumn{2}{x{8.4cm}}{•nu mai avem recursie nelimitată, dar avem recursie primitivă (looping cu număr cunoscut de iterații) \{\{nl\}\} •tipurile pot fi prea restrictive (soluții posibile: {\emph{let-polymorphism}}, unde variabilele libere se redenumesc la fiecare folosire; {\emph{cuantificatori de tipuri}} operatorul de legare Π)} \tn 
% Row Count 25 (+ 7)
% Row 4
\SetRowColor{LightBackground}
\mymulticolumn{2}{x{8.4cm}}{{\bf{{\emph{Corespondența Curry-Howard}}}} (card 6.1, 6.2)} \tn 
% Row Count 26 (+ 1)
% Row 5
\SetRowColor{white}
{\bf{Teoria Tipurilor}} & {\bf{Logică}} \tn 
% Row Count 27 (+ 1)
% Row 6
\SetRowColor{LightBackground}
∘ tipuri \{\{nl\}\} ∘ termeni \{\{nl\}\} ∘ inhabitation a tipului σ & ∘formule \{\{nl\}\} ∘ demonstrații \{\{nl\}\} ∘ demonstrație a lui σ \tn 
% Row Count 31 (+ 4)
\end{tabularx}
\par\addvspace{1.3em}

\vfill
\columnbreak
\begin{tabularx}{8.4cm}{x{4 cm} x{4 cm} }
\SetRowColor{DarkBackground}
\mymulticolumn{2}{x{8.4cm}}{\bf\textcolor{white}{Curs 6 (cont)}}  \tn
% Row 7
\SetRowColor{LightBackground}
∘ tip produs \{\{nl\}\} ∘ tip funcție \{\{nl\}\} ∘ tip sumă \{\{nl\}\} ∘ tipul void \{\{nl\}\} ∘ tipul unit & ∘ conjuncție \{\{nl\}\} ∘ implicație \{\{nl\}\} ∘ disjuncție \{\{nl\}\} ∘ false \{\{nl\}\} ∘ true \tn 
% Row Count 6 (+ 6)
% Row 8
\SetRowColor{white}
\mymulticolumn{2}{x{8.4cm}}{{\bf{{\emph{Logica Intuiționistă}}}}} \tn 
% Row Count 7 (+ 1)
% Row 9
\SetRowColor{LightBackground}
\mymulticolumn{2}{x{8.4cm}}{∘ logică constructivă, bazată pe {\emph{demonstrație}} \{\{nl\}\} ∘ demonstrațiile sunt executabile și produc exemple \{\{nl\}\} Urm formule echiv nu sunt demonstrabile în logica intuiționistă: \{\{nl\}\} ~ ~ {\emph{¬¬φ ⊃ φ}} (dubla negație)\{\{nl\}\} ~ ~ {\emph{φ ∨ ¬φ}} (excluded middle)\{\{nl\}\} ~ ~{\emph{((φ ⊃ τ) ⊃ φ) ⊃ φ}} (legea lui Pierce) \{\{nl\}\} Nu există semantică cu tabele de adevăr pentru logica intuiționistă! \{\{nl\}\} {\emph{Inițial, corespondența Curry-Howard a fost între: (Calcul Church λ →) și (Sistemul de deducție naturală al lui Gentzen pentru logica intuiționistă)}}} \tn 
% Row Count 20 (+ 13)
\hhline{>{\arrayrulecolor{DarkBackground}}--}
\end{tabularx}
\par\addvspace{1.3em}


% That's all folks
\end{multicols*}

\end{document}