Program = Proof (Mimram)

91 flashcards · Mathematics · by lakesare

1. Visually imagine type of comp function: as a usual type as a logical implication.

   as a usual type Meaning that for any types ’a, ’b and ’c, – if f is a function which takes a value of type ’a as argument and returns a value of type ’b, – if g is a function which takes a value of type ’b as argument and returns a value of type ’c, and – if x is a value of type ’a, then the result is of type ’c.as a logical implication Now, if we read -> as a logical implication ⇒, the type can be written this way, which is a valid formula. This is not by chance: in some sense, the program com…

2. Visually imagine how would we type euclidean division with propositional logic VS with dependent types. Of course, if we want to prove richer properties of programs (or use programs to prove more interesting formulas), we should use a logic which is more expressive than propositional logic.

   with propositional logic with dependent types Of course, if we want to prove richer properties of programs (or use programs to prove more interesting formulas), we should use a logic which is more expressive than propositional logic. In this course, we will present dependent types which achieve this, while keeping the proof-as-program correspondence.

3. What does HOTT stand for?

   HOmotopy Type Theory

4. Why did the Fields medalist Voevodsky propose HOTT? Vladimir Alexandrovich Voevodsky was a Russian-American mathematician. His work in developing a homotopy theory for algebraic varieties and formulating motivic cohomology led to the award of a Fields Medal in 2002.

   He couldn't find a mistake in his proof for more than 20 years.

5. What does (sic) mean in Latin?

   "Just as" In full: sic erat scriptum, "thus was it written". The Latin adverb sic inserted after a quoted word or passage indicates that the quoted matter has been transcribed or translated exactly as found in the source text, complete with any erroneous, archaic, or otherwise nonstandard spelling, punctuation, or grammar. It also applies to any surprising assertion, faulty reasoning, or other matter that might be interpreted as an error of transcription.

6. Name 2 formalisms that we can base all mathematics on.

   Set theory Type theory

7. [OCaml] Explain why map function has this type. For instance, suppose that we have a list l of integers, and we want to double all its elements. We can use the List.map function from the standard library.

   takes a function 'a -> 'b as an argument takes a' list as an argument returns b' list It takes as arguments a function f of type 'a -> 'b (here 'a and 'b are intended to mean “any type”), and a list whose elements are of type 'a, and returns the list whose elements are of type 'b, obtained by applying f to all the elements of the list.

8. [OCaml] How can we modify x?

   Use ref (references). Incrementing a counter 10 times. As in most programming languages, OCaml has support for values that we can modify, here called references: they can be thought of as memory cells, from which we can retrieve the value and also change it. We can create a reference r containing x with let r = ref x, then we can obtain its contents with !r and change it to y with r := y

9. [OCaml] What's the only value in the Unit type?

   ()

10. [OCaml] What's the type of this add function?

    Note that arrows are implicitly bracketed on the right: this type means int -> (int -> int)

11. [OCaml] What's the type of this add' function?

    The pair of x and y is noted x,y. For instance, we can consider the pair 3,"hello" which has the product type int * string (it is a pair consisting of an integer and a string)

12. [OCaml] Curious fact about recursive functions in OCaml?

    They have to be defined with rec keyword. The factorial function. Functions can be recursive, meaning that they can call themselves. In this case, the rec keyword has to be used.

13. [OCaml] What's meat by OCaml's "toplevel"?

    Just OCaml's REPL. Many OCaml guides and tutorials refer to the OCaml toplevel, but what exactly is this thing? In short, the toplevel is OCaml’s Read-Eval-Print-Loop (repl) allowing interative use of the OCaml system. You can consider the toplevel an alternative to compiling OCaml into an executable.

14. [OCaml] What should we use in OCaml instead of: == !=

    == - = != - <> In order to compare whether two values x and y are equal or different, one should use x = y and x <> y.Beware that the operators == and != also exist, but they compare values physically, i.e. check whether they have the same memory location, not if they have the same contents.

15. [OCaml] In Ocaml, what's the difference between a constructor and a function?

    constructor - doesn't reduce to anything function - reduces to 5 Constructors don't reduce to anything.

