2023.2 λ Topics in Denotational Semantics of Programming Languages (IMD0104)

Contact:thanos@imd.ufrn.br (though you should use Zulip instead)
Horários de aula: 24T12 [13h15–14h55]
Sala: A303
Monitoria/TA: fmc.imd.ufrn.br
Older semesters: ..

Info

Prereqs

  • {will, time} to {study, research, hack}
  • some mathematical maturity™: you should be able to reason and to express mathematical ideas in natural mathematical language using appropriate notation and nomenclature;
  • you must have learned well the main subjects of FMC1 and FMC2—do contact me if you are unsure, especially given the weak (or inexistent) grading that frequently takes place in this department;
    • familiarity with the general ideas and tools of structural induction and recursion (see IRI);
    • familiarity with common mathematical structures and data types, (structured) sets, functions, relations, orders, “et al” (see CFR1 and CFR2);
    • familiarity with the general ideas and tools of abstract algebra (see IEA);
    • familiarity with real numbers, and some of their metric, topological, and order-theoretic properties (see IDMb);
  • familiarity with at least one programming paradigm (if you have programmed a bit in your life, you should be OK);

Need to revise?

If you want to revise some material related to the prerequisites, specifically any of IRI, IDMb, CFR1, CFR2, IEA, do check the self-study pages I have prepared. Dive in! 🤿

(Obs. 1: learnpass.)

(Obs. 2: studyread.)

Tips

You might benefit by having a look at my tips for students.

Syllabus

The principal objective of this «topics» course is to introduce the student to programming language theory, specifically denotational semantics of programming languages. The objective of a denotational semantics is to assign formal mathematical objects as meanings of programs and programming language constructions in a useful way.

We shall use tools obtained in FMC1 & FMC2, but, most importantly, elaborate new, powerful tools (beyond the reach of FMC1–FMC2). that will permit defining (and proving) interesting concepts (and theorems) as applications.

We might also take detours in topology (pointful and pointless) and type theory; this will depend crucially on the interest and work of the students, and on the pace of the class.

Denotational semantics

Denotational semantics for imperative, functional, and logic programming languages. Typed and untyped λ-calculus. PCF. Domain-theoretic, game-theoretic, category-theoretic, and fixpoint semantics.

Possible detours

  • Topology. Topology (pointful and pointless). Synthetic topology and applications in computer science, programming languages, and logic.
  • Type theory. Constructive mathematics. Martin-Löf type theory. Programming with dependent types.
  • Linear logic. Proof-theoretic and game-theoretic semantics.

Bibliography

(Heard of libgen.rs?)

The following is subject to change during the semester.

  • Winskel (1993): The Formal Semantics of Programming Languages
  • Tennent (1991): Semantics of Programming Languages
  • Lloyd (1987): Foundations of Logic Programming, 2nd ed.

Auxiliar

  • Escardó (2004): Synthetic topology of data types and classical spaces
  • Streicher (2006): Domain-theoretic Foundations of Functional Programming
  • Harper (2016): Practical Foundations for Programming Languages, 2nd ed. [PFPL]
  • Laurent: notes on game semantics
  • Abramsky & Jung (1994): Domain theory
  • Davey & Priestley (2002): Introduction to Lattices and Order, 2nd ed. [DP]
  • Stoy (1977): Denotational Semantics
  • Apt (1990): Logic Programming
  • Miller & Nadathur (2012): Programming with Higher-Order Logic
  • Plotkin: Pisa notes
  • Wadler et al (2022): Programming Language Foundations in Agda
  • Pierce (1991): Basic Category Theory for Computer Scientists
  • Munkres (2000): Topology, 2nd ed.
  • Simmons (1963): Topology and Modern Analysis
  • Sutherland (2009): Introduction to Metric and Topological Spaces, 2nd ed.
  • Mendelson (1975): Introduction to Topology, 3rd ed.
  • Vickers (1989): Topology via Logic
  • Moschovakis (2005): Notes on set theory
  • Goldrei (1996): Classic Set Theory

Tecnologias e ferramentas

Obs.: As tecnologías/ferramentas seguintes podem mudar durante a disciplina—exceto a primeira.

  1. PAPEL (um caderno para dedicar à disciplina) e LAPIS/CANETA.
  2. Zulip (leia o FAQ).

