Capture-avoiding substitution
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889909192
=begin pod
Perl 6 program that implements the capture-avoiding substitution algorithm
described at
L<http://www.mcrl2.org/web/developer_manual/_downloads/substitutions.pdf>.
=end pod
role Expr {
}
class Var does Expr {
has Str $.var;
}
class Abs does Expr {
has Str $.param;
has Expr $.body;
}
class App does Expr {
has Expr $.fun;
has Expr $.arg;
}
sub var($var) { Var.new(:$var) }
sub abs($param, $body) { Abs.new(:$param, :$body) }
sub app($fun, $arg) { App.new(:$fun, :$arg) }
proto expr-free(Expr:D $expr --> Set:D) {*}
multi expr-free(Var:D $expr --> Set:D) {
set($expr.var);
}
multi expr-free(Abs:D $expr --> Set:D) {
expr-free($expr.body) ∖ set($expr.param);
}
multi expr-free(App:D $expr --> Set:D) {
expr-free($expr.fun) ∪ expr-free($expr.arg);
}
sub subst-free(%subst --> Set:D) {
[∪] %subst.kv.map: { expr-free($^b) ∖ set($^a) };
}
sub fresh(--> Str:D) {
'$' ~ (state $ = 'a')++;
}
sub subst(Str:D $var --> Expr:D) {
%*subst{$var} // var($var);
}
proto subst-ca(Expr:D $expr --> Expr:D) {*}
multi subst-ca(Var:D $expr --> Expr:D) {
subst($expr.var);
}
multi subst-ca(Abs:D $expr --> Expr:D) {
my $captures = subst($expr.param) !eqv var($expr.param) || $expr.param ∈ $*free;
my $new-param = $captures ?? fresh() !! $expr.param;
(temp %*subst){$expr.param} = var($new-param);
temp $*free ∪= set($new-param);
abs($new-param, subst-ca($expr.body));
}
multi subst-ca(App:D $expr --> Expr:D) {
App.new(
fun => subst-ca($expr.fun),
arg => subst-ca($expr.arg),
);
}
my $lambda = abs('a', abs('b', var('a')));
say app($lambda, var('b'));
{
my %*subst = a => var('b');
my $*free = expr-free($lambda.body) ∪ subst-free(%*subst);
say subst-ca($lambda.body);
}
{
my %*subst;
my $*free = expr-free($lambda.body) ∪ subst-free(%*subst);
say subst-ca($lambda.body);
}
Raku
INFO