16. [OCaml] Visually imagine type tree: "Node" with 1 number, 2 children "Leaf" with 1 number A binary tree.

    A tree is recursively characterized as being Node applied to a triple consisting of an integer and two trees or Leaf applied to an integer.

17. [OCaml] Where is a pattern? A binary tree.

    Node (n, t1, t2) is called a pattern and n, t1 and t2 are variables which will be defined as the values corresponding to the tree we are currently matching with, and could be given any other name.

18. [Typing in functional languages] What's strongly typed language VS weakly typed language?

    Subjective, how strongly the language feels about typing.

19. [Typing in functional languages] Visually imagine why OCaml is statically typed.

    Moreover, typing is statically checked: when compiling a program, the compiler ensures that all the types match, and we use values of the expected type.

20. [Typing in functional languages] What's dynamically typed language VS statically typed language?

    dynamically typed - checked during execution statically typed language - checked during compilation

21. [Typing in functional languages] What's a principal type? A program can admit multiple types. For instance, the identity function admits all of these types.

    Type from which other types can be derived.

22. [OCaml] What type do Some and None constructors come from?

    a' option Same as a'? in some languages.

23. [A small language] What is prog option type? A small language. We first introduce a small programming language, which can be considered as a very restricted subset of OCaml, that we will implement in OCaml itself. In this language, the values we use are either integers or booleans.

    Either prog or None. Same as prog? in some languages.

24. [A small language: Reduction rules and Typing rules] How do we read p1 → p2? Reduction rules

    p1 reduces to p2.

25. [A small language: Reduction rules and Typing rules] How do we read ⊢ p: A? Typing rules

    Program p has the type A.

26. [A small language: Reduction rules and Typing rules] What do we call this?

    Reduction Rules p1 → p2Program p1 reduces to program p2.

27. [A small language: Reduction rules and Typing rules] What do we call this?

    Typing rules p : AProgram p has type A.

28. [OCaml] What is this a shortcut for?

    This shortcut was introduced because it is very common to directly match on the argument of a function.OCaml has syntactic sugar that allows you to do pattern matching directly in lambda expressions. This is never necessary, because you can always ignore it and use match directly, but it can lead to more concise code. You can do this with the function keyword; the syntax is: function pattern-matching and it's exactly equivalent to fun x -> match x with pattern-matching.

29. [Type theory: Type System properties] What is a Subject Reduction property of a type system? (Also known as subject evaluation, type preservation or simply preservation)

    p1 → p2 : A → : A Evaluation of an expression doesn't cause its type to change. Intuitively, this means one would not like to write a expression, in say Haskell, of type Int, and have it evaluate to a value v, only to find out that v is a string.

30. [Type theory: Type System properties] How are these connected: Reduction rules Typing rules? Reduction rules Typing rules

    [Subject Reduction property] Evaluation of an expression doesn't cause its type to change. By the subject reduction property.

31. [Type theory: Type System properties] What is a Progress property of a type system?

    Program is either: a value can be reduced

32. [Type theory: Type System properties] What is a Safety property of a type system?

    Program either: reduces to a value reduces infinitely The safety property finally states that typable programs never encounter errors, in the sense that their execution is never stuck: typically, we will never try to evaluate a program such as 3 + true during the reduction.

33. [Type theory: Type System properties] Name 3 properties a type system might have.

    Subject Reduction property p1 → p2: A → : AProgress property Program is either: a value; can be reduced.Safety property Program either: loops or reduces.

34. [Typing in functional languages] Why can't typing in OCaml prevent this error?

    Because typing in OCaml is not expressive enough, we can't do:

35. [Typing-logic correspondence] Logic: A ⇒ B Typing: ______________

    Logic: A ⇒ B Typing: A → B

36. [Typing-logic correspondence] Logic: A ∧ B Typing: ______________

    Logic: A ∧ B Typing: A * B (product/tuple type)

37. [Typing-logic correspondence] Logic: A ∨ B Typing: ______________

    Logic: A ∨ B Typing: (A, B) coprod (coproduct, either A or B)