Regras

  1. Nunca escreva algo que você mesmo não sabe explicar: (i) o que significa; (ii) seu papel na tua resolução. Por exemplo: um aluno escreveu a frase seguinte na sua demonstração: «Como f é cancelável pela esquerda temos que g=h». Ele deve saber o que significa ser cancelável pela esquerda e também explicar como isso foi usado e/ou o que isso tem a ver com essa parte da sua demonstração.
  2. Qualquer trabalho poderá ser questionado em forma de prova oral, em modo privado ou aberto. Se um aluno não consegue explicar o que ele mesmo escreveu numa resolução, será considerado plágio (veja abaixo).
  3. Participando, nunca dê uma resposta que tu não pensou sozinho, exceto dando os créditos correspodentes.
  4. Não tente “forçar a barra” perguntando ou respondendo coisas aleatórias com objetivo único de ganhar pontos. Os pontos de participação não correspondem em apenas perguntas ou dúvidas que mostram interesse. O interesse é implícito pelo fato que tu escolheu matricular nesta turma—não vale pontos.
  5. Não procurem informações ou resoluções em qualquer lugar fora dos indicados em cada homework. O único recurso aceitável para procurar ajuda é no nosso Zulip (especificamente seus canáis públicos—não DM) e a monitoria.

Uns deveres dos alunos

  1. Visitar o site e o Zulip da disciplina pelo menos uma vez por dia durante o semestre. (Qualquer coisa postada no site ou no Zulip da disciplina será considerada como conhecida por todos os alunos da turma.)
  2. Estudar o conteúdo lecionado e tentar resolver todos os trabalhos atribuidos.
  3. Participar no Zulip diariamente, compartilhando tuas resoluções para receber feedback, e checando as resoluções de outros colegas para dar feedback.
  4. Checar e atender seu email cadastrado no SIGAA pelo menos uma vez por dia durante o semestre.
  5. Participar nas aulas! Obs.: tendo uma dúvida durante a aula, levante a mão para solicitar “a fala” e assim que a receber, pergunte! Não espere o fim da aula para discutir tua dúvida em “modo particular”! A maioria das vezes eu vou negar isso e pedir ao aluno iniciar a discussão no Zulip ou na próxima aula.
  6. Participar nas aulas de exercícios de monitoria e utilizar seus horários de tirar dúvidas.
  7. Cada aluno será responsável para manter organizado e bem escrito o seu caderno com todos os teoremas e exercícios que estudou durante a disciplina.

(Veja também os FAQs relevantes.)

Sobre plágio

  1. Plágio detectado implica que o aluno será reprovado imediatamente por nota e por faltas.
  2. Entregar tuas resoluções para um aluno copiar é proibido do mesmo jeito, e também não ajuda mesmo ninguém.

Cadernos vs. celulares

Não faz sentido aparecer na aula sem caderno. E não faz sentido aparecer na aula com celular ligado; bote no modo avião antes de entrar na sala. As aulas são interativas e se não pretende participar e concentrar nesses 100 minutos, sugiro ficar fora e escolher uma outra maneira de passar teu tempo. Não é necessário (e obviamente nem suficiente) aparecer nas minhas aulas para passar.

Avaliação e faltas

Disclaimer. Eu suponho que os alunos desta turma escolheram se matricular por interesse em aprender seu conteúdo. O ideal seria ignorar assuntos irrelevantes de avaliação, presenças, carga horária, etc., e se jogar nos estudos.

Avaliação

A nota final de cada aluno vai ser principalmente baseada em um ou mais dos: (i) sua participação nas aulas; (ii) sua participação no Zulip; (iii) provas escritas; (iv) trabalhos atribuidos; (v) hw resolvidos (veja o FAQ relevante); (vi) caderno;

Cada aluno será responsável para manter organizado e bem escrito o seu caderno com todos os teoremas e exercícios que estudou durante a disciplina.

Presenças e faltas

A presença pela regulação da UFRN é obrigatória. Os alunos que não gostam/querem/podem aparecer nas minhas aulas ainda tem chances de ganhar até nota máxima e aprovar na disciplina. Ou seja: alunos que escolhem não participar ou aparecer nas aulas, e mesmo assim aparecem nas provas escritas e conseguem nota final de aprovação vão ter sua porcentagem de faltas ajustada para não reprovar por faltas. Esclarecimento: alunos que não conseguem nota final de aprovação não terão sua porcentagem de presença ajustada de jeito nenhum e por nenhum motivo.

