{
  "metadata": {
    "title": "Study Card: Lambda Calculus Fundamentals",
    "topic": "Introduction to lambda calculus syntax and evaluation",
    "audience": "Computer science students studying functional programming",
    "learner_focus": "Understand lambda abstraction, application, and beta-reduction",
    "estimated_read_time_minutes": 12,
    "prerequisites": [
      "Basic understanding of functions",
      "Familiarity with mathematical notation"
    ],
    "learning_objectives": [
      "Define lambda abstraction and application",
      "Perform beta-reduction on simple expressions",
      "Identify bound and free variables"
    ],
    "sources": [
      {
        "title": "The Lambda Calculus: Its Syntax and Semantics",
        "author": "Henk Barendregt",
        "year": "1984",
        "citation": "Barendregt, H. (1984). The Lambda Calculus: Its Syntax and Semantics. North-Holland.",
        "link": "https://doi.org/10.1016/C2013-0-07856-2"
      },
      {
        "title": "An Introduction to Functional Programming Through Lambda Calculus",
        "author": "Greg Michaelson",
        "year": "2011",
        "citation": "Michaelson, G. (2011). An Introduction to Functional Programming Through Lambda Calculus. Dover Publications."
      }
    ],
    "provenance": {
      "model": "Claude 3.5 Sonnet",
      "date": "2025-11-09",
      "version": "1.0",
      "notes": "Example study card demonstrating tufte-press skill usage"
    }
  },
  "pages": [
    {
      "page_number": 1,
      "layout": "two-column",
      "main_flow": [
        {
          "type": "text",
          "content": "Lambda calculus is a formal mathematical system for expressing computation through function abstraction and application.",
          "attributes": {
            "emphasis": "newthought"
          }
        },
        {
          "type": "text",
          "content": "At its core, lambda calculus has three fundamental constructs: variables (x, y, z), abstractions (λx.M), and applications (M N). These simple building blocks are sufficient to express any computable function."
        },
        {
          "type": "callout",
          "content": "The λ symbol denotes function abstraction, creating an anonymous function that binds a variable within an expression.",
          "attributes": {
            "callout_title": "Lambda Abstraction"
          }
        },
        {
          "type": "list",
          "content": "Syntax components:\n• Variable: x (represents a value)\n• Abstraction: λx.M (function with parameter x and body M)\n• Application: M N (apply function M to argument N)",
          "attributes": {
            "list_style": "bullet"
          }
        }
      ],
      "margin_notes": [
        {
          "anchor": "λx.M",
          "content": "Read as 'lambda x dot M' where x is the parameter and M is the function body",
          "note_type": "definition"
        },
        {
          "anchor": "abstraction",
          "content": "Also called lambda terms or function definitions",
          "note_type": "definition"
        }
      ]
    },
    {
      "page_number": 2,
      "layout": "single-column",
      "main_flow": [
        {
          "type": "text",
          "content": "Beta-reduction is the fundamental computation step in lambda calculus, applying a function to an argument by substituting the argument for the bound variable.",
          "attributes": {
            "emphasis": "newthought"
          }
        },
        {
          "type": "equation",
          "content": "(λx.M) N → M[x := N]",
          "attributes": {
            "equation_latex": "(\\lambda x. M)\\,N \\to_\\beta M[x := N]"
          }
        },
        {
          "type": "text",
          "content": "For example, applying the identity function to the value 5:"
        },
        {
          "type": "equation",
          "content": "(λx.x) 5 → 5",
          "attributes": {
            "equation_latex": "(\\lambda x. x)\\,5 \\to_\\beta 5"
          }
        },
        {
          "type": "callout",
          "content": "Variable capture must be avoided during substitution by renaming bound variables when necessary (alpha-conversion).",
          "attributes": {
            "callout_title": "Important: Alpha-Conversion"
          }
        },
        {
          "type": "text",
          "content": "A variable is bound if it appears within the scope of a lambda abstraction that binds it; otherwise it is free. Free variables represent external values that must be supplied by the environment."
        }
      ],
      "margin_notes": [
        {
          "anchor": "beta-reduction",
          "content": "Also written as β-reduction; the primary reduction rule in lambda calculus",
          "note_type": "definition"
        },
        {
          "anchor": "M[x := N]",
          "content": "Substitution notation: replace all free occurrences of x in M with N",
          "note_type": "definition"
        },
        {
          "anchor": "alpha-conversion",
          "content": "Renaming bound variables to avoid capture: λx.λy.x ≡ λz.λy.z",
          "note_type": "example"
        }
      ]
    }
  ]
}