38. [Typing-logic correspondence] Logic: T Typing: ______________

    Logic: T Typing: unit

39. [Typing-logic correspondence] Why can "True" be easily proved?

    Just return ().

40. [Typing-logic correspondence] Logic: ⊥ Typing: ______________

    Logic: ⊥ Typing: empty

41. [OCaml] In OCaml: fun keyword VS function keyword?

    fun keyword - anonymous function These are syntactically different but semantically equivalent.function keyword - shortcut for match OCaml has syntactic sugar that allows you to do pattern matching directly in lambda expressions. This is never necessary, because you can always ignore it and use match directly, but it can lead to more concise code. You can do this with the function keyword; the syntax is: function pattern-matching and it's exactly equivalent to fun x -> match x with pattern-matc…

42. [Typing-logic correspondence] How would you prove using typing?

    The formula (A ⇒ B) ⇒ (B ⇒ C) ⇒ (A ⇒ C) can be proved by the composition. Now, we can observe that there is a program of a given type (in a reasonable subset of OCaml, see below) precisely when the corresponding formula is true (for a reasonable notion of true formula).

43. [Typing-logic correspondence] Why is OCaml imperfect for types-logic correspondence?

    It's easy to prove anything if we use advanced features of the language, e.g. throw an exception. In next chapters, we will see that it is indeed possible to design languages in which a formula is provable precisely when there is a program of the corresponding type. Such languages do not have functions with “side-effects” (such as raising an exception) and enforce that all the programs are terminating.

44. Visually imagine functions: in extensional perspective VS in intensional perspective.

    in extensional perspective - inputs and outputs in intensional perspective - compare photos Where we care about the inner world of the function! In extensional perspective, two functions are equal when they have the same values on the same inputs. In an intentional perspective, the way the result is computed matters.

45. Visually imagine a disjoint union A ⊔ B.

    The disjoint union A ⊔ B of the sets A and B is the set formed from the elements of A and B labelled (indexed) with the name of the set from which they come. So, an element belonging to both A and B appears twice in the disjoint union, with two different labels.

46. Classic logic VS intuitionistic logic?

    classic logic Someone got 90% on the test. Okay!We're proving: There is a number such that...intuitionistic logic Someone got 90% on the test. Who???We're proving: There is a number such that...; WHICH NUMBER Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems of intuitionistic logic do not include the…

47. [Propositional logic] Name 3 alternative logical formalisms.

    natural deduction sequent calculus Hilbert calculus Hilbert put forth a most influential list of 23 unsolved problems at the International Congress of Mathematicians in Paris in 1900. This is generally reckoned as the most successful and deeply considered compilation of open problems ever to be produced by an individual mathematician.

48. [Propositional logic] Where do symbols ⊢ and ¬ originate from?

    From Frege's graphical notation for logic. Gottlob Frege (1848-1925), German philosopher, logician, and mathematician

49. [Propositional logic] Visually imagine: sequent VS inference rule.

    sequent Γ = A1, . . . , An called context.inference rule Consists of n sequents Γi ⊢ Ai, called the premises of the rule, and a sequent Γ ⊢ A, called the conclusion of the rule.

50. [Propositional logic] What's Г in a sequent?

    A context. A context (Г) is a list of propositions.

51. [Propositional logic] What's the name of this inference rule? Inference rules

    The principle of explosion Ex falso [sequitur] quodlibet, 'from falsehood, anything [follows]'. The principle of explosion states that once a contradiction has been asserted, any proposition (including their negations) can be inferred from it.

52. [Propositional logic] What's the problem with "All horses are the same color" paradox? P(1): set of 1 horses have the same color P(n) → P(n+1) 3. All sets of n >= 1 horses have the same color!

    There are no "middle horses" when we go from n=1 to 2! Note that the argument works if we assume P(2) is true. The argument above makes the implicit assumption that the set of n + 1 horses has the size at least 3, so that the two proper subsets of horses to which the induction assumption is applied would necessarily share a common element. This is not true at the first step of induction, i.e., when n + 1 = 2.