Obviamente, alunos que não aparecem nas aula não terão como ganhar pontos de participação—duh!—nem acesso nos pontos de possíveis provas-surpresas.

As presenças/faltas serão cadastradas usando o sistema Plickers (veja o FAQ relevante).

Atrasados

Definição (atrasado). Seja $a$ aluno desta turma. Dizemos que $a$ é atrasado sse $a$ não está já sentado na sua mesa, com seu caderno já aberto, seu celular já desligado e na mochila, no momento que a aula começa.

Tentem estar presentes na sala da aula ANTES do horário do seu começo, e fiquem até o fim da aula.

Caso que alguém chega atrasado: não faz sentido bater na porta da sala de aula; não faz sentido cumprimentar nem o professor (não é mostra educação cumprimentar nesse caso—pelo contrário!) nem os amigos/colegas da aula. Entrando numa sala onde a aula já começou, tentem fazer sua entrada o menos possível notada por os participantes pois atrapalha a concentração de todos.

FAQs

Dynamic content

Scoreboard

Participation points will appear here. (None yet.)

Exams

Exams will be announced here. Do not expect a notice in advance; I might notify the class about an exam the previous day. Do treat each day as a possible exam day.

Prova

Homework

Read the FAQ about hw. Also note that:

  • Homeworks are also assigned during class and within Zulip

2023-08-27

  1. Keeping the same syntax for Nml, give a semantics so that it serves to name integers.
  2. Flip B and N on the definition of Nml, so that “bits are prepended” (instead of appended). Show how to define the semantic function to maintain the same meaning.
  3. Define a languge for “reduced” binary numerals (no leading zeros).

2023-08-28

  1. We left the job incomplete in class: define what needs to be defined to complete the definition of the semantics of Impinha that we were working on.

2023-08-30

  1. Prove that for all $C : \mathsf{cmd}$ of Impinzinha, $C \approx_{\mathrm{cmd}} \mathtt{skip}$.
  2. Guess a handy RHS and prove:
    1. if B then C else C ≈ ?
    2. if not B then C₁ else C₂ ≈ ?
    3. if B then (if B then C₁ else C₂) else C₃ ≈ ?
    4. if B then C₁ else (if B then C₂ else C₃) ≈ ?
    5. for (if B then N₁ else N₂) do C ≈ ?
  3. Prove or refute:
    1. for 0 do C ≈ skip;
    2. for succ 0 do C ≈ C;
    3. for succ N do C ≈ C ; for N do C;
    4. for succ N do C ≈ (for N do C) ; C;
    5. C₀ ; (if B then C₁ else C₂) ≈ if B then (C₀;C₁) else (C₀;C₂);
    6. if B then (for N do C₁) else (for N do C₂) ≈ for N do (if B then C₁ else C₂);
    7. for N + N do C ≈ for N do (C ; C).

2023-09-04: Metric spaces

  1. Prove or refute:
    1. (Ian-)Bounded ⇔ JP-Bounded
    2. A ⊆ B ⇒ diam(A) ≤ diam(B)
    3. an arbitrary union of bounded sets is bounded
    4. an arbitrary but nonvoid intersection of bounded sets is bounded
  2. Try to define the notion of:
    1. Closed set
    2. Boundary of a set bdry(A)
  3. Show an example where diam(A∪B) > diam(A) + diam(B) and find a suficient condition for diam(A∪B) ≤ diam(A) + diam(B)
  4. Prove the uniqueness of limits in metric spaces

2023-09-10: Metric spaces

  1. X and Ø are open sets
  2. (Open) balls are open sets
  3. Open(A)ff ⇔ f A is a union of open balls
  4. Any union of open sets is open
  5. Any finite intersection of open sets is open
  6. Define the interior of a set A, inter(A). It should satisfy:
    1. inter(A) is the best open subset of A (what does that mean?)
    2. A is open ⇔ A = inter(A)
    3. inter(A) is the union of all open subsets of A
  7. Investigate:
    1. inter(A) ∪ inter(B) ≟ inter(A∪B)
    2. inter(A) ∩ inter(B) ≟ inter(A∩B)

2023-09-12: Metric spaces

  1. fmcbook: Cap. 16, até §«Continuidade»

