Lambda

class proveit.Lambda(parameter_or_parameters, body, *, styles=None)

Bases: proveit.Expression

A lambda-function Expression. A lambda function maps parameter(s) to its body. For example, (x, y) -> sin(x^2 + y), where (x, y) are the parameters and sin(x^2 + y) is the body. Each parameter must be a Variable. Note that the body of a Lambda may be a Conditional such that the mapping is only defined when one of the conditions is satisfied.

Methods Summary

apply(self, \*operands[, …])	Apply this lambda map onto the given operands (a beta reduction in the lambda calculus terminology), returning the expression that results from applying the map.
compose(self, lambda2)	Given some x -> f(x) for self (lambda1) and y -> g(y) for lambda2, return x -> f(g(x)).
extract_argument(self, mapped_expr)	Given a mapped expression, return the argument that will transform this Lambda expression into the mapped expression.
extract_arguments(self, mapped_expr)	Given a mapped expression, return the arguments that will transform this Lambda expression into the mapped expression.
global_repl(master_expr, sub_expr[, assumptions])	Returns the Lambda map for replacing the given sub-Expression everywhere that it occurs in the master Expression.
latex(self, \*\*kwargs)	Return a latex-formatted representation of the Expression.
relabeled(self, relabel_map)	Return a variant of this Lambda expression with one or more of its parameter labels changed.
remake_arguments(self)	Yield the argument values or (name, value) pairs that could be used to recreate the Lambda expression.
string(self, \*\*kwargs)	Return a string representation of the Expression.

Methods Documentation

apply(self, \*operands, param_to_num_operand_entries=None, equiv_alt_expansions=None, allow_relabeling=False, assumptions=None, requirements=None)

Apply this lambda map onto the given operands (a beta reduction in the lambda calculus terminology), returning the expression that results from applying the map. Assumptions may be necessary to prove requirements that will be passed back if a requirements list is provided. Requirements may be needed to ensure that operands are an appropriate length to match a corresponding ExprRange of parameters. Specifically, the Len of an ExprTuple containing the operands must equal the Len of an ExprTuple containing the range of indices covered by a corresponding parameter range (see the example below). Full automation of the length proof will only be performed for the last parameter entry; proving the length equivalence may need to be performed in advance.

For example, applying the Lambda (x, y_1, …, y_3, z_i, …, z_j) ->

x*y_1 + … + x*y_3 + z_i + … + z_j

to operands (a, b, c, d, e_m, …, e_n, f) will result in a*b + a*c + a*d + e_m + … _ e_n + f provided that|(b, c, d)| = |(1, ..., 3)| is proven in advance and that |(e_m, ..., e_n, f)| = |(i, ..., j)| can be proven via automation.

A dictionary may be provided for equiv_alt_expansions to accomplish instantiation of ranges of parameters with more versatility. For example, given the following Lambda (x_1, …, x_{n+1}) -> (x_1 < x_{1+1}) and …

and (x_n < x_{n+1})

we can apply this on the following operands:

(a_1, …, a_{k+1}, b_1, …, b_{n-k})

along with the following entries in equiv_alt_expansions (x_1, …, x_n, x_{n+1}) :

(a_1, …, a_k, a_{k+1}, b_1, …, b_{n-k-1}, b_{n-k})

(x_1, x_{1+1}, …, x_{n+1}) :

(a_1, a_{1+1}, …, a_{k+1}, b_1,

b_{1+1}, …, b_{(n-k-1)+1})

to obtain (a_1 < a_{1+1}) and … and (a_k < a_{k+1}) and a_k < b_1

and (b_1 < b_{1+1}) and … and (b_{n-k-1} < b_{(n-k-1)+1})

under the following requirements: |(a_1, ..., a_{k+1}, b_1, ..., b_{n-k})| = |(1, ..., n+1)| (1, …, n) = (1, …, n, n+1) (1, …, n) = (1, 1+1, …, n+1) (a_1, …, a_{k+1}, b_1, …, b_{n-k})

= (a_1, …, a_k, a_{k+1}, b_1, …, b_{n-k-1}, b_{n-k})

(a_1, …, a_{k+1}, b_1, …, b_{n-k})

= (a_1, a_{1+1}, …, a_{k+1}, b_1,

b_{1+1}, …, b_{(n-k-1)+1})

|({a_1, ..., a_k, a_{k+1}, b_1, ..., b_{n-k-1})|

= |(1, ..., n)|

|(a_{1+1}, ..., a_{k+1}, b_1, b_{1+1}, ..., b_{(n-k-1)+1})|

= |(1+1, ..., n+1)|

If allow relabeling is True then inn

There are limitations with respect the Lambda map application involving parameter ranges when perfoming operation substitution in order to keep derivation rules (i.e., instantiation) simple. For details, see the ExprRange.replaced documentation.

There may be additional requirements introduced when expanding ranges. For example, indices may need to match, not just lengths.

compose(self, lambda2)

Given some x -> f(x) for self (lambda1) and y -> g(y) for lambda2, return x -> f(g(x)). Also works with multiple parameters: x1, x2, …, xn -> f(x1, x2, …, xn) for lambda 1 and y1, y2, …, yn -> g1(y1, y2, …, yn), y1, y2, …, yn -> g2(y1, y2, …, yn), … y1, y2, …, yn -> gn(y1, y2, …, yn) for lambda2 returns x1, x2, …, xn -> f(g1(x1, x2, …, xn), g2(x1, x2, …, xn), …, gn(x1, x2, …, xn)).

extract_argument(self, mapped_expr)

Given a mapped expression, return the argument that will transform this Lambda expression into the mapped expression. For example, if the Lambda expression is x -> x + 1 and the mapped expression is 2 + 1, this will return 2. If there is more than one parameter in this Lambda expression, use extract_arguments instead.

extract_arguments(self, mapped_expr)

Given a mapped expression, return the arguments that will transform this Lambda expression into the mapped expression. For example, if the Lambda expression is (x, y) -> x + y and the mapped expression is 1 + 2, this will return (1, 2).

global_repl(master_expr, sub_expr, assumptions=None)

Returns the Lambda map for replacing the given sub-Expression everywhere that it occurs in the master Expression.

When replacing an ExprTuple of operands, we will return a lambda expression with a range of parameters for replacing the operands individually. For example,

master_expr : a + b + c sub_expr : (a, b, c) will return something equal to

(a_1, …, a_3) -> a_1 + … + a_3

‘assumptions’ may be required for computing the number of operands (which may contain ranges themselves) in this latter process.

latex(self, \*\*kwargs)

Return a latex-formatted representation of the Expression. The kwargs can contain formatting directives (such as ‘fence’ used to indicate when a sub-expression should be wrapped in parentheses if there can be ambiguity in the order of operations).

relabeled(self, relabel_map)

Return a variant of this Lambda expression with one or more of its parameter labels changed. The resulting expression should be “equal” to the original (having the same meaning) but essentially has a different “style” (formats differently) and uses different labels for substitution purposes.

remake_arguments(self)

Yield the argument values or (name, value) pairs that could be used to recreate the Lambda expression.

string(self, \*\*kwargs)

Return a string representation of the Expression. The kwargs can contain formatting directives (such as ‘fence’ used to indicate when a sub-expression should be wrapped in parentheses if there can be ambiguity in the order of operations).