* @author Christian Fraß */ public $mapping; /** * @param map * @author Christian Fraß */ public function __construct( array $mapping ) { $this->mapping = $mapping; } } /** * @author Christian Fraß */ function _substitution_clone( struct_substitution $substitution ) : struct_substitution { $mapping_ = []; foreach ($substitution->mapping as $name => $term) { $mapping[$name] = $term->clone_(); } return (new struct_substitution($mapping_)); } /** * @return set * @author Christian Fraß */ function _substitution_domain( struct_substitution $substitution ) : array { return array_keys($substitution->mapping); } /** * @param set $names * @author Christian Fraß */ function _substitution_restricted( struct_substitution $substitution, array $set ) : struct_substitution { $mapping = []; foreach ($substitution->mapping as $name => $term) { if (in_array($name, $set)) { $mapping[$name] = $term; } } return (new struct_substitution($mapping)); } /** * @author Christian Fraß */ function substitution_instance( struct_substitution $substitution, interface_term $term ) : interface_term { if ($term instanceof class_variable) { $variable = $term; return ( array_key_exists($variable->name, $substitution->mapping) ? $substitution->mapping[$variable->name] : $term->clone_() ); } else if ($term instanceof class_function) { $function = $term; return ( new class_function( $function->head, \alveolata\list_\map( $function->arguments, function ($argument) use (&$substitution) { return substitution_instance($substitution, $argument); } ) ) ); } else { throw (new \Exception('invalid term')); } } /** * @author Christian Fraß */ function _substitution_compose( struct_substitution $substitution1, struct_substitution $substitution2 ) : struct_substitution { $substitution3 = _substitution_clone($substitution1); $domain1 = _substitution_domain($substitution1); // überschreiben der vorhandenen Zuordnungen und entfernen der Identitäten { foreach ($domain1 as $name) { $term = substitution_instance($substitution2, $substitution1->mapping[$name]); if (equal(new class_variable($name), $term)) { unset($substitution3->mapping[$name]); } else { $substitution3->mapping[$name] = $term; } } } // hinzufügen der neuen Ersetzungen { $domain2 = _substitution_domain($substitution2); foreach ($domain2 as $name) { if (! in_array($name, $domain1)) { $substitution3->mapping[$name] = $substitution2->mapping[$name]; } } } return $substitution3; } /** * @author Christian Fraß */ function _substitution_empty( ) : struct_substitution { return (new struct_substitution([])); } /** * ermittelt die anzuwendenen Substiutionen und die neuen Term-Paare für ein gegebenes Term-Paar * * @param record $pair * @return record,pairs:list>> */ function _unificationstep( array $pair ) : array { $nothing = [ 'substitutions' => [], 'pairs' => [], ]; if ($pair['first'] instanceof class_variable) { $x_variable = $pair['first']; if ($pair['second'] instanceof class_variable) { $y_variable = $pair['second']; return [ 'substitutions' => \alveolata\list_\map( [ ['from' => $x_variable, 'to' => $y_variable], ['from' => $y_variable, 'to' => $x_variable], ], function (array $satz) : struct_substitution { $mapping = []; if (! ($satz['from']->name === $satz['to']->name)) { $mapping[$satz['from']->name] = $satz['to']; } else { // do nothing } return (new struct_substitution($mapping)); } ), 'pairs' => [], ]; } else { if (contains($pair['second'], $x_variable)) { return $nothing; } else { return [ 'substitutions' => [ new struct_substitution([$x_variable->name => $pair['second']]), ], 'pairs' => [], ]; } } } else if ($pair['first'] instanceof class_function) { $x_function = $pair['first']; if ($pair['second'] instanceof class_variable) { return [ 'substitutions' => [_substitution_empty()], 'pairs' => ['first' => $pair['second'], 'second' => $pair['first']], ]; } else if ($pair['second'] instanceof class_function) { $y_function = $pair['second']; if ($x_function->head === $y_function->head) { if (count($x_function->arguments) === count($y_function->arguments)) { return [ 'substitutions' => [_substitution_empty()], 'pairs' => \alveolata\list_\zip( $x_function->arguments, $y_function->arguments, false ), ]; } else { throw (new \Exception('ungleiche Anzahl an Argumenten bei Funktionen mit gleichem Kopf')); } } else { return $nothing; } } else { throw (new \Exception('ungültiger Term')); } } else { throw (new \Exception('ungültiger Term')); } } /** * ermittelt die Menge aller allgemeinsten unifiers * * @param list> $problem * @param int [$depth] * @return list * @author Christian Fraß */ function unifiers( array $problem, int $depth = 0 ) : array { $solution = null; if (empty($problem)) { $solution = [_substitution_empty()]; } else { $components = [ 'head' => $problem[0], 'rest' => array_slice($problem, 1), ]; $step = _unificationstep($components['head']); $solution = \alveolata\list_\reduce( $step['substitutions'], [], function (array $solution_, struct_substitution $substitution) use ($depth, &$components, &$step) { $rest = \alveolata\list_\map( $components['rest'], function ($pair) use (&$substitution) { return [ 'first' => substitution_instance($substitution, $pair['first']), 'second' => substitution_instance($substitution, $pair['second']), ]; } ); $subsolution = unifiers( \alveolata\list_\concat($step['pairs'], $rest), $depth+1 ); return \alveolata\list_\concat( $solution_, \alveolata\list_\map( $subsolution, function ($substitution_) use (&$substitution) { return _substitution_compose($substitution, $substitution_); } ) ); } ); } \alveolata\log\debug( 'unification', [ 'problem' => implode( ' + ', \alveolata\list_\map( $problem, function ($pair) { return sprintf( '[%s ~ %s]', to_string($pair['first']), to_string($pair['second']) ); } ) ), 'solution' => $solution, ] ); return $solution; } /** * @author Christian Fraß */ function unifier( interface_term $x, interface_term $y ) : struct_substitution { return ( unifiers( [ [ 'first' => $x, 'second' => $y ] ] )[0] ); }