2023-10-08: Semantics and topological spaces

  1. Work on some topology!
    1. [sutherland]: Ch. 7 & Ch. 8
    2. [mendelson]: first section of Ch. 3
    3. [simmons]: first section of Ch. 3 (§16)
    4. [munkres]: first couple of sections of Ch. 2 (§§12-13)
  2. Semantics
    1. Guess and prove: ⟦x := 0; if iszero y then x := y else y := x⟧ = ⟦?⟧
    2. Extend Imp with a repeat C until B (like the do-while of C), and give its denotational semantics as the fixpoint of a certain functional F.
    3. Study [winskel] up to §5.3
    4. Study [tennent] up to Ch. 3

2023-10-15: Topological spaces

  1. Work (more) on some topology!
    1. [sutherland]: C9
    2. [mendelson]: C3: §2, §3, §4
    3. [simmons]: C3: §17, §18
    4. [munkres]: C2: §12, §13

2023-10-29: Topological spaces

  1. Work (more) on some topology!
    1. [sutherland]: C10.1 (subspaces); C11, C13
    2. [mendelson]: C3: §6; C5: §1, §2, §3
    3. [simmons]: C4: §21, §26
    4. [munkres]: C2: §16; C3: §26, §27

2023-11-10: Transfinite arithmetic

  1. [moschovakis]: Ch 5; Problems: x5.14, x5.15, x5.16, x5.17, x5.25,
  2. [goldrei]: Ch 8: §§8.1–4

2023-11-10: Posets and fixpoints

  1. [moschovakis]: Ch 6; Problems: x6.1–x6.21

2023-11-18: Posets and fixpoints

  1. [moschovakis]: Problems: x6.22–x6.29

2023-12-02: Logic programming

  1. [lloyd]: §2–§4

2023-12-14: Logic programming

  1. [lloyd]: §5
  2. [lloyd]: Ch1 probs: 12, 13
  3. [lloyd]: §6
  4. [lloyd]: Ch2 probs: 2, 3, 4, 5, 6, 7

Log

2023-08-16: Intro

  • Overview
  • Paradigms: declarative & imperative
  • Statics vs dynamics
  • Static types vs dynamic type”s”
  • Domains of meanings

2023-08-23: Numerals and numbers

  • BNF notation
  • nml: a language for binary numerals
  • how (not) to define a semantics for nml
  • Θ. correctness of (syntactic) successor

2023-08-28: Impinzinha (a toy imperative language)

  • Impinha: a simple imperative language
  • Syntax of Impinzinha
  • Syntactic sugar
  • Semantics for some of Impinzinha’s constructs

2023-08-30: Impinha (a toy imperative language)

  • Semantics for the rest of Impinzinha’s constructs
  • Equivalences between (fragments of) programs
  • Impinha: Impinzinha + Idenifiers (names) and assignments

2023-09-04: Metric spaces

  • From ℝ to metric spaces
  • Bounded, diameter, limit, open

2023-09-11: Metric spaces

2023-09-20: Operational semantics

  • Imp: introducing while
  • Small-step vs big-step
  • Evaluation strategies
  • Imposing a short-circuit

2023-09-27: Denotational semantics

  • while is difficult

2023-10-04: Denotational semantics; Topology

  • recap: semantics of Imp
  • some equivalences of programs of Imp
  • fixpoints for calculating and defining semantics
  • introduction to topology

2023-10-11: Topology

  • Metric spaces
  • Open, closed, interior, closure, boundary
  • temporal and informal nomenclature
  • Limit points

2023-10-18: Topology

  • Continuity

2023-10-25: Topology

  • Connectedness
  • Totally bounded
  • Complete
  • Completions of ℚ
  • Compactness in metric spaces
  • Compactness in topological spaces

2023-11-01: Order theory

  • Posets: discrete, flat, lub, glb
  • Cardinal and ordinal numbers
  • Transfinite induction & recursion

2023-11-08: Order theory

  • inductive (chain-complete) posets
  • continuous mappings
  • compact mappings

2023-11-08: Order theory

2023-11-13: Logic Programming

2023-11-29: Logic Programming

2023-12-06: Logic Programming

2023-12-13: Logic Programming

  • (α)-iterations of monotone endomaps of complete lattices
  • closure ordinal
  • $\mathrm{LHM}(P) = \mathrm{lfp}(T_P) = T_P \mathbin{\uparrow} \omega$

2023-12-20: Game semantics

2023-12-20: Exam

Future

No future. This semester has ended.

Last update: Sat Dec 23 01:44:03 -03 2023