Concepts
Key terms and definitions from programming language theory.
A38
Abstract binding graphAn extension of Abstract binding tree ABT/plt/concepts/abstract-binding-tree-abts to a Directed acyclic graph DAG/plt/concepts/directed-acyclic-graph-dag structure while preserving the binding discipline.Abstract binding tree (ABT)An enriched Abstract syntax tree AST/plt/concepts/abstract-syntax-tree-ast with bindings and scopes. According to Practical foundations for programming languages , each node in an ABT is either a Variable or an Operator whose arguments are ${fref"programming-language-theory/concepts/abstractor.td"}s.Abstract binding tree abt valence abstractorAn enriched Abstract syntax tree AST/plt/concepts/abstract-syntax-tree-ast with bindings and scopes. According to Practical foundations for programming languages , each node in an ABT is either a Variable or an Operator whose arguments are Abstractors.Abstract data typeA type defined by its operations and their specifications rather than its implementation, providing encapsulation by hiding internal representation while exposing a public interface.Abstract machineA formal model of computation defined by a set of states, an initial state, final states, and a ${fref"programming-language-theory/concepts/transition-function.td"} specifying how states evolve step-by-step until halting.Abstract syntax tree (AST)Syntax & Grammar According to Practical foundations for programming languages , a tree representation of a term's essential structure not necessarily a program, omitting superficial syntactic details like parentheses, delimiters, and keywords. Can be of some specified Sorts.Abstract syntax tree ast labeled treeSyntax & Grammar According to Practical foundations for programming languages , a tree representation of a term's essential structure not necessarily a program, omitting superficial syntactic details like parentheses, delimiters, and keywords. Can be of some specified Sorts.AbstractorPractical foundations for programming languages 's notationActual parameter/argumentSyntax & Grammar According to Practical foundations for programming languages , the child of an Operator in an Abstract syntax tree AST/plt/concepts/abstract-syntax-tree-ast.AdmissibilityNo description yetAdmissibility judgmentNo description yetAdmissibleNo description yetAlgebraic data typeA composite type formed by combining ${fref"programming-language-theory/concepts/sum-type.td"}s variants/tagged unions and product types tuples/records, enabling precise modeling of data structures like Option, Result, or tree nodes. Synonymous with Sum of products SoP/plt/concepts/sum-of-products-sop.AliasingA semantic phenomenon where multiple identifiers, references, or paths denote the same memory location, causing mutations through one to be observable through the others - complicating reasoning, optimization, and safety guarantees.Alpha conversion/renamingExample:Alpha conversion renaming variable capture capture avoidingExample:Alpha-equivalenceThen, $=_\\alpha$ is the strongest Congruence on $\\mathcal{A}$that contains the followings:Alpha-variantIf two terms are related by the ${fref"programming-language-theory/concepts/alpha-equivalence.td"} relation, they are alpha-variants.AntecedentThe part above the line in a typing rule - the ${fref"programming-language-theory/concepts/premise.td"}s that must hold before the ${fref"programming-language-theory/concepts/conclusion.td"} can be drawn \"if\" part.AntisymmetricA property of a ${fref"programming-language-theory/concepts/binary-relation.td"} $R$ such that if $t\ R\ s$ and $s\ R\ t$ then $s = t$, for every $t$, $s$ $\in T$.AntisymmetryNo description yetAPI boundaryNo description yetApplication/Function callThe fundamental operation of applying a function to an argument.Architecture invariantNo description yetAritySyntax & Grammar According to Practical foundations for programming languages , a syntactic type signature of an ${fref"programming-language-theory/concepts/operator.td"}, determining the ${fref"programming-language-theory/concepts/sort.td"} of an operator and the number and the sorts of the arguments expected by the operator.Arrow typeThis generalization unifies simple function types, universal types $\\forall\\alpha.T$, and dependent function types under a single constructor.AssertionSynonymous with ${fref"programming-language-theory/concepts/judgment.td"}.AssociativityA parsing rule that determines grouping when the same operator repeats left: a - b - c = a - b - c; right: a :: b :: c = a :: b :: c.Assume-guarantee reasoningA pattern where interacting components have mutual obligations - one component assumes what another guarantees, and vice versa e.g., lambda assumes parameter has type $T$, application guarantees it;AST rewritingA program transformation technique that modifies the ${fref"programming-language-theory/concepts/abstract-syntax-tree-ast.td"} to implement features like ${fref"programming-language-theory/concepts/macro.td"}s, optimizations, or language extensions before code generation.AutoboxingExample:Automated theorem proverA tool that attempts to prove theorems automatically without human guidance, using techniques like resolution, rewriting, or SAT/SMT solving contrast with interactive provers like ${fref"programming-language-theory/concepts/coq.td"} that require uAutomated theorem prover sat solver smt solverA tool that attempts to prove theorems automatically without human guidance, using techniques like resolution, rewriting, or SAT/SMT solving contrast with interactive provers like ${fref"programming-language-theory/concepts/coq.td"} that require uAutomatic memory managementA language or runtime mechanism that handles allocation and deallocation of memory without explicit programmer intervention - encompassing techniques like ${fref"programming-language-theory/concepts/garbage-collection.td"}, reference counting, and ownership systems.AxiomA ${fref"programming-language-theory/concepts/rule.td"} with no ${fref"programming-language-theory/concepts/premise.td"}.Axiom inference ruleAn ${fref"programming-language-theory/concepts/axiom.td"} is an ${fref"programming-language-theory/concepts/inference-rule.td"} with no premise.Axiom rule proper ruleAn ${fref"programming-language-theory/concepts/axiom.td"} is an ${fref"programming-language-theory/concepts/inference-rule.td"} with no premise.Axiomatic semanticsA style of semantics that defines a language based on its proof rules/laws, rather than how it runs or what mathematical objects it denotes.B25
Backward chainingA proof technique for ${fref"programming-language-theory/concepts/judgment.td"}s that starts from the desired judgement and works backwards towards the ${fref"programming-language-theory/concepts/axiom.td"}s.Backward chaining searchA search strategy for a ${fref"programming-language-theory/concepts/derivation.td"} of some ${fref"programming-language-theory/concepts/judgment.td"} that starts from the desired Judgment as the initial goal, picks a rule at each step with the conclusion as the current goal, adds its premises as subgoals into a queue & continues until all subgoals are ${fref"programming-language-theory/concepts/axiom.td"}s.Backward chaining search backward chainingA search strategy for a ${fref"programming-language-theory/concepts/derivation.td"} of some ${fref"programming-language-theory/concepts/judgment.td"} that starts from the desired Judgment as the initial goal, picks a rule at each step with the conclusion as the current goal, adds its premises as subgoals into a queue & continues until all subgoals are ${fref"programming-language-theory/concepts/axiom.td"}s.Backward chaining search goal directedA search strategy for a ${fref"programming-language-theory/concepts/derivation.td"} of some ${fref"programming-language-theory/concepts/judgment.td"} that starts from the desired Judgment as the initial goal, picks a rule at each step with the conclusion as the current goal, adds its premises as subgoals into a queue & continues until all subgoals are ${fref"programming-language-theory/concepts/axiom.td"}s.Basic judgmentNo description yetBehavioral/Observational/Contextual equivalenceExample: $\lambda x.\ x \simeq \lambda x.\ (\lambda y.\ y)\ x$Beta-equivalenceA ${fref"programming-language-theory/concepts/binary-relation.td"} that relates terms connected by ${fref"programming-language-theory/concepts/beta-reduction.td"} - $(\lambda x.\ t)\ s =_\beta [x\to s]t$ - capturing the fundamental computation rule of function application.Beta-redex/Reducible expressionA term of the form: $t_1\ t_2$, in which $t_1$ is a ${fref"programming-language-theory/concepts/lambda-abstraction.td"} and $t_2$ is any term.Beta-reductionThe act of reducing a ${fref"programming-language-theory/concepts/beta-redex-reducible-expression.td"} by substituting the redex's argument into its function body.Beta reduction beta redex reducible expressionThe act of reducing a ${fref"programming-language-theory/concepts/beta-redex-reducible-expression.td"} by substituting the redex's argument into its function body.Big-step/Natural operational semanticsA style of semantic which defines evaluation via ${fref"programming-language-theory/concepts/evaluation-statement-judgement.td"} of the form $t \\Downarrow v$, relating a term directly to its final value in a single derivation rather than through intBig step natural operational semantics small stepA style of semantic which defines evaluation via ${fref"programming-language-theory/concepts/evaluation-statement-judgement.td"} of the form $t \\Downarrow v$, relating a term directly to its final value in a single derivation rather than through intBinary relationAn ${fref"programming-language-theory/concepts/n-place-relation.td"} where $n = 2$.BinderA syntactic construct that introduces a variable and defines its scope. In ${fref"programming-language-theory/concepts/lambda-calculus.td"}, it's the variable directly following $\lambda$.BindingAn association between a name and an entity value, location, type, function, etc. within a given scope.Binding structure of syntaxA generalization of Abstract binding tree ABT/plt/concepts/abstract-binding-tree-abt.Blame trackingA mechanism that identifies which party module, component, contract boundary is responsible when a ${fref"programming-language-theory/concepts/contract.td"} violation occurs.BlockA syntactic construct that groups statements and typically introduces a new scope for local bindings - delimited by braces { }, keywords begin/end, or indentation depending on the language.BNFA ${fref"programming-language-theory/concepts/metalanguage.td"} notation for specifying ${fref"programming-language-theory/concepts/context-free.td"} grammars, using production rules of the form $\text{<nonterminal>} ::= \text{expression}$ to define the syntax of formal languages.Boolean blindness-> The boolean discards it; you must later \"remember\" what it meant.Borrow checkerNo description yetBottom-up constructionSynonymous with ${fref"programming-language-theory/concepts/forward-chaining.td"}.Bound variableA variable bound by an enclosing $\lambda$.Branch coverageA testing metric requiring that every branch true/false of each conditional is executed at least once - difficult to achieve in testing but automatic in type checking since type checkers traverse boBrouwer-Heyting-Kolmogorov (BHK) interpretationMotivation. Classical logic tells you that something exists, not how to find it. BHK says to prove something exists, you must exhibit a ${fref"programming-language-theory/concepts/witness.td"}.C64
Calculus of inductive constructionTools: Rocq formerly CoqCall by nameLambda calculus, Semantics An evaluation strategy that is ${fref"programming-language-theory/concepts/normal-order.td"} but ${fref"programming-language-theory/concepts/beta-reduction.td"} inside ${fref"programming-language-theory/concepts/lambda-abstraction.td"} is not allowed.Call by needLambda calculus, Semantics, Pure lambda calculus An evaluation strategy similar to ${fref"programming-language-theory/concepts/call-by-name.td"}, but terms' values are cached to avoid re-evaluation.Call by need call by name call by value normal order fullLambda calculus, Semantics, Pure lambda calculus An evaluation strategy similar to ${fref"programming-language-theory/concepts/call-by-name.td"}, but terms' values are cached to avoid re-evaluation.Call by valueLambda calculus, Semantics A ${fref"programming-language-theory/concepts/strict-eager-evaluation-strategy.td"} in which ${fref"programming-language-theory/concepts/beta-redex-reducible-expression.td"}s inside lambda abstractions must not be reduced.Capture-avoiding substitutionRules in ${fref"programming-language-theory/concepts/pure-untyped-lambda-calculus.td"}:Capture avoiding substitution variable captureRules in ${fref"programming-language-theory/concepts/pure-untyped-lambda-calculus.td"}:Cascading/Sequential letNo description yetChomsky hierarchyA classification of formal grammars by expressiveness - from simplest to most powerful: regular, ${fref"programming-language-theory/concepts/context-free.td"} parsers, ${fref"programming-language-theory/concepts/context-sensitive.td"} type systems, recursively enumerable; explains why parsingChurch booleanEncoding:Church numeralTools: Rocq formerly CoqChurch numeral (rocq)Church's encoding of numbers used in ${fref"programming-language-theory/concepts/pure-untyped-lambda-calculus.td"}.Circular dependencyNo description yetClassA blueprint or template that defines the structure fields and behavior methods for creating objects, serving as a factory for instantiating objects with shared characteristics.Class extensionJava The { ... } part in class Sub extends Sup { ... }, can be conceptually viewed as a ${fref"programming-language-theory/concepts/mixin.td"} specifically applied to Sup.Class patternThis pattern has many variants:Closed recursionWhen utilizing the ${fref"programming-language-theory/concepts/class.td"} pattern to define classes with method calls referencing other methods, a recursion pattern that causes method reference to be resolved immediately right at class definition.Closed termA ${fref"programming-language-theory/concepts/lambda-term.td"} with no ${fref"programming-language-theory/concepts/free-variable.td"}.Closed (under)No description yetClosureLanguage feature/design, Semantics A function value that remembers its surrounding ${fref"programming-language-theory/concepts/environment.td"}.Code semantic modelNo description yetCodomainA property of a function specifying the set of values it produces as outputs.CombinatorA ${fref"programming-language-theory/concepts/lambda-term.td"} that contains no ${fref"programming-language-theory/concepts/free-variable.td"}, or in other words, a ${fref"programming-language-theory/concepts/closed-term.td"}.CommandRocq A top-level directive in Rocq that controls the environment like `Definition`, `Theorem`, `Print`, `Check` rather than operating within a proof.Command patternNo description yetCompilation unitNo description yetCompilerMathematically, denote $\\mathcal{P}_S$ as the set of programs in the source language and $\\mathcal{P}_T$ as the set of programs in the target language. Then, a compiler is a function $C: \\mathcal{P}_S \\to \\mathcal{P}_T$Compiler interpreterNo description yetCompleteThe adjective form of ${fref"programming-language-theory/concepts/completeness.td"}.CompletenessNo description yetComputabilityThe property of a mathematical problem that can be solved by a program.Computation ruleA rule performing an actual reduction step e.g., ${fref"programming-language-theory/concepts/beta-reduction.td"}, as opposed to ${fref"programming-language-theory/concepts/congruence-rule.td"} which merely propagate evaluation into subterms.Computation rule congruence ruleA rule performing an actual reduction step e.g., ${fref"programming-language-theory/concepts/beta-reduction.td"}, as opposed to ${fref"programming-language-theory/concepts/congruence-rule.td"} which merely propagate evaluation into subterms.Computation theoryThe branch of theoretical computer science studying what can be computed and with what resources - includes models of computation Turing machines, ${fref"programming-language-theory/concepts/lambda-calculus.td"}, ${fref"programming-language-theory/concepts/decidability.td"} halting problem, RicConclusionThe consequent ${fref"programming-language-theory/concepts/judgment.td"} of an ${fref"programming-language-theory/concepts/inference-rule.td"} that is derived when all its ${fref"programming-language-theory/concepts/premise.td"}s are satisfied.Concolic testingA testing technique combining concrete execution with symbolic reasoning - runs program with real values while simultaneously tracking symbolic constraints, then solves constraints to generate inputsConcrete generator styleA style of formal definition that defines a set as a union of a sequence $S_0 \\subseteq S_1 \\subseteq \\dots$ where each $S_{i+1}$ is built from $S_i$ using rules - e.g., for naturals: $S_0 = \\emptyset$Concrete ruleA specific instance of a ${fref"programming-language-theory/concepts/rule-schema.td"} where all ${fref"programming-language-theory/concepts/metavariable.td"}s are replaced with actual terms - the schema is the general pattern, the concrete rule is a particular instantiation.Concrete/Surface syntaxThe textual representation programmers actually write, including parentheses, keywords, and punctuation - as opposed to ${fref"programming-language-theory/concepts/structural-abstract-syntax.td"} which captures only the essential structure.Concurrent programmingA programming paradigm where multiple computations execute in overlapping time periods, managing shared resources and coordination through synchronization primitives.Conditional expressionAn expression that selects between alternatives based on a boolean or ${fref"programming-language-theory/concepts/pattern-matching.td"} like if b then x else y or ternary b ? x : y.CongruenceAn ${fref"programming-language-theory/concepts/equivalence.td"} relation that is preserved under a specific operation. That is, assume a congruence $\mathcal{C}$ and an operation $p$, we have $a\ \mathcal{C}\ b \iff p(a)\ \mathcal{C}\ p(b)$.Congruence ruleA rule specifying how evaluation propagates into subterms, allowing reduction within a syntactic context while preserving the outer structure.ConsequentThe part below the line in a typing rule - the ${fref"programming-language-theory/concepts/conclusion.td"} that follows when all ${fref"programming-language-theory/concepts/antecedent.td"}s are satisfied \"then\" part.ConservativeA type checker that considers all possible executions rather than just actual ones - may reject programs that would run safely false positives because it can't know which branch will execute at runtConstantThe token itself is the value-the parser can extract it directly without consulting any environment or performing computationConstruct/Special formA built-in language primitive with special evaluation rules that cannot be implemented as a regular function e.g., `if`, `lambda`, `define` in Lisp. In other words, special forms are necessary for cases where ${fref"programming-language-theory/concepts/derived-form.td"}s do not suffice.ConstructorProgramming paradigm, Language feature/design In languages with closure/programming-language-theory/concepts/closures or prototypes, a function that returns objects of similar shapes.Constructor expressionRocq An expression that applies a constructor/programming-language-theory/concepts/constructor to arguments to build a value of an inductive type/programming-language-theory/concepts/inductive-type like `S (S O)` for 2, or `Some 42` for an optional integer.Constructor expression constructorRocq An expression that applies a constructor/programming-language-theory/concepts/constructor to arguments to build a value of an inductive type/programming-language-theory/concepts/inductive-type like `S (S O)` for 2, or `Some 42` for an optional integer.Constructor tagA runtime marker that distinguishes which variant of a ${fref"programming-language-theory/concepts/sum-type.td"} a value belongs to, enabling ${fref"programming-language-theory/concepts/pattern-matching.td"} to dispatch on the correct case. Not to be confused with ${fref"programming-language-theory/concepts/type-variant.td"}s, which are static properties.ContextNo description yetContext-freeA grammar where production rules depend only on a single non-terminal, not its surroundings - parsers handle this level; e.g., balanced parentheses, syntax structure.Context-sensitiveA grammar where production rules can depend on surrounding symbols context - type systems handle this level; e.g., \"variable must be declared before use\" requires checking context of the usage site.ContractProblem: When typed code is called from untyped code, the type checker can't guarantee arguments will have correct types - untyped code has no static checking.CoqTools: Rocq formerly CoqCore calculus/languageA minimal formal language capturing the essential features of a paradigm or language, used to study semantics and prove properties without the complexity of full-scale syntax.Countable setA set that is either finite, or is infinite and there exists a bijection from itself into $\mathbb{N}$.Curry-Howard correspondenceRemark. Brouwer-Heyting-Kolmogorov BHK interpretation/programming-language-theory/concepts/brouwer-heyting-kolmogorov-bhk-interpretation makes this correspondence explicit:Curry/Y-CombinatorDetailsCurry y combinator z combinatorDetailsCurryingThe act of turning a multi-parameter function into a ${fref"programming-language-theory/concepts/higher-order-function.td"} that accepts one argument and returns a partially-applied version of the original function.Currying rocqNo description yetCursorNo description yetD38
DecidabilityA property of a problem or language where an algorithm exists that can always determine the correct yes/no answer in finite time for any input.Decidable propositionA proposition $P$ for which an algorithm exists that, in finite time, either produces a proof of $P$ or a proof of $\neg P$ - i.e., you can compute which side of $P \vee \neg P$ holds.Decision procedureAn algorithm that always terminates and correctly answers yes/no for any instance of a given problem class like propositional satisfiability or type equivalence.Decreasing analysisRocq A termination check in Rocq that verifies recursive functions always call themselves on structurally smaller arguments, ensuring all computations terminate required for logical consistency.Denotational semanticsA style of semantics that gives meanings to terms compositionally by mapping them to mathematical objects that possess interesting behaviors.Dependent typeConsider the $\\text{head}$ function which returns the first item of a list.DerivabilityNo description yetDerivability judgmentNo description yetDerivableA property of an ${fref"programming-language-theory/concepts/evaluation-statement-judgement.td"} that it can be derived using the evaluation rules in the calculus.Derivable evaluation statement judgementAn ${fref"programming-language-theory/concepts/evaluation-statement-judgement.td"} is derivable if there is a ${fref"programming-language-theory/concepts/derivation-tree.td"} conforming to the evaluation relation whose root is that evaluation statement.DerivationA finite composition of rules, starting with ${fref"programming-language-theory/concepts/axiom.td"}s and ending with a desired ${fref"programming-language-theory/concepts/judgment.td"}.Derivation derivation treeA specific visualization of a specific proof that $t \to t'$.Derivation forward chaining backward chaining bottom upNo description yetDerivation treeA specific visualization of a specific proof that $t \to t'$.Derived formA construct that adds no expressive power but can be translated into more primitive forms, e.g., $\text{let}\ x = s\ \text{in}\ t$ desugars to $(\lambda x.\ t)\ s$.Derived queryNo description yetDesired property determinacy of one step evaluationA desirable property of a ${fref"programming-language-theory/concepts/lambda-calculus.td"} where each term always evaluates to the same term in a single step.Desired property: determinacy of one-step evaluation relationA desirable property of a ${fref"programming-language-theory/concepts/lambda-calculus.td"} where each term always evaluates to the same term in a single step.Desired property: normal form implies valuesA desirable property of a ${fref"programming-language-theory/concepts/lambda-calculus.td"} where there's no ${fref"programming-language-theory/concepts/stuck-term.td"}. This property may not hold in most systems.Desired property: termination of evaluationA desirable property of a ${fref"programming-language-theory/concepts/lambda-calculus.td"} where every term all evaluates to a ${fref"programming-language-theory/concepts/normal-form.td"}, whether they become ${fref"programming-language-theory/concepts/stuck-term.td"} or Value. This property may not hold in most systems.Desired property termination of evaluation desired propertyA desirable property of a ${fref"programming-language-theory/concepts/lambda-calculus.td"} where every term all evaluates to a ${fref"programming-language-theory/concepts/normal-form.td"}, whether they become ${fref"programming-language-theory/concepts/stuck-term.td"} or Value. This property may not hold in most systems.Desired property: uniqueness of normal formsA desirable property of a ${fref"programming-language-theory/concepts/lambda-calculus.td"} where every term always evaluates to the same ${fref"programming-language-theory/concepts/normal-form.td"}. This property should hold in all deterministic systems.Desired property: value is in normal formA desirable property of a ${fref"programming-language-theory/concepts/lambda-calculus.td"} where every value is in ${fref"programming-language-theory/concepts/normal-form.td"}. This property must hold in all system.DesugarThe process of transforming ${fref"programming-language-theory/concepts/syntactic-sugar.td"} or high-level constructs into more primitive forms in the ${fref"programming-language-theory/concepts/core-calculus-language.td"}, simplifying the interpreter or compiler implementation.DesugarerA ${fref"programming-language-theory/concepts/compiler.td"} phase or program that transforms ${fref"programming-language-theory/concepts/syntactic-sugar.td"} into core language constructs, typically running before interpretation or further compilation stages.Dimensional analysisA static verification technique that encodes domain-specific properties e.g., physical units, array bounds, indices into types, ensuring operations respect these invariants by detecting mismatches at compile time rather than runtime.Directed acyclic graph (DAG)Edges have a direction from one node to another.Divergent/Big omega combinatorFormula: $\Omega = (\lambda x.\ x\ x)\ (\lambda x.\ x\ x)$Divergent big omega combinator curry y combinatorFormula: $\Omega = (\lambda x.\ x\ x)\ (\lambda x.\ x\ x)$Divergent termA term that does not evaluate to a ${fref"programming-language-theory/concepts/normal-form.td"}.DomainSet theory & Relation, Order & Lattice theory A mathematical structure typically a complete Partial order with a bottom element used in ${fref"programming-language-theory/concepts/denotational-semantics.td"} to model computation - enables reasoning about recursion, non-termination, and fixed points; values form a lattice where $\bot$ represents divergence/undefined.Domain theoryA branch of mathematics studying structured sets domains with partial orders and continuity, providing foundations for ${fref"programming-language-theory/concepts/denotational-semantics.td"} - particularly for modeling recursion via ${fref"programming-language-theory/concepts/fixed-point-combinator.td"}s.Double negation eliminationholds. It asserts that if it is false that $A$ is false, then $A$ is true.Duck typingAn informal term for Structural typing - if an object has the required methods/properties \"quacks like a duck\", it can be used regardless of its declared type or class hierarchy.Dynamic dispatchA runtime mechanism that selects which method implementation to invoke based on the actual dynamic properties of the object, rather than the declared static properties of the reference, enabling polymorphic behavior. Contrast with ${fref"programming-language-theory/concepts/static-dispatch.td"}.Dynamic scopeThis is considered unambiguously wrong in language design - it makes programs unpredictable and tools unreliable.Dynamic semanticsThe meaning of programs in terms of their runtime behavior - how expressions evaluate, statements execute, and state changes over time.Dynamically sized type (DST)No description yetE26
Elimination ruleExample:Empty setA set with no element.EntailmentNo description yetEnumerated typeA data type that defines a fixed set of named values like enum Color { Red, Green, Blue }, enabling type-safe representation of discrete choices.Environment${fref"programming-language-theory/concepts/lambda-calculus.td"}, Semantics A finite map from variables to values, used to track substitutions during evaluation.Environment extensionThe operation $\\Gamma[x \\leftarrow t]$ that creates a new environment with all bindings from $\\Gamma$ plus variable $x$ bound to term/type/etc. $t$.EquivalenceA ${fref"programming-language-theory/concepts/reflexive.td"}, ${fref"programming-language-theory/concepts/transitive.td"} and ${fref"programming-language-theory/concepts/symmetric.td"} relation.Error recoveryNo description yetEta-equivalenceA relation that relates a term to its ${fref"programming-language-theory/concepts/eta-expansion.td"} - $\lambda x.\ f\ x =_\eta f$ when $x \notin FV(f)$ - capturing the principle that functions with identical input-output behavior are equivalent.Eta-expansionThe transformation of a term $t$ to $\lambda x.\ t\ x$ where $x \notin FV(f)$ - the inverse of ${fref"programming-language-theory/concepts/eta-reduction.td"}, often used to delay evaluation or make function abstraction explicit.Eta-reductionThe transformation of $\lambda x.\ t\ x$ to $t$ where $x \notin FV(f)$ - eliminating a redundant ${fref"programming-language-theory/concepts/lambda-abstraction.td"} when a function simply passes its argument unchanged to another function.Evaluation/Reduction relationAn n-place relation on the set of terms in a calculus that represents computation, either ${fref"programming-language-theory/concepts/small-step-structural-operational-semantics-sos.td"}, ${fref"programming-language-theory/concepts/big-step-natural-operational-semantics.td"} or something else.Evaluation reduction relation derivableAn n-place relation on the set of terms in a calculus that represents computation, either ${fref"programming-language-theory/concepts/small-step-structural-operational-semantics-sos.td"}, ${fref"programming-language-theory/concepts/big-step-natural-operational-semantics.td"} or something else.Evaluation statement/judgementA formal assertion of the form $t \to t'$ or $t \Downarrow v$, stating that a term reduces to another term or evaluates to a value under specific ${fref"programming-language-theory/concepts/inference-rule.td"}s.Evaluation strategyA specification of which ${fref"programming-language-theory/concepts/beta-redex-reducible-expression.td"} to reduce and in what order, determining how terms are evaluated e.g., ${fref"programming-language-theory/concepts/call-by-value.td"}, ${fref"programming-language-theory/concepts/call-by-name.td"}, ${fref"programming-language-theory/concepts/normal-order.td"}.Evaluation strategy strict eager evaluation strategy lazyA specification of which ${fref"programming-language-theory/concepts/beta-redex-reducible-expression.td"} to reduce and in what order, determining how terms are evaluated e.g., ${fref"programming-language-theory/concepts/call-by-value.td"}, ${fref"programming-language-theory/concepts/call-by-name.td"}, ${fref"programming-language-theory/concepts/normal-order.td"}.EvaluatorA program that turns programs into answersEvaluator interpreterNo description yetEventNo description yetEvent-based parsingNo description yetEvidenceNo description yetExpansionNo description yetExpressionSemantics, Syntax & Grammar, Language feature/design A syntactic construct that evaluates to a value, as opposed to a ${fref"programming-language-theory/concepts/statement.td"}.Expression problemNeither paradigm naturally supports both dimensions of extensibility without modifying existing code or sacrificing ${fref"programming-language-theory/concepts/type-safety.td"}. Solutions exist type classes, object algebras, tagless final but invoExpressivenessLanguage feature/design The ease and directness of expressing programmer intent - a more expressive feature allows saying something concisely and naturally e.g., pattern matching expresses variant dispatch more directly than chains of predicates + accessors; list comprehensions express transformations more naturally than explicit loops; distinct from computational power since both may be Turing-complete but differ in convenience.Extensible/Open recursionWhen utilizing the ${fref"programming-language-theory/concepts/class-pattern.td"} to define classes with method calls referencing other methods, a recursion pattern that allows method references to be resolved at call site.F30
FalsyA value that evaluates as false in a boolean context despite not being literally false like 0, null, \"\", or undefined in dynamic languages.FieldA named data member of a class or object that stores part of the object's state, accessed via dot notation or accessor methods.Finite typeA type with a bounded number of inhabitants like bool with 2 or enum with fixed variants, often enabling exhaustive enumeration or decidable equality.First-classCan be stored in variables.First class functional programming pureThe status of an entity being a first-class citizen in a language - typically:First-order variableA variable that ranges over data values e.g., integers, booleans, records - as opposed to ${fref"programming-language-theory/concepts/higher-order-function.td"} variables which can hold functions or other computational entities.Fixed-point combinatorTools: Rocq formerly CoqFixityA syntactic property specifying an operator's position relative to its arguments: prefix -x, infix x + y, or postfix x.Flow analysisA static analysis technique that tracks how information propagates through a program's control flow - determining what facts hold at each program point based on paths taken.Flow-sensitive typingSynonym for Flow typing - the type checker is \"sensitive\" to control flow, tracking how conditionals, assignments, and predicates refine types at different program points.Flow typingA type system feature where a variable's type changes based on control flow - after if x = null, the type of x narrows from T | null to T.Formal derivability judgmentNo description yetFormal generic judgmentNo description yetFormal parameterThe variable declared in a function definition that receive values when called - placeholders in the function signature.Formal systemA mathematical framework consisting of a syntax for forming statements, axioms taken as given, and inference rules for deriving new statements from existing ones.Forward chainingA proof technique for ${fref"programming-language-theory/concepts/judgment-form.td"}s that starts with an ${fref"programming-language-theory/concepts/axiom.td"} and tries to derive the desired judgment.Forward chaining backward chainingA proof technique for ${fref"programming-language-theory/concepts/judgment-form.td"}s that starts with an ${fref"programming-language-theory/concepts/axiom.td"} and tries to derive the desired judgment.Forward chaining forward chaining searchA proof technique for ${fref"programming-language-theory/concepts/judgment-form.td"}s that starts with an ${fref"programming-language-theory/concepts/axiom.td"} and tries to derive the desired judgment.Forward chaining searchA search strategy for a ${fref"programming-language-theory/concepts/derivation.td"} of a ${fref"programming-language-theory/concepts/judgment-form.td"} that keeps track of the currently derivable judgments initially the ${fref"programming-language-theory/concepts/axiom.td"}s and tries to expand the set using the rules at each step.Forward chaining search backward chaining searchA search strategy for a ${fref"programming-language-theory/concepts/derivation.td"} of a ${fref"programming-language-theory/concepts/judgment-form.td"} that keeps track of the currently derivable judgments initially the ${fref"programming-language-theory/concepts/axiom.td"}s and tries to expand the set using the rules at each step.Free variableA variable that is not bound by any enclosing $\lambda$. Contrast with ${fref"programming-language-theory/concepts/bound-variable.td"}.Fresh renamingGiven a set of variables $\\mathcal{X}$ and a finite sequence of variables $\\vec{x}$, a bijection $\\rho : \\vec{x} \\leftrightarrow \\vec{x}'$ between $\\vec{x}$ and $\\vec{x}'$, where $\\vec{x}'$ is fresh fFresh variableGiven a set of variable $\mathcal{X}$, a Variable $v \notin \mathcal{X}$.Fresh variable abstract syntax tree astGiven a set of variable $\mathcal{X}$, a Variable $v \not\in \mathcal{X}$.Full beta-reductionIn ${fref"programming-language-theory/concepts/pure-untyped-lambda-calculus.td"}, this strategy is defined by the following rules:FunctionLanguage feature/design A reusable piece of code that returns a result.Function definitionA syntactic construct that declares a function by specifying its name optionally, ${fref"programming-language-theory/concepts/formal-parameter.td"}s, and body - establishing a binding between the name and the corresponding abstraction.Function headerThe declarative part of a function that specifies its name, ${fref"programming-language-theory/concepts/formal-parameter.td"}s, and return type if any, without the body implementation.Function rocqUse the `Fixpoint` definition. For example:Functional programmingA programming paradigm centered on pure functions, immutability, and expressions rather than statements, treating computation as evaluation of mathematical functions.G16
GallinaA ${fref"programming-language-theory/concepts/functional-programming.td"} language ${fref"programming-language-theory/concepts/rocq.td"}'s specification language that allows writing purely functional programs and formal proofs, using ${fref"programming-language-theory/concepts/dependent-type.td"} to express precise logical properties.Garbage collectionAn ${fref"programming-language-theory/concepts/automatic-memory-management.td"} technique that identifies and reclaims ${fref"programming-language-theory/concepts/heap.td"}-allocated memory no longer reachable by the program, freeing the programmer from explicit deallocation and preventing memory leaks and dangling references.General judgmentNo description yetGeneric derivabilityNo description yetGeneric derivability judgmentNo description yetGeneric derivationNo description yetGeneric (general) judgmentNo description yetGeneric inductive definitionNo description yetGeneric ruleNo description yetGenericityNo description yetGlobal hypothesisNo description yetGlobal variableNo description yetGoalTools: Rocq formerly CoqGoal-directedThe property of an algorithm that is aware of its goal and uses that knowledge to take educated steps towards the goal, or in the case of ${fref"programming-language-theory/concepts/backward-chaining-search.td"}, starting from the goal, and working backwards towards the ${fref"programming-language-theory/concepts/axiom.td"}s.Gradual typingFully untyped <---------------> Fully typedGradual typing macro gradual typing micro gradual typingAn approach that allows mixing typed and untyped code in the same program, enabling incremental migration from dynamic to static typing.H15
HaltThe terminal state of an ${fref"programming-language-theory/concepts/abstract-machine.td"} reached when the current term is in ${fref"programming-language-theory/concepts/normal-form.td"} i.e., no evaluation rule applies, signaling completion of evaluation.HeapA region of a process's memory used for dynamic allocation at runtime, growing as needed and managed explicitly via malloc/free or by a ${fref"programming-language-theory/concepts/garbage-collection.td"} - as opposed to the stack which handles fixed-size, short-lived local variables and call frames.Heap addressAn address on the ${fref"programming-language-theory/concepts/heap.td"}.Higher-order contractContracts on values that are themselves functions or contain functions, presenting unique challenges because the contract cannot be fully checked immediately.Higher-order functionA function that accepts or returns another function.Hindley-Milner systemA type system with complete type inference via constraint generation and unification - automatically determines the most general principal type for all expressions without annotations; basis for ML,Hoare logicA formal system for reasoning about program correctness using triples {P} C {Q} precondition, command, postcondition to specify and verify imperative programs.Hoare type theoryA type theory that integrates Hoare-style specifications into types, allowing pre/postconditions and invariants to be expressed and checked within a dependently typed language.Host languageThe language a compiler is implemented in.Hygienic macroHygienic macros are analogous to ${fref"programming-language-theory/concepts/lexical-static-scope.td"} for ${fref"programming-language-theory/concepts/macro.td"}s: Macro variables are not just names, but rather binding information records.HypothesisFormal system, Proof/Reason technique, Language feature/design Rocq A named assumption in the proof context that can be used to justify proof steps, introduced by tactics like `intros` or `assert`.Hypothetical inductive definitionNo description yetHypothetical judgmentNo description yetHypothetical ruleNo description yetHypothetical rule inductionNo description yetI40
Identity combinatorFormula: $\text{id} = \lambda x.\ x$If-splittingA type system mechanism where conditionals narrow union types based on predicates - after if mt? t, the type of t refines from BT union to just mt in that branch, implementing Flow-sensitive typinImmediately invoked function expression (IIFE)Example: ${fref"programming-language-theory/concepts/parallel-simultaneous-let.td"} in Scheme is actually a ${fref"programming-language-theory/concepts/syntactic-sugar.td"} for IIFE.Implicit formNo description yetImportRocq A command in Rocq:/programming-language-theory/concepts/rocq that brings names from a loaded module/programming-language-theory/concepts/module into the current namespace, allowing unqualified access often combined as `Require Import`.Import requireNo description yetInadmissibleNo description yetIncomplete syntax treeNo description yetIncremental computationNo description yetIndexed operatorA family of operators $o$ indexed by symbols $u$, so that $o[u]$ is an operator when $u$ is an available symbol.Induction on derivationsAn induction technique in which to prove a specific property about a ${fref"programming-language-theory/concepts/derivation.td"}, we take the ${fref"programming-language-theory/concepts/inductive-hypothesis.td"} is that every smaller derivations satisfy that property.Inductive conclusionwe typically need to show:Inductive definitionTools: Rocq formerly CoqInductive definition 2 dimensional inference rule formatA definition technique that specifies a set or type by its base cases and rules for building new elements from existing ones.Inductive definition functionA definition technique that specifies a set or type by its base cases and rules for building new elements from existing ones.Inductive definition judgment formA definition technique that specifies a set or type by its base cases and rules for building new elements from existing ones.Inductive definition termA definition technique that specifies a set or type by its base cases and rules for building new elements from existing ones.Inductive hypothesiswe typically need to show:Inductive typeTools: Rocq formerly CoqInference ruleLogic A formal statement consisting of ${fref"programming-language-theory/concepts/premise.td"}s and a ${fref"programming-language-theory/concepts/conclusion.td"}, asserting that if all premises hold, the conclusion may be derived.Infinite typeA type that has infinitely many inhabitants like nat, string, or list, as opposed to finite types like bool or enums with fixed members.InfixA Fixity where an operator appears between its two arguments like x + y, as opposed to prefix or postfix.InheritanceA mechanism where a class subclass derives properties and behaviors from another class superclass, enabling code reuse and establishing an \"is-a\" relationship between types. This coupling betweenInheritance subtypingNo.Input queryNo description yetInstance of a rule schemeSynonymous with ${fref"programming-language-theory/concepts/instance-of-an-inference-rule.td"}.Instance of an inference ruleA specific substitution of the rule's ${fref"programming-language-theory/concepts/metavariable.td"}s with concrete terms, yielding a particular ${fref"programming-language-theory/concepts/derivation.td"} step.Instance of the judgment formA ${fref"programming-language-theory/concepts/judgment-form.td"} applied with one or more values. For a judgment form $-\ J$ and a value $a$, it is written as $a\ J$ or $J\ a$.InternerNo description yetInterning tableNo description yetInterpretationA semantic mapping that assigns meaning to a Representation e.g., 0b101 can interpret as 5 in binary or a bit pattern.Interpretation functionA function mapping syntactic terms to mathematical objects denotations in a ${fref"programming-language-theory/concepts/semantic-domain.td"}, assigning meaning compositionally based on the structure of terms.InterpreterMathematically, denote $\mathcal{P}_L$ as the set of programs written in the language $L$ and $V$ the set of all possible values, an interpreter is a function $I: \mathcal{P}_L \to V$.Intro patternRocq A tactic modifier/programming-language-theory/concepts/tactic-modifier in Rocq:/programming-language-theory/concepts/rocq that destructures hypothesis/programming-language-theory/concepts/hypothesises as they're introduced like `intros [x y]` to unpack a pair or `intros [H|H]` for a disjunction.Introduction ruleExample:Intuitionistic/Constructive logic\\frac{A \\quad B}{A \\land B} & & \\land\\text{-intro} \\\\ \\\\InvolutionA function that is its own inverse, satisfying ffx = x like negation on booleans or reversing a list twice.InvolutiveA property of a function where applying it twice returns the original value i.e., ffx = x.Iterated inductive definitionAn ${fref"programming-language-theory/concepts/inductive-definition.td"} technique that specifies a set of elements as the strongest sets closed under a set of ${fref"programming-language-theory/concepts/inference-rule.td"}s - each inference rule may only refer to already defined sets or the currently defined one.Iterated inductive definition simultaneous inductiveAn ${fref"programming-language-theory/concepts/inductive-definition.td"} technique that specifies a set of elements as the strongest sets closed under a set of ${fref"programming-language-theory/concepts/inference-rule.td"}s - each inference rule may only refer to already defined sets or the currently defined one.J6
JoinIn the context of a ${fref"programming-language-theory/concepts/partial-order.td"}, the least upper bound of a set $S$, denoted $\bigvee S$.JudgmentLogic The mental act of affirming or denying a ${fref"programming-language-theory/concepts/proposition.td"} is true.Judgment assertion judgment form judgment form instancesA ${fref"programming-language-theory/concepts/judgment-form.td"} is a relation, interpreted as a ${fref"programming-language-theory/concepts/predicate.td"}.Judgment formSynonymous with an n-place relation. For a unary relation/predicate, a judgment form is usually written as $J\\ -$ or $-\\ J$, with $-$ being a placeholder for some value drawn from the domain of the prJudgment judgment formSynonymous with an n-place relation. For a unary relation/${fref"programming-language-theory/concepts/predicate.td"}, a ${fref"programming-language-theory/concepts/judgment-form.td"} is usually written as $J\ -$ or $-\ J$, with $-$ being a placeholder for some value drawn from the domain of the predicate.Just-in-time (JIT) compilationAn ${fref"programming-language-theory/concepts/evaluator.td"} that starts out as an ${fref"programming-language-theory/concepts/interpreter.td"} but includes a monitor to detect, compile and utilize compiled hot code.L28
Labeled treeSynonymous with Abstract syntax tree AST/plt/concepts/abstract-syntax-tree-ast.Lambda abstractionA ${fref"programming-language-theory/concepts/lambda-term.td"} of the form $\lambda x.\ t$ - a function that binds variable $x$ over body $t$.Lambda abstraction lambda calculusA ${fref"programming-language-theory/concepts/lambda-term.td"} of the form $λx.\ t$ - a function that binds variable $x$ over body $t$.Lambda calculusA minimal formal system for expressing computation using only variable binding and function application, yet serves as a foundation that can be extended with types, effects, recursion primitives, and other constructs to form the basis of modern programming languages.Lambda expressionA syntactic construct denoting an anonymous function, consisting of a list of ${fref"programming-language-theory/concepts/formal-parameter.td"}s and a body - e.g., $\lambda x.\ t$ or $(\text{lambda}\ (x)\ t)$.Lambda termAny expression in the ${fref"programming-language-theory/concepts/lambda-calculus.td"} grammar: a variable, an ${fref"programming-language-theory/concepts/lambda-abstraction.td"}, or an application.Language safetyLanguage feature/design, Runtime According to Types and programming languages, from the view of portability, a language whose behavior can be entirely determined by its programmer's manual, that is, it is not subject to the internals of the specific machine it runs on.Language safety partialityAccording to Types and programming languages, a language that protects its own abstraction, that is, it is mostly impossible to corrupt the run-time’s data structure and program’s data structure although there can be escape hatches to perform unsafe operations.Law of excluded middle (LEM)holds. It asserts that every statement is either true or false, with no middle ground.Lazy evaluation strategyLanguage feature/design An ${fref"programming-language-theory/concepts/evaluation-strategy.td"} in which the argument is not evaluated before substituted into the function call.Left-left-lambdaReading left-to-right: `(` `(` `lambda` -> "left-left-lambda".Lexical analysisSyntax & Grammar, Linguistics The process of classifying texts into ${fref"programming-language-theory/concepts/syntactic-category.td"}s.Lexical analysis parsingA step in the ${fref"programming-language-theory/concepts/compiler.td"} that involves converting texts into sequences of ${fref"programming-language-theory/concepts/token.td"}s. This typically involves:Lexical/Static scopeA ${fref"programming-language-theory/concepts/binding.td"} resolution strategy where a variable's binding is determined by its textual position in the source code - the enclosing ${fref"programming-language-theory/concepts/scope.td"} at the point of definition, not the call site at runtime.Lexicographic orderA total ordering on sequences that compares elements position-by-position from left to right, with the first differing position determining precedence - like dictionary ordering of words.Lexicographic order principle of lexicographic inductionA total ordering on sequences that compares elements position-by-position from left to right, with the first differing position determining precedence - like dictionary ordering of words.LifetimeNo description yetLight-parsingNo description yetLinkWhat do you want to grasp from this question?Liskov substitution principle (LSP)A design principle for OO inheritance stating that subtypes must preserve behavioral contracts of supertypes, ensuring code using parent class works correctly with any child class - preventing bugs frLiteralSynonymous with syntactic ${fref"programming-language-theory/concepts/constant.td"}.Local binding form; Local binding - x only exists inside the letLocal formNo description yetLocal hypothesisNo description yetLocal variableA variable declared within a ${fref"programming-language-theory/concepts/block.td"} or function whose ${fref"programming-language-theory/concepts/scope.td"} and ${fref"programming-language-theory/concepts/lifetime.td"} are limited to that region - inaccessible from outside and typically deallocated when the block exits.LogicA ${fref"programming-language-theory/concepts/formal-system.td"} for reasoning about truth, validity, and inference, defining syntax for propositions and rules for deriving conclusions.Logical derivationA step-by-step proof showing how a conclusion follows from premises using ${fref"programming-language-theory/concepts/inference-rule.td"}s - each step applies a rule to previous steps; in type systems, a ${fref"programming-language-theory/concepts/derivation-tree.td"} is a derivation proving that anLogical systemA formal framework comprising a syntax well-formed formulas, ${fref"programming-language-theory/concepts/axiom.td"}s, and ${fref"programming-language-theory/concepts/inference-rule.td"}s that together determine which statements are ${fref"programming-language-theory/concepts/derivable.td"}.M32
MacroA syntactic pattern that is expanded into other code at compile time via ${fref"programming-language-theory/concepts/macro-expansion.td"}, enabling metaprogramming by allowing code to generate or transform other code before execution.Macro definition hazard: duplicationA ${fref"programming-language-theory/concepts/macro.td"} pitfall where an expression passed as argument is evaluated multiple times in the ${fref"programming-language-theory/concepts/macro-expansion.td"}, causing unintended repeated ${fref"programming-language-theory/concepts/side-effect.td"}s or performance issues.Macro expansionA compile-time code transformation where macro invocations are replaced by their expanded definitions, enabling ${fref"programming-language-theory/concepts/syntactic-abstraction.td"} and code generation before regular compilation.Macro gradual typingA ${fref"programming-language-theory/concepts/gradual-typing.td"} approach where typed and untyped code exist as two separate sibling languages that interact only at module boundaries, typically requiring ${fref"programming-language-theory/concepts/blame-tracking.td"}.Macro hygienic macroA ${fref"programming-language-theory/concepts/macro-system.td"} that automatically renames variables to prevent accidental ${fref"programming-language-theory/concepts/variable-capture.td"}, ensuring that identifiers introduced by the macro don't clash with identifiers at the call site.Macro parenthetical languageNo description yetMacro side effectNo description yetMacro systemA language facility that provides programmable syntax transformations through ${fref"programming-language-theory/concepts/macro.td"}s, enabling users to define new syntactic forms that expand into existing language constructs at compile time.ManglingNo description yetMap-ReduceA ${fref"programming-language-theory/concepts/programming-model.td"} that processes large datasets by applying a function to each element map then combining results with an associative operation reduce, enabling parallelization.Match armNo description yetMathematical inductionFormally, assume $n\ \text{nat}$ means that $n$ is a natural number. To prove that whenever $n\ \text{nat}$, we have $\mathcal{P}(n)$, it's sufficient to show that:MeetIn the context of a ${fref"programming-language-theory/concepts/partial-order.td"}, the greatest lower bound of a set $S$, denoted as $\bigwedge S$ .Message passingNo description yetMeta-mathematicsThe study of mathematical systems themselves using mathematical methods - analyzing properties like consistency, completeness, and decidability of formal theories.MetalanguageThe language used to describe, define, or reason about another language ${fref"programming-language-theory/concepts/object-language.td"} - e.g., English and mathematical notation when specifying ${fref"programming-language-theory/concepts/lambda-calculus.td"}.MetatheoryThe study of properties about a ${fref"programming-language-theory/concepts/formal-system.td"} e.g., ${fref"programming-language-theory/concepts/sound.td"}ness, ${fref"programming-language-theory/concepts/completeness.td"}, termination, using external reasoning to prove facts about the system itself.MetavariableA variable in the ${fref"programming-language-theory/concepts/metalanguage.td"} that ranges over elements of a ${fref"programming-language-theory/concepts/syntactic-category.td"} in the object language - e.g., $t$ ranging over terms, $v$ over values, $x$ over variables.MethodA function defined within a class that operates on instances of that class, typically bound to and having implicit access to the object's state through this or self.Method functionA ${fref"programming-language-theory/concepts/method.td"} is a function that gets bound to an ${fref"programming-language-theory/concepts/object.td"}.Micro gradual typingA ${fref"programming-language-theory/concepts/gradual-typing.td"} approach where type annotations can be added to any subset of variables within the same code, freely mixing typed and untyped expressions.MixfixA notation to write down an instance of an ${fref"programming-language-theory/concepts/n-place-relation.td"}. For example, for a ternary relation $R$, one can write $\Gamma \vdash t : T$ to denote $(\Gamma, t, T) \in R$.MixinA function that transforms a class into another class, typically adding behaviors to it assuming the class conforms to an interface, similar to a ${fref"programming-language-theory/concepts/class-extension.td"}.Model checkerAn automated verification technique that exhaustively explores the state space of a typically finite-state system to detect violations of specified properties such as safety, liveness, or protocol correctness.Model checker type system runtime monitoringAn automated verification technique that exhaustively explores the state space of a typically finite-state system to detect violations of specified properties such as safety, liveness, or protocol correctness.ModularizationPapers: On the Criteria To Be Used in Decomposing Systems into Modules ../../Papers/Papers/On%20the%20Criteria%20To%20Be%20Used%20in%20Decomposing%20Systems%20%2031baa8fcd08880429536c92add4ffb42.mdModulePapers: On the Criteria To Be Used in Decomposing Systems into Modules ../../Papers/Papers/On%20the%20Criteria%20To%20Be%20Used%20in%20Decomposing%20Systems%20%2031baa8fcd08880429536c92add4ffb42.mdModule systemA language feature that organizes code into namespaced units with controlled visibility, enabling encapsulation, separate compilation, and abstraction through signatures/interfaces.Multi-step evaluation relationThe ${fref"programming-language-theory/concepts/reflexive-closure.td"} and ${fref"programming-language-theory/concepts/transitive-closure.td"} of the ${fref"programming-language-theory/concepts/one-step-evaluation-relation.td"}. The relation is often denoted as $\to^*$.Multiple inheritanceAn ${fref"programming-language-theory/concepts/inheritance.td"} model where a class can inherit from multiple parent classes, combining their behaviors but potentially introducing ambiguity ${fref"programming-language-theory/concepts/the-diamond-problem.td"} when parents share method names.MutableThe property of an entity variable, data structure, reference whose contents can be modified in place after creation.MutationThe act of modifying a value in place at a memory location, rather than producing a new value - introducing ${fref"programming-language-theory/concepts/state.td"} changes that depend on evaluation order and complicating equational reasoning.N12
N-place relationGiven $n$ sets $X_1, X_2, ..., X_n$, the subset of the Cartesian product $X_1 \times X_2 \times ... \times X_n$.Name combination algebraThe set of rules governing how names interact when combining program fragments, addressing whether bindings ${fref"programming-language-theory/concepts/shadowing.td"}, conflict, or merge central to understanding ${fref"programming-language-theory/concepts/substitution.td"}, ${fref"programming-language-theory/concepts/scope.td"}, and module composition.Natural deduction styleA presentation of ${fref"programming-language-theory/concepts/logical-system.td"}s where ${fref"programming-language-theory/concepts/inference-rule.td"}s are organized into ${fref"programming-language-theory/concepts/introduction-rule.td"} and ${fref"programming-language-theory/concepts/elimination-rule.td"} for each connective, with proofs structured as trees that introduce and discharge assumptions.Newtype idiomNo description yetNodeNo description yetNominal typeA type identified by its name - two types are equal only if they have the same declared name, regardless of structure.Nominal typingA type system where ${fref"programming-language-theory/concepts/type-compatibility.td"} is determined by explicit declarations class names, inheritance hierarchy, not structure - class A and class B are different even if identical in shape.Nominal typing structural typingA type system where ${fref"programming-language-theory/concepts/type-compatibility.td"} is determined by explicit declarations class names, inheritance hierarchy, not structure - `class A` and `class B` are different even if identical in shape.Nonsensical termExample: In the ${fref"programming-language-theory/concepts/untyped-calculus-of-booleans-and-numbers.td"}, the followings are nonsensical:Normal formA term that cannot be evaluated further.Normal form valueA term that cannot be evaluated further.Normal orderIn pure lambda calculus, this strategy is defined by the following rules:O16
ObjectA multi-entrypoint ${fref"programming-language-theory/concepts/closure.td"} that can be accessed using ${fref"programming-language-theory/concepts/message-passing.td"}.Object closureAn ${fref"programming-language-theory/concepts/object.td"} is a ${fref"programming-language-theory/concepts/closure.td"} with multiple entrypoints.Object lambda expressionNo description yetObject languageThe formal language being defined, analyzed, or reasoned about - as opposed to the ${fref"programming-language-theory/concepts/metalanguage.td"} used to describe it.Object memberA component of an object, either a ${fref"programming-language-theory/concepts/field.td"} data or a ${fref"programming-language-theory/concepts/method.td"} behavior.Object patternNo description yetOccurrence typingA type system technique where a variable's type can differ at each occurrence use based on what predicates have been checked - the same variable x can have type Number in one branch and String in another. Synonymous with ${fref"programming-language-theory/concepts/flow-typing.td"}.On-demand computationNo description yetOne-step evaluation relationA relation defining a single atomic reduction, mapping a term to its immediate successor by applying exactly one reduction rule. The relation is denoted using the symbol $\to$.One step evaluation relation partial functionA relation defining a single atomic reduction, mapping a term to its immediate successor by applying exactly one reduction rule. The relation is denoted using the symbol $\to$.Operational semanticsA style of semantics that defines the meaning of programs by syntactically transforming terms according to reduction rules, specifying execution either step-by-step ${fref"programming-language-theory/concepts/small-step-structural-operational-semantics-sos.td"} or as a direct relation to final values ${fref"programming-language-theory/concepts/big-step-natural-operational-semantics.td"}.Operational semantics untyped calculus of booleans andA style of semantics that defines the meaning of programs by syntactically transforming terms according to reduction rules, specifying execution either step-by-step Small-step/Structural operational semantics SOSSmall-step%20Structural%20operational%20semantics%20SOS%202c7aa8fcd08880f1b83aecba03d1192e.md or as a direct relation to final values Big-step/Natural operational semantics.OperatorAccording to Practical foundations for programming languages , an interior node of an Abstract syntax tree AST/plt/concepts/abstract-syntax-tree-ast, with a specified Arity $(s_1;\dots; s_n)s$, for $s_i \in \mathcal{S}$ - the set of Sorts.Operator abstract syntax tree astNo description yetOperator arityNo description yetOrdered variadic treeNo description yetP49
Pair encodingEncoding:Parallel/Simultaneous letPython's multi-assignment's semantic is similar to parallel let:Parametric (general) judgmentNo description yetParenthetical languagedefine-syntax-rule or a b if a a bParsingCompiler implementation The process of converting Concrete/Surface syntax into Abstract syntax tree AST/plt/concepts/abstract-syntax-tree-asts.Partial functionA ${fref"programming-language-theory/concepts/binary-relation.td"} $R$ such that if $s\ R\ t_1$ and $s\ R\ t_2$ then $t_1 = t_2$.Partial orderA ${fref"programming-language-theory/concepts/binary-relation.td"} that is ${fref"programming-language-theory/concepts/transitive.td"}, ${fref"programming-language-theory/concepts/reflexive.td"} and ${fref"programming-language-theory/concepts/antisymmetric.td"}.PartialityThe property of a computation that may not terminate or produce a result for all inputs. ${fref"programming-language-theory/concepts/partial-function.td"}s are undefined for some inputs, unlike ${fref"programming-language-theory/concepts/total-function.td"}s which always return a value.PatternA structural template that matches values by shape using constructors, variables, or wildcards, enabling destructuring and case analysis in match expressions.Pattern matchingA language construct that deconstructs ${fref"programming-language-theory/concepts/algebraic-data-type.td"} values by variant, binding fields to variables and enabling the type checker to refine types in each branch - safer than raw predicates + accessors.Polymorphic type systemA type system that allows types to contain variables like List<T>, $\forall$ a. a $\to$ a, enabling one definition to work across many types through type abstraction.PowersetDefinition: $\mathcal{P}(S) = \{ s\ |\ s \subseteq S \}$ .Pratt parsingNo description yetPrecedenceA parsing rule that determines which operator binds tighter e.g., `*` before `+` makes `1 + 2 * 3` parse as `1 + (2 * 3)`.PredicateAn unary n-place relation $P$, $(s) \in P$ is typically written as $P(s)$.Predicate typeA function type annotated with what it proves when returning true - e.g., -> Any Boolean : mt means \"takes anything, returns Boolean, and when true, input was mt.\" Essentially, a type of a Type predPremiseAn antecedent judgment in an ${fref"programming-language-theory/concepts/inference-rule.td"} that must be ${fref"programming-language-theory/concepts/derivable.td"} for the rule to derive its ${fref"programming-language-theory/concepts/conclusion.td"}.PreorderA ${fref"programming-language-theory/concepts/binary-relation.td"} that is ${fref"programming-language-theory/concepts/reflexive.td"} and ${fref"programming-language-theory/concepts/transitive.td"}.Primordial blockThe implicit outermost scope containing built-in definitions e.g., primitive types, standard functions that encloses the global scope, making built-ins available without explicit import.Principle of complete inductionA proof technique where the inductive step assumes the property holds for all predecessors not just the immediate one, deriving the property for the current element.Principle of lexicographic inductionA proof technique using ${fref"programming-language-theory/concepts/lexicographic-order.td"} on tuples of measures, allowing induction where each recursive step decreases the tuple lexicographically - any component may increase if an earlier component strictly decreases.Principle of ordinary inductionA proof technique with a base case and an inductive step that assumes the property holds for the immediate predecessor to prove it for the successor.Private memberA class member that is only accessible from within the class itself, providing encapsulation by hiding implementation details from external code.Procedural/Functional abstractionThe principle of encapsulating a computation behind a named interface, hiding implementation details and allowing reuse by parameterizing over inputs.ProcedureA subroutine that performs actions primarily for ${fref"programming-language-theory/concepts/side-effect.td"}s rather than returning a value. Unlike functions, procedures emphasize imperative steps over computation of results.ProgramThe start symbol representing a complete, well-formed unit of code - the top-level nonterminal from which all valid programs are derived.Programming modelA conceptual framework defining how computations are structured and executed like shared memory, ${fref"programming-language-theory/concepts/message-passing.td"}, or ${fref"programming-language-theory/concepts/map-reduce.td"}, abstracting over hardware details.Programming paradigmA style or philosophy of programming characterized by its core concepts and patterns like functional, imperative, object-oriented, or logic programming.ProliferationNo description yetProofTools: Rocq formerly CoqProof assistant/proverTools: Rocq formerly CoqProof by case analysisTools: Rocq formerly CoqProof by rewritingProof/Reason technique, Logic A ${fref"programming-language-theory/concepts/proof-technique.td"} that transforms expressions by substituting equals for equals, using known equalities to reshape the ${fref"programming-language-theory/concepts/goal.td"}.Proof by simplificationTools: Rocq formerly CoqProof checkerA program that verifies whether a given proof is valid according to the rules of a ${fref"programming-language-theory/concepts/formal-system.td"}, confirming that each step correctly follows from the ${fref"programming-language-theory/concepts/axiom.td"}s and ${fref"programming-language-theory/concepts/inference-rule.td"}s.Proof techniqueFormal system, Proof/Reason technique, Language feature/design, Programming paradigm Rocq In Rocq, a conceptual strategy for proving goals like induction or case analysis, typically realized by corresponding tactics.Proper ruleAn ${fref"programming-language-theory/concepts/inference-rule.td"} that is not an ${fref"programming-language-theory/concepts/axiom.td"}, in other words, has at least one ${fref"programming-language-theory/concepts/premise.td"}s.Proposition-> true/false do not merely \"corresponds to reality.\"PrototypeAn object that serves as a template for creating other objects through cloning, used in prototype-based languages like JavaScript as an alternative to class-based ${fref"programming-language-theory/concepts/inheritance.td"}, generalizing class-based inheritance.Prototype classCreate a prototype object that contains all the shared methods and default properties.PureThe property of a function or computation that has no side effects and always returns the same output for the same input, making it referentially transparent.Pure type systemA general framework parameterizing typed lambda calculi by a triple sorts, axioms, rules, unifying systems like ${fref"programming-language-theory/concepts/simply-typed-lambda-calculus.td"}, System F, and the ${fref"programming-language-theory/concepts/calculus-of-inductive-construction.td"} under a single formalism.Pure/Untyped lambda calculusNo description yetPure untyped lambda calculus call by valueNo description yetPure untyped lambda calculus church numeralNo description yetPure untyped lambda calculus curryingNo description yetPure untyped lambda calculus pair encodingNo description yetPure untyped lambda calculus runtime error stuck termNo description yetPure untyped lambda calculus syntactic categoryNo description yetR42
RangeSynonymous with ${fref"programming-language-theory/concepts/codomain.td"}.Read-eval-print-loop (REPL)A program that provides an interactive interface for programmers to interact with a programming language in an adhoc and highly-responsive fashion. The name represents the typical phases of this interaction: The program reads the input from the user, evaluates it, prints out the result and loops.Read eval print loop repl compiler interpreterA program that provides an interactive interface for programmers to interact with a programming language in an adhoc and highly-responsive fashion. The name represents the typical phases of this interaction: The program reads the input from the user, evaluates it, prints out the result and loops.Recursive descentNo description yetRecursive descent parserNo description yetRecursive letNo description yetRecursive macroA ${fref"programming-language-theory/concepts/macro.td"} that can expand to code containing further macro invocations, including calls to itself. Enables powerful metaprogramming but requires careful handling to ensure termination.Recursive typeA type whose definition reference itself.Refined typeA type that carries additional constraints beyond the base type, such as \"positive integers\" or \"non-null strings\". Enables more precise specifications and stronger compile-time guarantees.ReflexiveA property of a ${fref"programming-language-theory/concepts/binary-relation.td"} $R$ on a set $T$ such that $t\ R\ t$ for every $t \in T$.Reflexive closureThe smallest superset of a set that is reflexive.Reflexive transitiveNo description yetReflexivityTools: Rocq formerly CoqRenamingNo description yetRepresentationA concrete encoding of abstract data e.g., the numeral 5 can be represented as \"101\", SSSSS O, or 0x05.RequireRocq A command in Rocq that loads a compiled module into memory, making its contents available but not directly accessible without qualification.Retrofitted type systemA ${fref"programming-language-theory/concepts/type-system.td"} added to an existing untyped language after the fact - must accommodate existing idioms and codebases rather than designing types from scratch.RiceA theorem stating that any non-trivial semantic property of programs is ${fref"programming-language-theory/concepts/decidability.td"} - we cannot automatically determine arbitrary properties about what programs compute e.g., "does this function always return a positive number?", which is why type systems must be conservative approximations.RocqTools: Rocq formerly CoqRocq axiomNo description yetRocq church numeralNo description yetRocq constructor function computation ruleA ${fref"programming-language-theory/concepts/constructor-expression.td"} is an expression constructed using a ${fref"programming-language-theory/concepts/constructor.td"}, effectively creating a member of a set represented by a type.Rocq dependent typeNo description yetRocq gallinaNo description yetRocq inductive definitionIt allows defining ${fref"programming-language-theory/concepts/algebraic-data-type.td"}s in Rocq, including ${fref"programming-language-theory/concepts/recursive-type.td"}s.Rocq kernelTools: Rocq formerly CoqRocq tacticNo description yetRocq truthyThe first constructor of an inductive type that has two constructors.RoslynNo description yetRuleShort-hand for ${fref"programming-language-theory/concepts/inference-rule.td"}.Rule inductionwe typically need to show:Rule schemaAn parameterized inference rules with ${fref"programming-language-theory/concepts/metavariable.td"}s that can be instantiated to ${fref"programming-language-theory/concepts/concrete-rule.td"}s or ${fref"programming-language-theory/concepts/inference-rule.td"}s.Rule schema inference rule concrete rule instance of anAn parameterized inference rules with ${fref"programming-language-theory/concepts/metavariable.td"}s that can be instantiated to ${fref"programming-language-theory/concepts/concrete-rule.td"}s or ${fref"programming-language-theory/concepts/inference-rule.td"}s.Rule schemeSynonymous with ${fref"programming-language-theory/concepts/rule-schema.td"}.Rule scheme inference rule metavariableSynonymous with ${fref"programming-language-theory/concepts/rule-schema.td"}.Runtime errorRuntime An error that happens at runtime.Runtime monitoringA dynamic verification technique that inserts observers to track program execution and detect when behavior deviates from specified properties e.g., ${fref"programming-language-theory/concepts/contract.td"}s, protocols, temporal constraints.Runtime type dispatchA pattern typically associated with ${fref"programming-language-theory/concepts/union-type.td"}s in which the type of a value is checked so that specialized logic can be carried out. ${fref"programming-language-theory/concepts/flow-sensitive-typing.td"} is especially useful.Runtime type errorAccording to Types and programming languages, the class of undefined or undesirable behaviors that a ${fref"programming-language-theory/concepts/type-system.td"} is designed to prevent - whether they are actually eliminated depends on the soundness of the type system.Runtime type information (RTTI)A mechanism that allows the reflection of the type of a value at runtime.Rust crateNo description yetRust moduleNo description yetS75
S-expression/Symbolic expressionA notation for nested list-structured data, defined recursively as either an atom e.g., number, symbol or a parenthesized list of S-expressions - the uniform syntax used in Lisp for both code and data.Safe/Sound type systemA ${fref"programming-language-theory/concepts/type-system.td"} where the static judgment "term $t$ has type $T$" implies a corresponding semantic property at runtime - formalized as: if the type system accepts a program, execution cannot produce behaviors the types claim to exclude.Safety checkA mechanism, either carried out by the runtime to enforce ${fref"programming-language-theory/concepts/language-safety.td"} / avoid ${fref"programming-language-theory/concepts/runtime-type-error.td"} or by programmers to avoid ${fref"programming-language-theory/concepts/runtime-error.td"}.SAT solverA ${fref"programming-language-theory/concepts/decision-procedure.td"} that determines whether a propositional boolean formula has a satisfying assignment, foundational to many automated reasoning tools.ScopeSemantics The region of the code that a ${fref"programming-language-theory/concepts/binding.td"} takes effect.Scope bindingNo description yetSelf-referenceProgramming paradigm A technique in the ${fref"programming-language-theory/concepts/class-pattern.td"} that allows members of a class to reference their owner objects.Self-replicatorExample:Semantic domainThe mathematical structure e.g., sets, functions, lattices in which terms are given meaning by a ${fref"programming-language-theory/concepts/denotational-semantics.td"}.Sentence diagramA syntactic structure of a given sentence.SequenceAn ordered collection of elements indexed by natural numbers - formally, a function from $\mathbb{N}$ to some set, denoted $(a_0, a_1, a_2, ...)$ or $(a_i)_i\in\mathbb{N}$.Sequential evaluationAn execution model where expressions or statements are evaluated one after another in a specified order, with each completing before the next begins - the default in imperative languages, contrasted with parallel or concurrent evaluation.Set comprehensionExample: $\mathbb{Q} = \{\displaystyle \frac{p}{q}\ |\ p \in \mathbb{Z} \land q \in \mathbb{Z} \land q \neq 0 \}$.Set differenceDefinition: $R - Q = \{x \ | \ x \in R \land \ x \notin Q \}$.ShadowingThe phenomenon when an inner ${fref"programming-language-theory/concepts/binding.td"} uses the same name as an outer binding, making the outer one inaccessible within the inner ${fref"programming-language-theory/concepts/scope.td"}.Side-effectAn observable interaction with the outside world or modification of state beyond returning a value, such as I/O, mutation, or exceptions.Simply typed lambda calculusThe foundational typed lambda calculus where each ${fref"programming-language-theory/concepts/lambda-abstraction.td"} explicitly annotates its parameter with a type, providing a basis for more advanced type systems while guaranteeing termination.Simultaneous inductive definitionA definition technique that define more than one sets at once as a collection of ${fref"programming-language-theory/concepts/inference-rule.td"}s to determine membership of the elements of the sets - each inference rule shall refer to the sets in its ${fref"programming-language-theory/concepts/premise.td"}s and its ${fref"programming-language-theory/concepts/conclusion.td"}s.Small omega combinatorA ${fref"programming-language-theory/concepts/combinator.td"} defined as $\omega = \lambda x.\ x\ x$, useful in many patterns, such as ${fref"programming-language-theory/concepts/extensible-open-recursion.td"}.Small-step/Structural operational semantics (SOS)A style of semantics which defines evaluation via ${fref"programming-language-theory/concepts/evaluation-statement-judgement.td"} of the form $t \to t'$, specifying how a term reduces by one atomic step at a time until reaching a ${fref"programming-language-theory/concepts/normal-form.td"}.SMT solverA ${fref"programming-language-theory/concepts/decision-procedure.td"} that determines satisfiability of formulas in first-order logic with theories like arithmetic, arrays, bit-vectors, extending ${fref"programming-language-theory/concepts/sat-solver.td"} to richer domains.SortA Syntactic category that classifies Abstract syntax tree AST/plt/concepts/abstract-syntax-tree-asts. Roughly a type for ASTs.SoundThe adjective form of ${fref"programming-language-theory/concepts/soundness.td"}.SoundnessNo description yetStableNo description yetStateThe complete configuration of an ${fref"programming-language-theory/concepts/abstract-machine.td"} at a point during evaluation, comprising the current term and any auxiliary data e.g., ${fref"programming-language-theory/concepts/environment.td"}, store, stack. In ${fref"programming-language-theory/concepts/pure-untyped-lambda-calculus.td"}, the state is simply a ${fref"programming-language-theory/concepts/lambda-term.td"}.StatementA ${fref"programming-language-theory/concepts/term.td"} that does not evaluate to a value, but rather cause a ${fref"programming-language-theory/concepts/side-effect.td"}.Static analysisProgram analysis performed without executing the code, including type checking, dataflow analysis, and abstract interpretation. Can detect certain errors and properties before runtime.Static disciplineAn approach where ${fref"programming-language-theory/concepts/static-analysis.td"} and other analyses are performed before program execution, catching errors at compile time rather than runtime. Contrasts with dynamic discipline.Static dispatchMethod resolution that occurs at compile time based on some known may be imprecise static properties such as types of the receiver, as opposed to ${fref"programming-language-theory/concepts/dynamic-dispatch.td"} which resolves at runtime based on the actual dynamic properties.Static memberA field or method that belongs to the ${fref"programming-language-theory/concepts/class.td"} itself rather than to instances, shared across all objects of that class and accessible without creating an instance.Static semanticsThe meaning of programs determinable without execution - type checking, scope resolution, and other compile-time analyses that reject ill-formed programs.Static typeA type that is determined and checked at compile time, before the program runs, as opposed to dynamic types which are checked at runtime.Strength reductionNo description yetStrict/Eager evaluation strategyLanguage feature/design An ${fref"programming-language-theory/concepts/evaluation-strategy.td"} such that an argument is evaluated before passing into the function call.String internerNo description yetStrong normalizationThe property of a language written in which every program always terminates.StructuralNo description yetStructural/Abstract syntaxSyntax & Grammar According to Practical foundations for programming languages, the program's tree structure Abstract syntax tree AST/plt/concepts/abstract-syntax-tree-ast showing how phrases are built from ${fref"programming-language-theory/concepts/operator.td"}s and subphrases.Structural abstract syntax concrete surface syntaxSyntax & Grammar According to Practical foundations for programming languages, the program's tree structure Abstract syntax tree AST/plt/concepts/abstract-syntax-tree-ast showing how phrases are built from ${fref"programming-language-theory/concepts/operator.td"}s and subphrases.Structural inductionA proof technique for inductively defined structures, where a property is shown for all elements by proving base cases and proving composite cases assuming the property holds for all immediate sub-structures.Structural induction modulo fresh renamingTo show that $\\mathcal{P}[\\mathcal{X}](a)$ holds for every $a \\in \\mathcal{B}[\\mathcal{X}]$, it is enough to show the following:Structural propertyNo description yetStructural recursionA recursion scheme that decomposes data along its ${fref"programming-language-theory/concepts/constructor.td"}s, guaranteeing termination by recursing only on structurally smaller subterms.Structural ruleNo description yetStructural typeA type defined by its shape fields, methods, signatures rather than its name - two types are equal if they have the same structure.Structural typingA type system where ${fref"programming-language-theory/concepts/type-compatibility.td"} is determined by structure, not name - any value with matching shape satisfies the type, regardless of declared class or origin.StructuralityNo description yetStuck termA ${fref"programming-language-theory/concepts/lambda-calculus.td"} term that is in ${fref"programming-language-theory/concepts/normal-form.td"} but not a value.Stuck term value normal formA ${fref"programming-language-theory/concepts/lambda-calculus.td"} term that is in ${fref"programming-language-theory/concepts/normal-form.td"} but not a value.SubclassSemantics, Language feature/design, Programming paradigm A ${fref"programming-language-theory/concepts/class.td"} that extends a parent class.SubgoalTools: Rocq formerly CoqSubstitutabilityThe semantic/behavioral property that one value can safely replace another without breaking program correctness, of which ${fref"programming-language-theory/concepts/type-compatibility.td"} is a static approximation of.SubstitutionNo description yetSubstitution subjectA variable to which an object is substituted in.Substitution subject substitution targetA variable to which an object is substituted in.Substitution targetThe parameterized expression whose variables are substituted with objects.SubtypeA type $X$ that can be used wherever type $Y$ is expected - $X$ is \"more specific\" than $Y$.SubtypingThe ${fref"programming-language-theory/concepts/type-system.td"} mechanism that defines and enforces when substitution is allowed between types.Subtyping relationWritten $X <: Y$, a formal ordering on types meaning "$X$ is a ${fref"programming-language-theory/concepts/subtype.td"} of $Y$" - $X$ substitutes for $Y$.Sum of products (SoP)The structure of ${fref"programming-language-theory/concepts/algebraic-data-type.td"}s - sum because variants combine via "or" one of mt or node, product because each variant's fields combine via "and" a node has v and l and r.Sum typeAn algebraic datatype with multiple ${fref"programming-language-theory/concepts/type-variant.td"}s combined via "or" - a value is one of the variants, each with its own ${fref"programming-language-theory/concepts/constructor-tag.td"} e.g., BT = mt | node.Sum type union typeAn algebraic datatype with multiple ${fref"programming-language-theory/concepts/type-variant.td"}s combined via "or" - a value is one of the variants, each with its own ${fref"programming-language-theory/concepts/constructor-tag.td"} e.g., `BT = mt | node`.SupertypeIf $X$ is a ${fref"programming-language-theory/concepts/subtype.td"} of $Y$ then $Y$ is a supertype of $X$.Surface languageThe user-facing syntax of a programming language, including ${fref"programming-language-theory/concepts/syntactic-sugar.td"} and conveniences, as opposed to the ${fref"programming-language-theory/concepts/core-calculus-language.td"} that programs are desugared into.SymbolAs per Practical foundations for programming languages's terminology, an index to the families of operators. Given an ${fref"programming-language-theory/concepts/indexed-operator.td"} $o$ and a symbol $u$, $o[u]$ is an operator.Symbolic parameterAnalogous to ${fref"programming-language-theory/concepts/symbol.td"}.SymmetricA property of a ${fref"programming-language-theory/concepts/binary-relation.td"} $R$ on a set $T$ such that if $t\ R\ s$ then $s\ R\ t$, for every $t$, $s$ $\in T$.SymmetryNo description yetSyntactic abstractionA mechanism for defining new syntax forms, typically through ${fref"programming-language-theory/concepts/macro.td"}s, that expand into existing language constructs. Enables language extension without modifying the core implementation.Syntactic categorySyntax & Grammar According to Practical foundations for programming languages, largely analogous with ${fref"programming-language-theory/concepts/sort.td"}. Roughly means "syntactic type".Syntactic sugarA more convenient or readable syntax that is transformed into a ${fref"programming-language-theory/concepts/core-calculus-language.td"} construct, providing expressiveness without extending the language's fundamental semantics.Syntax tokenNo description yetSyntax treeNo description yetSystemPapers: On the Criteria To Be Used in Decomposing Systems into Modules ../../Papers/Papers/On%20the%20Criteria%20To%20Be%20Used%20in%20Decomposing%20Systems%20%2031baa8fcd08880429536c92add4ffb42.mdT45
TacticTools: Rocq formerly CoqTactic modifierTools: Rocq formerly CoqTagged unionSynonym for ${fref"programming-language-theory/concepts/sum-type.td"} - "union" because it combines variants, "tagged" because each variant has an explicit ${fref"programming-language-theory/concepts/constructor-tag.td"} distinguishing it unlike untagged ${fref"programming-language-theory/concepts/union-type.td"} types.Target languageThe language the compiled program is in.TermA term is a syntactic phrase in a grammar that represents computation and evaluates to a value - unlike ${fref"programming-language-theory/concepts/expression.td"} which broadly encompasses any well-formed syntactic construct including types, patterns, and declarations.Term expressionNo description yetTerm value${fref"programming-language-theory/concepts/lambda-abstraction.td"}s/Functions are the only values.The diamond problemAn ambiguity that arises in ${fref"programming-language-theory/concepts/multiple-inheritance.td"} when a class inherits from two classes that both inherit from a common ancestor, causing uncertainty about which inherited member to use.The plait programming languageA dialect of Lisp, based on Racket, but with ${fref"programming-language-theory/concepts/type-system.td"} resembling that of ML.TokenNo description yetTop-down constructionSynonymous with ${fref"programming-language-theory/concepts/backward-chaining.td"}.Total functionA ${fref"programming-language-theory/concepts/partial-function.td"} that is defined on all values of its domain.TraitThis is different from Rust's traitTrait mixinNote: Trait in this sense is different from Rust’s traits.Transition functionA ${fref"programming-language-theory/concepts/partial-function.td"} from machine configurations term, environment, stack, etc. to successor configurations, defining each atomic step of execution until a final state is reached. In ${fref"programming-language-theory/concepts/lambda-calculus.td"} with Small-step/Structural operational semantics SOS/plt/concepts/small-step-structural-operational-semantics-sos, the transition function usually relates a term with a simplification of that term, and is undefined for ${fref"programming-language-theory/concepts/normal-form.td"}s.TransitiveA property of a ${fref"programming-language-theory/concepts/binary-relation.td"} $R$ on a set $T$ such that if $t_0\ R\ t_1$ and $t_1\ R\ t_2$ then $t_0\ R\ t_2$, for every $t_0$, $t_1$, $t_2$ $\in T$.Transitive closureA smallest superset of a set that is ${fref"programming-language-theory/concepts/transitive.td"}.TransitivityNo description yetTrapped (runtime) errorAccording to "Type system" Luca Cardelli, 1996, a type of errors that immediately terminate the program, such as division by zero, array index out-of-bound in Java, Rust, etc.. These are deemed as safe as they cannot corrupt the program's state.Trapped runtime error untrapped runtime errorAccording to "Type system" Luca Cardelli, 1996, a type of errors that immediately terminate the program, such as division by zero, array index out-of-bound in Java, Rust, etc.. These are deemed as safe as they cannot corrupt the program's state.Tree-agnostic parserNo description yetTree inductionFormally, assume $a\ \text{tree}$ means that $a$ is a binary tree. To prove that whenever $a\ \text{tree}$, we have $\mathcal{P}(a)$, it's sufficient to show that:TruthyA value that evaluates as true in a boolean context despite not being literally true like non-zero numbers or non-empty strings in dynamic languages.Truthy falsy conditional expressionNo description yetTupleA data structure that groups a fixed number of values of possibly different types like 1, \"hello\", true, accessed by position rather than name.Tuple rocqMultiple fields inside a constructor.TurbofishNo description yetType annotationA syntactic hint to the ${fref"programming-language-theory/concepts/type-checker.td"} declaring the intended type of a term, used to guide inference, resolve ambiguity, or make types explicit for documentation.Type ascriptionNo description yetType checkerA program or algorithm that verifies type correctness by analyzing program text and ensuring expressions conform to typing rules before execution.Type compatibilityA relation between types that implies ${fref"programming-language-theory/concepts/substitutability.td"}. A static approximation of Substitutability.Type constructorA function at the type level that builds new types from existing ones, such as List, Array, or the arrow constructor $\\to$ that constructs function types.Type environmentA mapping from variable names to their types, often written as $\Gamma$, that tracks type bindings in scope during ${fref"programming-language-theory/concepts/type-checker.td"} analysis, extended when entering new binding forms.Type errorAccording to Programming languages: Application and Interpretation, an inability to construct a proof that a given term has some consistent type.Type inferenceThe automatic deduction of types from program context without explicit annotations, using constraint solving or unification algorithms e.g., ${fref"programming-language-theory/concepts/hindley-milner-system.td"} to determine usually the most general types.Type narrowingAnalogy: Think of types as sets, then type narrowing means to narrow a set ${fref"programming-language-theory/concepts/supertype.td"} -> ${fref"programming-language-theory/concepts/subtype.td"}.Type predicateA function that tests whether a value belongs to a specific type and informs the ${fref"programming-language-theory/concepts/type-checker.td"} of this fact - enables ${fref"programming-language-theory/concepts/type-narrowing.td"} after the check e.g., mt?, string?, typeof.Type safetyType theory, Language feature/design, Semantics According to Robert Bob Harper, the coherence between ${fref"programming-language-theory/concepts/static-semantics.td"} and ${fref"programming-language-theory/concepts/dynamic-semantics.td"}.Type safety language safetyThe property of a language in which every well-typed program accepted by the static semantics typing rules will never reach a “stuck term” state due to misusing values according to their types.Type systemA tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.Type theoryA ${fref"programming-language-theory/concepts/formal-system.td"} where every term has a type, providing a foundation for mathematics and programming through the ${fref"programming-language-theory/concepts/curry-howard-correspondence.td"} between proofs and programs.Type variableA placeholder e.g., $T$, $U$, $\\alpha$ representing an unknown or generic type - gets instantiated to a concrete type during type checking or remains polymorphic.Type variantA variant of a ${fref"programming-language-theory/concepts/sum-type.td"}.Type wideningAnalogy: Think of types as sets, then type widening means to widen a set ${fref"programming-language-theory/concepts/subtype.td"} -> ${fref"programming-language-theory/concepts/supertype.td"}.Typing judgmentA formal statement asserting that a term has a particular type under a given ${fref"programming-language-theory/concepts/type-environment.td"}, typically written as $\Gamma \vdash t : T$.U11
UnfoldA reduction step that replaces a defined name with its definition body, expanding abbreviations to expose underlying structure.UniformNo description yetUniformityNo description yetUnion typeUnion type: An untagged, ad-hoc combination of existing independent types e.g., U mt node - unlike ${fref"programming-language-theory/concepts/sum-type.td"} ${fref"programming-language-theory/concepts/algebraic-data-type.td"} where ${fref"programming-language-theory/concepts/type-variant.td"} are tagged and defined together as part of oneUnion type retrofitted type systemUnion type: An untagged, ad-hoc combination of existing independent types e.g., `(U mt node)` - unlike ${fref"programming-language-theory/concepts/sum-type.td"} ${fref"programming-language-theory/concepts/algebraic-data-type.td"} where ${fref"programming-language-theory/concepts/type-variant.td"} are tagged and defined together as part of one type.UniversalityNo description yetUntitledNo description yetUntrapped (runtime) errorAccording to "Type system" Luca Cardelli, 1996, a type of errors that does not terminate the program, such as buffer overflows, accessing deallocated memory, type punning gone wrong. These are deemed as dangerous as they can corrupt the program's state.Untyped calculus of booleans and numbers\dfrac{t_0 \to t_0'}{\text{if}\ t_0 \ \text{then}\ t_1\ \text{else}\ t_2 \to \text{if}\ t_0' \ \text{then}\ t_1\ \text{else}\ t_2 } \\ \\
\dfrac{t \to t'}{\text{succ}\ t \to \text{succ}\ t'} \\ \\
\dfrac{t \to t'}{\text{pred}\ t \to \text{pred}\ t'} \\ \\
\text{pred}\ \text{succ}\ nv \to nv \\ \\
\text{pred}\ 0 \to 0 \\ \\
\text{iszero}\ 0 \to \text{tru} \\ \\
\text{iszero}\ \text{succ}\ nv \to \text{fls} \\ \\
\dfrac{t \to t'}{\text{iszero}\ t \to \text{iszero}\ t'}
\end{array}Untyped calculus of booleans and numbers nonsensical term\dfrac{t_0 \to t_0'}{\text{if}\ t_0 \ \text{then}\ t_1\ \text{else}\ t_2 \to \text{if}\ t_0' \ \text{then}\ t_1\ \text{else}\ t_2 } \\ \\
\dfrac{t \to t'}{\text{succ}\ t \to \text{succ}\ t'} \\ \\
\dfrac{t \to t'}{\text{pred}\ t \to \text{pred}\ t'} \\ \\
\text{pred}\ \text{succ}\ nv \to nv \\ \\
\text{pred}\ 0 \to 0 \\ \\
\text{iszero}\ 0 \to \text{tru} \\ \\
\text{iszero}\ \text{succ}\ nv \to \text{fls} \\ \\
\dfrac{t \to t'}{\text{iszero}\ t \to \text{iszero}\ t'}
\end{array}UnwrapAn operation that extracts inner values from a wrapper type via ${fref"programming-language-theory/concepts/pattern-matching.td"} like getting x from Some x, exposing the contained data for use.V13
ValenceThe specification of how many variables a subterm binds and what ${fref"programming-language-theory/concepts/sort.td"}s types those variables have.Valence actual parameter argumentNo description yetValidityNo description yetValueA ${fref"programming-language-theory/concepts/term.td"} in ${fref"programming-language-theory/concepts/normal-form.td"} that is not deemed a bad state.Value environmentA mapping from variable names to runtime values used during interpretation.VariableSyntax & Grammar According to Practical foundations for programming languages , specifically Chapter 1. Abstract syntax, a syntactic variable which is a placeholder for an Abstract syntax tree AST/plt/concepts/abstract-syntax-tree-ast of a specific Sort.Variable abstract syntax tree astNo description yetVariable captureExample:Variable definitionA syntactic construct that introduces a new variable name and establishes a binding - optionally with an initial value e.g., let x = 5.Variadic treeA tree structure where operators can take a variable not fixed number of arguments, with that number determined by a ${fref"programming-language-theory/concepts/symbol.td"} index.VectorA contiguous, dynamically-sized array data structure supporting indexed access and operations like append, typically allocated on the ${fref"programming-language-theory/concepts/heap.td"}.VisibilityOwner: Huy Đỗ Nguyễn An
Category: Book walkthrough, Ruby
Parent wiki page: Ruby foundations ../Ruby%20foundations%2054af0db86b8a443b8ab70622d1aa508b.mdVisibleBooks & Chapters: Chapter 1 - The Psychopathology of Everyday Things ../../Books/Books%20&%20Chapters/Chapter%201%20-%20The%20Psychopathology%20of%20Everyday%20Things%202e8aa8fcd08880ab9bfaf8cd47f3634a.mdW5
WeakeningNo description yetWell-foundedThe property of a ${fref"programming-language-theory/concepts/preorder.td"} whose strict part $a < b \iff a \le b\land b \not\le a$ admits no infinite descending chains, ensuring every non-empty subset has a minimal element.Wildcard patternA ${fref"programming-language-theory/concepts/pattern.td"} usually written `_` that matches any value without binding it to a name, useful for ignoring irrelevant cases in ${fref"programming-language-theory/concepts/pattern-matching.td"}.Wildcard pattern rocqA ${fref"programming-language-theory/concepts/pattern.td"} usually written `_` that matches any value without binding it to a name, useful for ignoring irrelevant cases in ${fref"programming-language-theory/concepts/pattern-matching.td"}.WitnessA specific object that satisfies an existential claim, for example, a concrete value $t$ for $\exists x., P(x)$ such that $P(t)$ holds.