Комбинатор с фиксированной точкой - это функция высшего порядка fix
, которая по определению удовлетворяет эквивалентности
forall f. fix f = f (fix f)
fix f
представляет собой решение x
для уравнение с фиксированной точкой
x = f x
Факториал натурального числа может быть доказан с помощью
fact 0 = 1
fact n = n * fact (n - 1)
Используя fix
, произвольные конструктивные доказательства над общими / µ-рекурсивными функциями могут быть получены без одноименной самоссылки.
fact n = (fix fact') n
где
fact' rec n = if n == 0
then 1
else n * rec (n - 1)
так, что
fact 3
= (fix fact') 3
= fact' (fix fact') 3
= if 3 == 0 then 1 else 3 * (fix fact') (3 - 1)
= 3 * (fix fact') 2
= 3 * fact' (fix fact') 2
= 3 * if 2 == 0 then 1 else 2 * (fix fact') (2 - 1)
= 3 * 2 * (fix fact') 1
= 3 * 2 * fact' (fix fact') 1
= 3 * 2 * if 1 == 0 then 1 else 1 * (fix fact') (1 - 1)
= 3 * 2 * 1 * (fix fact') 0
= 3 * 2 * 1 * fact' (fix fact') 0
= 3 * 2 * 1 * if 0 == 0 then 1 else 0 * (fix fact') (0 - 1)
= 3 * 2 * 1 * 1
= 6
Это формальное доказательство того, что
fact 3 = 6
методично использует эквивалентность комбинатора с фиксированной запятой для переписывает
fix fact' -> fact' (fix fact')
Формализм нетипизированного лямбда-исчисления состоит из контекстной грамматики
E ::= v Variable
| λ v. E Abstraction
| E E Application
где v
распространяется на переменные, вместе с правилами бета и сокращения
(λ x. B) E -> B[x := E] Beta
λ x. E x -> E if x doesn’t occur free in E Eta
Восстановление бета заменяет все свободные вхождения переменной x
в тело абстракции («функция») B
по выражению («аргумент») E
. Эта сокращение уменьшает избыточную абстракцию. Иногда это исключается из формализма. неприводимое выражение , к которому не применяется правило редукции, имеет нормальную или каноническую форму .
λ x y. E
- сокращение для
λ x. λ y. E
(абстракция, мультиарность),
E F G
- сокращение для
(E F) G
(приложение левой ассоциативности)
λ x. x
и
λ y. y
являются альфа-эквивалентами .
Абстракция и приложение являются двумя единственными «языковыми примитивами» лямбда-исчисления, но они позволяют кодировать произвольно сложных данных и операций.
Церковные цифры представляют собой кодировку натуральных чисел, сходных с Peano-аксиоматическими натуралами.
0 = λ f x. x No application
1 = λ f x. f x One application
2 = λ f x. f (f x) Twofold
3 = λ f x. f (f (f x)) Threefold
. . .
SUCC = λ n f x. f (n f x) Successor
ADD = λ n m f x. n f (m f x) Addition
MULT = λ n m f x. n (m f) x Multiplication
. . .
Формальное доказательство того, что
1 + 2 = 3
использует правило переписывания бета-сокращения:
ADD 1 2
= (λ n m f x. n f (m f x)) (λ g y. g y) (λ h z. h (h z))
= (λ m f x. (λ g y. g y) f (m f x)) (λ h z. h (h z))
= (λ m f x. (λ y. f y) (m f x)) (λ h z. h (h z))
= (λ m f x. f (m f x)) (λ h z. h (h z))
= λ f x. f ((λ h z. h (h z)) f x)
= λ f x. f ((λ z. f (f z)) x)
= λ f x. f (f (f x)) Normal form
= 3
В лямбда-исчислении, комбинаторы - это абстракции, которые не содержат свободных переменных. Проще говоря: I
, тождественный комбинатор
λ x. x
изоморфен тождественной функции
id x = x
Такие комбинаторы являются примитивными операторами исчислений комбинаторов подобно Лыжная система.
S = λ x y z. x z (y z)
K = λ x y. x
I = λ x. x
Уменьшение бета не сильно нормализует ; не все приводимые выражения, «redexes», сходятся к нормальной форме при бета-редукции. Простым примером является расходящееся применение комбинатора omega ω
λ x. x x
к себе:
(λ x. x x) (λ y. y y)
= (λ y. y y) (λ y. y y)
. . .
= _|_ Bottom
Приоритет является уменьшение крайних левых подвыражений («голов»). Аппликативный порядок нормализует аргументы перед заменой, нормальный порядок - нет. Эти две стратегии аналогичны стремлению к оценке, например, С и ленивая оценка, например, Haskell.
K (I a) (ω ω)
= (λ k l. k) ((λ i. i) a) ((λ x. x x) (λ y. y y))
расходится при энергичном сокращении бета-аппликативного порядка
= (λ k l. k) a ((λ x. x x) (λ y. y y))
= (λ l. a) ((λ x. x x) (λ y. y y))
= (λ l. a) ((λ y. y y) (λ y. y y))
. . .
= _|_
, поскольку в строгая семантика
forall f. f _|_ = _|_
, но сходится при ленивой бете нормального порядка сокращение
= (λ l. ((λ i. i) a)) ((λ x. x x) (λ y. y y))
= (λ l. a) ((λ x. x x) (λ y. y y))
= a
Если выражение имеет нормальную форму, бета-редукция нормального порядка найдет его.
Существенное свойство Y
комбинатора с фиксированной точкой
λ f. (λ x. f (x x)) (λ x. f (x x))
задается в
Y g
= (λ f. (λ x. f (x x)) (λ x. f (x x))) g
= (λ x. g (x x)) (λ x. g (x x)) = Y g
= g ((λ x. g (x x)) (λ x. g (x x))) = g (Y g)
= g (g ((λ x. g (x x)) (λ x. g (x x)))) = g (g (Y g))
. . . . . .
. эквивалентность
Y g = g (Y g)
изоморфна
fix f = f (fix f)
Нетипизированное лямбда-исчисление может кодировать произвольные конструктивные доказательства над общими / µ-рекурсивными функциями.
FACT = λ n. Y FACT' n
FACT' = λ rec n. if n == 0 then 1 else n * rec (n - 1)
FACT 3
= (λ n. Y FACT' n) 3
= Y FACT' 3
= FACT' (Y FACT') 3
= if 3 == 0 then 1 else 3 * (Y FACT') (3 - 1)
= 3 * (Y FACT') (3 - 1)
= 3 * FACT' (Y FACT') 2
= 3 * if 2 == 0 then 1 else 2 * (Y FACT') (2 - 1)
= 3 * 2 * (Y FACT') 1
= 3 * 2 * FACT' (Y FACT') 1
= 3 * 2 * if 1 == 0 then 1 else 1 * (Y FACT') (1 - 1)
= 3 * 2 * 1 * (Y FACT') 0
= 3 * 2 * 1 * FACT' (Y FACT') 0
= 3 * 2 * 1 * if 0 == 0 then 1 else 0 * (Y FACT') (0 - 1)
= 3 * 2 * 1 * 1
= 6
(Задержка умножения, слияние)
Для нетипизированного лямбда-исчисления Черча, как было показано, существует рекурсивно перечислимая бесконечность комбинаторов с фиксированной точкой, кроме Y
.
X = λ f. (λ x. x x) (λ x. f (x x))
Y' = (λ x y. x y x) (λ y x. y (x y x))
Z = λ f. (λ x. f (λ v. x x v)) (λ x. f (λ v. x x v))
Θ = (λ x y. y (x x y)) (λ x y. y (x x y))
. . .
Бета-редукция нормального порядка превращает неинтенсивное нетипизированное лямбда-исчисление в систему полного переписывания по Тьюрингу.
В Хаскеле комбинатор с фиксированной точкой может быть элегантно реализован
fix :: forall t. (t -> t) -> t
fix f = f (fix f)
Лень Хаскелла нормализуется до конечности до того, как все подвыражения будут оценены.
primes :: Integral t => [t]
primes = sieve [2 ..]
where
sieve = fix (\ rec (p : ns) ->
p : rec [n | n <- ns
, n `rem` p /= 0])
yes , http://www.gidforums.com/t-1816.html
<?php
/**
NAME : autolink()
VERSION : 1.0
AUTHOR : J de Silva
DESCRIPTION : returns VOID; handles converting
URLs into clickable links off a string.
TYPE : functions
======================================*/
function autolink( &$text, $target='_blank', $nofollow=true )
{
// grab anything that looks like a URL...
$urls = _autolink_find_URLS( $text );
if( !empty($urls) ) // i.e. there were some URLS found in the text
{
array_walk( $urls, '_autolink_create_html_tags', array('target'=>$target, 'nofollow'=>$nofollow) );
$text = strtr( $text, $urls );
}
}
function _autolink_find_URLS( $text )
{
// build the patterns
$scheme = '(http:\/\/|https:\/\/)';
$www = 'www\.';
$ip = '\d{1,3}\.\d{1,3}\.\d{1,3}\.\d{1,3}';
$subdomain = '[-a-z0-9_]+\.';
$name = '[a-z][-a-z0-9]+\.';
$tld = '[a-z]+(\.[a-z]{2,2})?';
$the_rest = '\/?[a-z0-9._\/~#&=;%+?-]+[a-z0-9\/#=?]{1,1}';
$pattern = "$scheme?(?(1)($ip|($subdomain)?$name$tld)|($www$name$tld))$the_rest";
$pattern = '/'.$pattern.'/is';
$c = preg_match_all( $pattern, $text, $m );
unset( $text, $scheme, $www, $ip, $subdomain, $name, $tld, $the_rest, $pattern );
if( $c )
{
return( array_flip($m[0]) );
}
return( array() );
}
function _autolink_create_html_tags( &$value, $key, $other=null )
{
$target = $nofollow = null;
if( is_array($other) )
{
$target = ( $other['target'] ? " target=\"$other[target]\"" : null );
// see: http://www.google.com/googleblog/2005/01/preventing-comment-spam.html
$nofollow = ( $other['nofollow'] ? ' rel="nofollow"' : null );
}
$value = "<a href=\"$key\"$target$nofollow>$key</a>";
}
?>
Вот фрагмент электронного письма:
$email = "abc@def.com";
$pos = strrpos($email, "@");
if (!$pos === false) {
// This is an email address!
$email .= "mailto:" . $email;
}
Что именно вы собираетесь делать со ссылками? убрать www или http? или добавьте http: // www к любой ссылке, если требуется?