Module logic

A version of first order logic, built on top of the untyped lambda calculus.

The class of Expression has various subclasses:

Classes

Error

Variable
A variable, either free or bound.

Constant
A nonlogical constant.

Expression
The abstract class of a lambda calculus expression.

VariableExpression
A variable expression which consists solely of a variable.

IndVariableExpression
An individual variable expression, as determined by is_indvar().

ConstantExpression
A constant expression, consisting solely of a constant.

Operator
A boolean operator, such as 'not' or 'and', or the equality relation ('=').

VariableBinderExpression
A variable binding expression: e.g.

LambdaExpression
A lambda expression: \x.M.

SomeExpression
An existential quantification expression: some x.M.

AllExpression
A universal quantification expression: all x.M.

ApplicationExpression
An application expression: (M N).

Parser
A lambda calculus expression parser.

Functions

Boolean

is_indvar(expr)
Check whether an expression has the form of an individual variable.

source code

expressions()
Return a sequence of test expressions.

source code

demo()

source code

Function Details

Check whether an expression has the form of an individual variable.

An individual variable matches the following regex: '^[wxyz](\d*)'.

Parameters:

Returns: Boolean