Please enable JavaScript.

Coggle requires JavaScript to display documents.

Lambda calculus (Boolean (def cond = λ.e1.λ.e2.λ.c.((c e1) e2) Syntactic…

- - - - By convention we will always use a capture-avoiding substitution. Substitution will only proceed if the variable is not in the set of free variables (fv) of the expression, and if it does then a fresh variable will be created in its place
        (λx.e) a → [x/a]e, if x ∉ fv(e)
- - - - System with true and false as basic operations and and, or, not as basic operations.
        
        can prove
        
        theorem
        
        with axioms
        
        and apply rules of inference
      - Used in electronics where signals are represented as true or false
    - - This is through predicates to generalise logical expressions to describe properties of non logical values and functions to generalise operations of non-logical values.
        
        Also introduces universal and existencial quantifiers
      - Forms the basis of Prolog
    - - In 1936 three approaches to computability were proposed.
        Define a set of primitive operations and simple rules for structing operations. Each has a proof theory
        
        Turing's Turing Machines
        
        Concentrated on computation as mechanised symbol manipulation based on assignment and time ordered evaluation.
        
        Turing demonstrated that it is impossible to tell whether or not a Turing machine is going to halt.
        
        Kleene's recursive function theory (based on Hilbert's work)
        
        Church's λ calculus
        
        Emphasised computation as structured function application. With evaluation order independent. #both
        
        It is impossible to tell if a function call is going to terminate #both #similar
  - - - Culminates on LISP - simple language based on recursive functions manipulating lists of words and numbers. There is not distinction between programs and data. A LISP program is a list. It is not purely functional and contains imperative elements.
    - - Landin's approach was based on an operational description of λ calculus defined in terms of an abstract interpreter for it - the SECD machine.
        
        Used to construct an abstract interpreter for ALGOL 60 #Used to describe
        
        Culminates on VDL used to define IBM's PL/1.
      - Strachey' approach was to construct descriptions of imperative languages using notation based on λ calculus. So, every imperative construct has an equivalent function denotation. Functional languages are closely related to λ calculus based semantic languages.
- - - - Order of evaluation
        
        Applicative order, the parameter expression is evaluated before being passed to the formal parameter
        
        Normal order, the actual parameter expression is not evaluated before being passed to the formal parameter