53. [Propositional logic] What is a fragment of a logic? Grammar rules Inference rules

    When we restrict 1. grammar rules 2. inference rules to certain connectives. E.g., only to implication ⇒.

54. [Propositional logic] When is the rule: admissible VS not admissible?

    admissible - premises are provable ⇒ conclusion is provable. not admissible - depends on the proof itself!

55. [Propositional logic] Why are these rules called structural rules?

    They concern the structure of logical proofs (and not particular connectives!).

56. [Propositional logic] Visually imagine the cut structural rule.

    A most important admissible rule is the cut rule, which states that if we can prove a formula B using a hypothesis A (thought of as a lemma used in the proof) and we can prove the hypothesis A, then we can directly prove the formula B. Its meaning is that, if a formula A appears as a conclusion in one proof and a hypothesis in another, then another proof in which the formula A does not appear can be deduced. In the particular case of the modus ponens, for example occurrences of man are eliminat…

57. [Propositional logic] Visually imagine a definable logical connective.

    - can be replaced by the definition- preserves provability

58. [Propositional logic] What does xch stand for? Structural rules.

    xch - exchange The rules of exchange, contraction, weakening and truth strengthening are often called structural rules.

59. [Propositional logic] What does contr stand for? Structural rules.

    contr - contraction The rules of exchange, contraction, weakening and truth strengthening are often called structural rules.

60. [Propositional logic] What does wk stand for? Structural rules.

    wk - weakening The rules of exchange, contraction, weakening and truth strengthening are often called structural rules.

61. [Propositional logic] What does tstr stand for? Structural rules.

    tstr - truth strengthening The rules of exchange, contraction, weakening and truth strengthening are often called structural rules.

62. [Propositional logic] Why can: a list of contexts be seen as a set? Structural rules.

    Because we have: exchange rule (== reordering is allowed) contraction rule (== { A, A } = {A})

63. [Notation] What is 𝒫(A) for set A?

    𝒫(A) = { all subsets of A } In mathematics, the power set (or powerset) of a set S is the set of all subsets of S, including the empty set and S itself.

64. [Notation] What is A* for set A?

    A* = { all sublists over A }

65. [Propositional logic] How does this substitution work?

    We detect all X substitute them with B.

66. [Propositional logic] What is a principal premise? ∨E inference rule Grammar rules Inference rules

67. [Cut elimination] Visually a cut formula VS a cut.

    cut formula - sandwiched between ~I and ~E cut - ~E rule Formally, a cut in a proof is an elimination rule whose principal premise is proved by an introduction rule of the same connective.The formula in the principal premise is called the cut formula.

68. [Cut elimination] Visually imagine a cut formula.

    Formally, a cut in a proof is an elimination rule whose principal premise is proved by an introduction rule of the same connective.The formula in the principal premise is called the cut formula.

69. [Cut elimination] Visually imagine a cut.

    Formally, a cut in a proof is an elimination rule whose principal premise is proved by an introduction rule of the same connective.The formula in the principal premise is called the cut formula.

70. [Cut elimination] Why is cut elimination is sometimes called a detour?

    Because we're always doing useless work! We will see that, however, we can always avoid using cuts in order to prove formulas.

71. [Notation] What does "admits" mean?

    "There exists".

72. [Cut elimination] How would we prove "6 admits a half": normally via cut elimination? There exists a number n such that n + n = 6.

    normally cut elimination

73. [Propositional logic] Name 3 equivalent statements: The logical system is consistent __________________________________ __________________________________

    The logical system is consistent Can't prove ⊥ Can't prove A and ¬A

74. [Propositional logic] Visually imagine a reversible rule. Reduction rules

    Proof of the reversed rule. In NJ, the reversible rules are (ax), (⇒I), (∧I), (⊤I) and (¬I).

75. [Classical Logic VS Intuitionistic Logic] Name the only difference between the deduction rules of: Intuitionistic Logic Classical Logic Reduction rules (Intuitionistic Logic)

    Intuitionistic Logic Classical Logic = Intuitionistic Logic + ¬A ∨ A is true Classical Logic = Intuitionistic Logic + excluded middle

