**Are you an EPFL student looking for a semester project?**

Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.

Concept# Free variables and bound variables

Summary

In mathematics, and in other disciplines involving formal languages, including mathematical logic and computer science, a variable may be said to be either free or bound. The terms are opposites. A free variable is a notation (symbol) that specifies places in an expression where substitution may take place and is not a parameter of this or any container expression. Some older books use the terms real variable and apparent variable for free variable and bound variable, respectively. The idea is related to a placeholder (a symbol that will later be replaced by some value), or a wildcard character that stands for an unspecified symbol.
In computer programming, the term free variable refers to variables used in a function that are neither local variables nor parameters of that function. The term non-local variable is often a synonym in this context.
An instance of a variable symbol is bound, in contrast, if the value of that variable symbol has been bound to a specific value or range o

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related publications

Loading

Related people

Loading

Related units

Loading

Related concepts

Loading

Related courses

Loading

Related lectures

Loading

Related publications (3)

Related people

No results

Loading

Loading

Loading

Related units

No results

Related concepts (24)

Mathematical logic

Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research i

Lambda calculus

Lambda calculus (also written as λ-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution.

Quantifier (logic)

In logic, a quantifier is an operator that specifies how many individuals in the domain of discourse satisfy an open formula. For instance, the universal quantifier \forall in the firs

Related courses (10)

COM-500: Statistical signal and data processing through applications

Building up on the basic concepts of sampling, filtering and Fourier transforms, we address stochastic modeling, spectral analysis, estimation and prediction, classification, and adaptive filtering, with an application oriented approach and hands-on numerical exercises.

CS-119(c): Information, Computation, Communication

L'objectif de ce cours est d'introduire les étudiants à la pensée algorithmique, de les familiariser avec les fondamentaux de l'Informatique et de développer une première compétence en programmation (langage C++).

CS-453: Concurrent algorithms

With the advent of multiprocessors, it becomes crucial to master the underlying algorithmics of concurrency. The objective of this course is to study the foundations of concurrent algorithms and in particular the techniques that enable the construction of robust such algorithms.

Pattern matching combined with regular expressions has many applications including text and XML processing, lexical analysis, classification of DNA segments and content-based routing. Patterns contain variables to refer to parts of the matching input. But regular patterns pose the problem of ambiguity: Words can be matched against 'overlapping' sections of the pattern in several ways, yielding different variable bindings. A match policy like shortest or longest match disambiguates the outcome of matching. In order to implement the longest/shortest match policies, we propose to compile regular patterns to sequential machines. This intuitive approach %to resolving ambiguities by means of shortest/longest match %policies (and the slightly different ungreedy/greedy match), with lets us derive a compilation scheme with linear runtime complexity. \par The main contributions of this paper are firstly, a decision procedure for unambiguous regular patterns, which can be matched with a single traversal of the input, and secondly, algorithms to obtain deterministic sequential machines from ambiguous patterns. These produce the shortest(longest) match in two consecutive runs. The first run produces an intermediary result from which all possible variable bindings can be reproduced. The second run then chooses the unique binding which adheres to the given match policy. In the general case, this approach is optimal.

2004Mirco Dotta, Viktor Kuncak, Philippe Paul Henri Suter

We describe a family of decision procedures that extend the decision procedure for quantifier-free constraints on recursive algebraic data types (term algebras) to support recursive abstraction functions. Our abstraction functions are catamorphisms (term algebra homomorphisms) mapping algebraic data type values into values in other decidable theories (e. g. sets, multisets, lists, integers, booleans). Each instance of our decision procedure family is sound; we identify a widely applicable many-to-one condition on abstraction functions that implies the completeness. Complete instances of our decision procedure include the following correctness statements: 1) a functional data structure implementation satisfies a recursively specified invariant, 2) such data structure conforms to a contract given in terms of sets, multisets, lists, sizes, or heights, 3) a transformation of a formula (or lambda term) abstract syntax tree changes the set of free variables in the specified way.

2010Christoph Koch, Lionel Emile Vincent Parreaux, Amir Shaikhha

Metaprograms are programs that manipulate (generate, analyze and evaluate) other programs. These tasks are greatly facilitated by quasiquotation, a technique to construct and deconstruct program fragments using quoted code templates expressed in the syntax of the manipulated language. We argue that two main flavors of quasiquotes have existed so far: Lisp-style quasiquotes, which can both construct and deconstruct programs but may produce code that contains type mismatches and unbound variables; and MetaML-style quasiquotes, which rely on static typing to prevent these errors, but can only construct programs. In this paper, we show how to combine the advantages of both flavors into a unified framework: we allow the construction, deconstruction and evaluation of program fragments while ensuring that generated programs are well-typed and well-scoped, a combination unseen in previous work. We formalize our approach as λ{}, a multi-stage calculus with code pattern matching and rewriting, and prove its type safety. We also present its realization in Squid, a metaprogramming framework for Scala, leveraging Scala's expressive type system. To demonstrate the usefulness of our approach, we introduce *speculative rewrite rules*, a novel code transformation technique that makes decisive use of these capabilities, and we outline how it simplifies the design of some crucial query compiler optimizations.

2018Related lectures (11)