text: Maths - Types - Curry-Howard
  
  Curry-Howard Correspondence
  
  There is a relationship between computer programs and mathematical proofs, this is known as the Curry-Howard correspondence.
  
  A type in λ-calculus has the same mathematical structure as a proposition in intuitionistic logic.
  
  A constructor for that type corresponds to a proof of the proposition. The following table has some specific types with their corresponding propositions:
  
  Proposition Type
  true formula unit type
  false formula empty type
  implication function type
  conjunction product type
  disjunction sum type
  universal quantification generalised product type (Π type)
  existential quantification generalised sum type (Σ type)
  
  λ-calculus Structure
  
  There is more information about λ-calculus on page here but here we are interested in its basic type structure.
  
   We can start with some predefined type. T A function type goes from one type to another T->S We can have higher order function types which go from a function to another function. (T->S)->(P->Q) ... and so on.
  
  Intuitionistic Logic Structure
  
  There is more information about Intuitionistic Logic on page here but here we are interested in its basic structure.
  
   We can start with a simple proposition. A Predicate calculus allows us to have conditional predicates. if A then B Again we han have higher order versions of this to any level. if (if A then B) then (if C then D) ... and so on.
  
  Curry–Howard–Lambek Correspondence
  
  We can extend this correspondence to include cartesian closed categories (CCC) in category theory.
   Introduction to Higher Order Categorical Logic - Lambek & Scott - Relates lambda calculus to higher order logic and cartesian closed categories.
  
  Cartesian Closed Category λ-calculus intuitionistic logic
  objects
  
  types
  p:P
  
  proposition
  p = proposition
  P = proof of p
  Operator Types
  
  function type
  b(a):A->B
  
  implication
  A implies B
  product type
  <a,b>:A/\B
  conjunction
  if A is proof of 'a'
  and B is proof of 'b'
  then A/\B is proof of <a,b>
  sum type
  a+b:A\/B
  disjunction
  if A is proof of 'a'
  and B is proof of 'b'
  then A\/B is proof of a+b
  Dependant Types
  dependent product type
  The type of the result B(a) depends on the value a .
  universal quantification
  (a:A).B(a)
  
  dependent sum type
  a of type A meets the specification B(a) as proved by b:B(a)
  Can be used to represent abstract data types.
  
  existential quantification
  (a:A).B(a)
  
  unit type true formula
  T
  bottom type false formula
  _|_
  Inductive Types
  recursive function inductive proof
  
  morphisms terms proof
  variable axiom
  constructor introduction rule
  destructor elimination rule
  normal form normal deduction
  weak normalisation normalisation of deductions
  type inhabitation problem provability
  inhabited type intuitionistic tautology
  function application
  substitution
  
  See Wiki
  
  Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.
  
   Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.
explanation: The document provides an overview of the Curry-Howard correspondence, which establishes a relationship between computer programs (specifically in λ-calculus) and mathematical proofs (in intuitionistic logic). It also touches on the extension of this correspondence to include cartesian closed categories in category theory. The text includes a detailed table that maps specific types in λ-calculus to corresponding propositions in intuitionistic logic and objects in cartesian closed categories. Additionally, it discusses the structure of λ-calculus and intuitionistic logic, and provides references for further reading.
distilabel_metadata.content: Evaluate the user given text extract and determine if it contains a math question and optionally and answer to this question.
  
  Output rules:
  
  1. Briefly describe the document and mention if it contains a question or a question and answer.
  2. Finalize the output with: Label: no-question,question,question-and-answer,multiple-question,multiple-question-and-answer
distilabel_metadata.role: system
distilabel_metadata.content: Maths - Types - Curry-Howard
  
  Curry-Howard Correspondence
  
  There is a relationship between computer programs and mathematical proofs, this is known as the Curry-Howard correspondence.
  
  A type in λ-calculus has the same mathematical structure as a proposition in intuitionistic logic.
  
  A constructor for that type corresponds to a proof of the proposition. The following table has some specific types with their corresponding propositions:
  
  Proposition Type
  true formula unit type
  false formula empty type
  implication function type
  conjunction product type
  disjunction sum type
  universal quantification generalised product type (Π type)
  existential quantification generalised sum type (Σ type)
  
  λ-calculus Structure
  
  There is more information about λ-calculus on page here but here we are interested in its basic type structure.
  
   We can start with some predefined type. T A function type goes from one type to another T->S We can have higher order function types which go from a function to another function. (T->S)->(P->Q) ... and so on.
  
  Intuitionistic Logic Structure
  
  There is more information about Intuitionistic Logic on page here but here we are interested in its basic structure.
  
   We can start with a simple proposition. A Predicate calculus allows us to have conditional predicates. if A then B Again we han have higher order versions of this to any level. if (if A then B) then (if C then D) ... and so on.
  
  Curry–Howard–Lambek Correspondence
  
  We can extend this correspondence to include cartesian closed categories (CCC) in category theory.
   Introduction to Higher Order Categorical Logic - Lambek & Scott - Relates lambda calculus to higher order logic and cartesian closed categories.
  
  Cartesian Closed Category λ-calculus intuitionistic logic
  objects
  
  types
  p:P
  
  proposition
  p = proposition
  P = proof of p
  Operator Types
  
  function type
  b(a):A->B
  
  implication
  A implies B
  product type
  <a,b>:A/\B
  conjunction
  if A is proof of 'a'
  and B is proof of 'b'
  then A/\B is proof of <a,b>
  sum type
  a+b:A\/B
  disjunction
  if A is proof of 'a'
  and B is proof of 'b'
  then A\/B is proof of a+b
  Dependant Types
  dependent product type
  The type of the result B(a) depends on the value a .
  universal quantification
  (a:A).B(a)
  
  dependent sum type
  a of type A meets the specification B(a) as proved by b:B(a)
  Can be used to represent abstract data types.
  
  existential quantification
  (a:A).B(a)
  
  unit type true formula
  T
  bottom type false formula
  _|_
  Inductive Types
  recursive function inductive proof
  
  morphisms terms proof
  variable axiom
  constructor introduction rule
  destructor elimination rule
  normal form normal deduction
  weak normalisation normalisation of deductions
  type inhabitation problem provability
  inhabited type intuitionistic tautology
  function application
  substitution
  
  See Wiki
  
  Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.
  
   Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.
distilabel_metadata.role: user
distilabel_metadata.raw_output_q_a_detector_0: The document provides an overview of the Curry-Howard correspondence, which establishes a relationship between computer programs (specifically in λ-calculus) and mathematical proofs (in intuitionistic logic). It also touches on the extension of this correspondence to include cartesian closed categories in category theory. The text includes a detailed table that maps specific types in λ-calculus to corresponding propositions in intuitionistic logic and objects in cartesian closed categories. Additionally, it discusses the structure of λ-calculus and intuitionistic logic, and provides references for further reading.
  
  Label: no-question