I am creating a C# library for Lambda calculus and lambda terms and I have error in my code:
namespace Datatypes.Collections.MathCollections
{
public abstract record Expression;
public record Variable(char Name) : Expression;
public record Function(Variable Parameter, Expression Body) : Expression;
public record Application(Expression Function, Expression Argument) : Expression;
public abstract record Token;
public record LeftParentheses : Token;
public record Letter(char Value) : Token;
public record Lambda : Token;
public record Dot : Token;
public record RightParentheses : Token;
public static class Evaluator
{
public static string Evaluate(this string program) => new(program.Tokenize().Parse().Interpret().Unparse().Untokenize().ToArray());
public static string Bruijn(this string program) => new string(program.Tokenize().Parse().ToBruijn().Unparse().Untokenize().ToArray());
public static string BruijnBinary(this string program) => program.Tokenize().Parse().ToBruijn().ToBinary();
}
public static class Interpreter
{
public static Expression Interpret(this Expression expression) => expression.Interpret(100);
public static Expression Interpret(this Expression expression, int maxReductions) =>
expression.CanReduce() && maxReductions >= 0 ? expression.Reduce().Interpret(--maxReductions) : expression;
public static bool CanReduce(this Expression expression) => expression.HasBetaRedex();
public static bool HasBetaRedex(this Expression expression) => expression switch
{
Variable => false,
Function function => function.Parameter.HasBetaRedex() || function.Body.HasBetaRedex(),
Application application => application.Function switch
{
Function => true,
_ => application.Function.HasBetaRedex() || application.Argument.HasBetaRedex()
},
_ => throw new Exception()
};
public static Expression Reduce(this Expression expression) => expression switch
{
Variable variable => variable,
Function function => function with { Body = function.Body.Reduce() },
Application application => application.Function switch
{
Function function => function.BetaReduce(application.Argument),
Expression expression1 => new Application(expression1.Reduce(), application.Argument.Reduce())
},
_ => throw new Exception()
};
public static Expression BetaReduce(this Function function, Expression argument) =>
Substitude(argument, function.Parameter, function.Body);
public static Expression Substitude(Expression argument, Variable parameter, Expression body) => body switch
{
Variable variable => parameter == body ? argument : variable,
Function function => parameter == function.Parameter
? function
: !function.Parameter.VariableOccursFree(argument)
? function with { Body = Substitude(argument, parameter, function.Body) }
: Substitude(argument, parameter, function.AlphaConvert()),
Application application => new Application(Substitude(argument, parameter, application.Function), Substitude(argument, parameter, application.Argument)),
_ => throw new Exception()
};
public static bool VariableOccursFree(this Variable variable, Expression expression) => expression switch
{
Variable variable1 => variable == variable1,
Application application => (variable.VariableOccursFree(application.Function) || variable.VariableOccursFree(application.Argument)),
Function function => function.Parameter != variable && variable.VariableOccursFree(function.Body),
_ => throw new Exception()
};
public static Function AlphaConvert(this Function function) =>
function.Parameter.NextVariableThatDoesntOccurInBody(function.Body).Pipe(variable => new Function(variable, Convert(function.Parameter, variable, function.Body)));
public static Expression Convert(this Variable variableToConvertFrom, Variable variableToConvertTo, Expression expressionToConvert) => expressionToConvert switch
{
Variable variableToConvert =>
variableToConvert == variableToConvertFrom ? variableToConvertTo : variableToConvert,
Application applicationToConvert =>
new Application(Convert(variableToConvertFrom, variableToConvertTo, applicationToConvert.Function), Convert(variableToConvertFrom, variableToConvertTo, applicationToConvert.Argument)),
Function functionToConvert => functionToConvert.Parameter == variableToConvertFrom || functionToConvert.Parameter == variableToConvertTo
? functionToConvert
: new Function(functionToConvert.Parameter, Convert(variableToConvertFrom, variableToConvertTo, functionToConvert.Body)),
_ => throw new Exception()
};
public static Variable NextVariableThatDoesntOccurInBody(this Variable variable, Expression body) =>
variable.NextVariable().Pipe(nextVariable => IsVariableInBody(nextVariable, body) ? NextVariableThatDoesntOccurInBody(nextVariable, body) : nextVariable);
public static bool IsVariableInBody(this Variable variable, Expression body) => body switch
{
Variable variable1 => variable == variable1,
Application application => variable.IsVariableInBody(application.Function) || variable.IsVariableInBody(application.Argument),
Function function => variable.IsVariableInBody(function.Parameter) || variable.IsVariableInBody(function.Body),
_ => throw new Exception()
};
public static Variable NextVariable(this Variable variable) => new Variable(variable.Name.NextLowerCaseLetter());
public static char NextLowerCaseLetter(this char value) => value switch
{
'z' => 'a',
_ => (char)(value + 1)
};
}
public static class BruijnConverter
{
public static Expression ToBruijn(this Expression expression, List<char> context = null) => expression switch
{
Variable variable => new DeBruijnIndex((context ?? new List<char>()).LastIndexOf(variable.Name) + 1),
Function function => new Function((Variable)null, function.Body.ToBruijn(new List<char> { function.Parameter.Name }.Concat(context ?? Enumerable.Empty<char>()).ToList())),
Application application => new Application(application.Function.ToBruijn(context), application.Argument.ToBruijn(context)),
_ => throw new Exception()
};
public static string ToBinary(this Expression expression) => expression switch
{
DeBruijnIndex index => new string('1', index.Value) + "0",
Function function => "00" + function.Body.ToBinary(),
Application application => "01" + application.Function.ToBinary() + application.Argument.ToBinary(),
_ => throw new Exception()
};
public record DeBruijnIndex(int Value) : Expression;
}
public static class Parser
{
public static Expression Parse(this IEnumerable<Token> tokens) => ParseRecursive(tokens).Expression;
private static (Expression Expression, IEnumerable<Token> UnusedTokens) ParseRecursive(this IEnumerable<Token> tokens) => tokens.First() switch
{
LeftParentheses => tokens.Skip(1).ParseRecursive().Pipe(left => left.UnusedTokens.ParseRecursive().Pipe(right => (new Application(left.Expression, right.Expression), right.UnusedTokens.Skip(1)))),
Letter letter => (new Variable(letter.Value), tokens.Skip(1)),
Lambda => tokens.Skip(1).ParseRecursive().Pipe(parameter => parameter.UnusedTokens.Skip(1).ParseRecursive().Pipe(body => (new Function((Variable)parameter.Expression, body.Expression), body.UnusedTokens))),
_ => throw new Exception(),
};
public static IEnumerable<Token> Unparse(this Expression expression) => expression switch
{
Variable variable => new List<Token> { new Letter(variable.Name) },
Function function => new List<Token> { new Lambda() }
.Concat(Unparse(function.Parameter))
.Concat(new List<Token> { new Dot() })
.Concat(Unparse(function.Body)),
Application application => new List<Token> { new LeftParentheses() }
.Concat(Unparse(application.Function))
.Concat(Unparse(application.Argument))
.Concat(new List<Token> { new RightParentheses() }),
_ => throw new Exception()
};
}
public static class Lexer
{
public static IEnumerable<Token> Tokenize(this IEnumerable<char> characters) => characters.Select<char, Token>(character => character switch
{
'(' => new LeftParentheses(),
'λ' => new Lambda(),
'.' => new Dot(),
')' => new RightParentheses(),
_ when char.IsLower(character) => new Letter(character),
_ => throw new Exception()
});
public static IEnumerable<char> Untokenize(this IEnumerable<Token> tokens) => tokens.Select(token => token switch
{
LeftParentheses => '(',
Lambda => 'λ',
Dot => '.',
RightParentheses => ')',
Letter letter => letter.Value,
_ => throw new Exception()
});
}
public static class PipeExtensions
{
public static TOutput Pipe<TInput, TOutput>(this TInput input, Func<TInput, TOutput> function) => function(input);
}
}
I am trying to parse lambda terms and create binary numbers to store as true binaries. I used wiki for the rules on how to do it.
To convert lambda calculus expressions into de Bruijn notation and then into their binary representation, follow these steps: Replace each variable with an index representing the number of lambdas between its binding lambda and its occurrence, counting the abstraction levels needed to find the binding abstraction. For example, in λx. x
, the variable x
becomes 1
because it is bound by the closest lambda. Abstractions are represented as λ. M'
, where M'
is the de Bruijn notation of M
, without naming the bound variable. Applications are represented as (M' N')
, where M'
and N'
are the de Bruijn notations of M
and N
. For example, λa.λb. abb
becomes λ. λ. 2 1 1
. To convert this into binary, each index i
is represented as 1
repeated i
times followed by 0
(e.g., index 1
is 10
, index 2
is 110
). Abstractions are represented as 00M'
and applications as 01M'N'
. Hence, λ. λ. 2 1 1
converts to 000011011010
, concatenating the binary forms of indices, abstractions, and applications. Thus, λa.λb. abb
translates to de Bruijn notation λ. λ. 2 1 1
and binary representation 000011011010
.
Please look at Binary Combinatory Logic as this was my main source on how to do it. All I want from this code is this:
- Simplification of lambda terms using alpha and beta reduction
- Output of de Bruijn notation
- Binary de Bruijn numbers
I tested it out on this input:
string lambdaExpression = "λa.λb.λc.abc(ab)";
Console.WriteLine(lambdaExpression.Evaluate().ToString());
Console.WriteLine(lambdaExpression.BruijnBinary());
The function lambdaExpression.Bruijn()
is broken so gives and error but other work.
Evaluate
gives a wrong answer: λa.λb.λc.a
And BruijnBinary
outputs: 0000001110
Please help!
Ruslan Golov is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.