76. [Classical Logic VS Intuitionistic Logic] Name the deduction rule that's ≡ excluded middle that can be added to the Intuitionistic Logic to make Classical Logic. Reduction rules (Intuitionistic Logic)

    ¬¬A ⇒ A

77. [Classical Logic VS Intuitionistic Logic] Name a super interesting proof that: works in Classical Logic, but fails in Intuitionistic Logic.

    irrationalirrational = rational (∃ a, b) (a, b are irrational ∧ ab is rational)

78. [Classical Logic VS Intuitionistic Logic] In what case can ¬A ∨ A be proven in Intuitionistic Logic?

    When we enter the details of A, e.g. A = T.

79. [Notation] How should you read this notation?

    Supposing all formulas in Γ, I can prove at least one formula in ∆.

80. [Boolean logic terminology] Visually imagine a product term in Boolean logic.

    In Boolean logic, a product term is a conjunction of literals, where each literal is either a variable or its negation.

81. [Boolean logic terminology] Name 2 examples of the canonical normal forms.

    Disjunctive Normal Form (DNF) (p ∧ q ∧ r) ∨ (p ∧ ¬q ∧ r ∧ s) ∨ (¬p ∧ ¬q)Aka minterm canonical form.Conjunctive Normal Form (CNF) (p ∨ q ∨ r) ∧ (p ∨ ¬q)Aka maxterm canonical form, or clausal form.Blake form Algebraic normal form In Boolean algebra, any Boolean function can be put into the canonical disjunctive normal form (CDNF) or minterm canonical form and its dual canonical conjunctive normal form (CCNF) or maxterm canonical form. Other canonical forms include the complete sum of prime implic…

82. [Notation] What's a lowercase and uppercase of lambda?

    uppercase Λ lowercase λ

83. [Notation] What are these letters: Δ Λ

    Δ - delta (δ) Delta (uppercase Δ, lowercase δ) is the fourth letter of the Greek alphabet.Λ - lambda (λ) Lambda (uppercase Λ, lowercase λ) is the eleventh letter of the Greek alphabet.

84. [Sequent Calculus] Name 2 notable features of Sequent Calculus? Sequent Calculus rules

    there are only I (Introduction) rules wffs look like Γ ⊢ ∆, where it's conjunction ⊢ disjunction Gentzen-style systems have significant practical and theoretical advantages compared to Hilbert-style systems. For example, both natural deduction and sequent calculus systems facilitate the elimination and introduction of universal and existential quantifiers so that unquantified logical expressions can be manipulated according to the much simpler rules of propositional calculus. In a typical argum…

85. [λ-calculus] How would you write this in λ-calculus? Anonymous function in OCaml

    λ

86. [λ-calculus] How would you write this in λ-calculus? Anonymous function in OCaml

    .

87. [λ-calculus] In your own words, what is: α-conversion VS β-reduction?

    α-conversion - rename bound variable β-reduction - apply the function to the argument The meaning of lambda expressions is defined by how expressions can be reduced.

88. [λ-calculus] Visually imagine 2 ways to β-reduce this expression.

    β-reduction to y: β-reduction to ...: This expression can reduce to y, which is a normal form, and is thus weakly normalizing. It can also reduce to itself and is thus not strongly normalizing.

89. [λ-calculus] Visually imagine when the expression is: weakly normalising VS strongly normalising VS NOT normalising.

    weakly normalising - exists a path to normal form strongly normalising - all paths lead to normal form not normalising - 0 paths lead to normal form Clearly, a strongly normalizing term is weakly normalizing, but the converse does not hold. For instance, the term (λx.y)((λx.xx)(λx.xx)) can reduce to y, which is a normal form, and is thus weakly normalizing. It can also reduce to itself and is thus not strongly normalizing.

90. [λ-calculus] Visually imagine confluence.

    No matter the path, final normal form is always the same.(Confluence only applies to normal forms!)

91. [λ-calculus] Visually imagine the definition of a normal form.

    In the context of normal form terms in lambda calculus, "characterized" and "defined" are used to describe the specific criteria that must be met for a term to be considered a normal form.